Trusted Logic's Approach to Security for Embedded Systems: Innovation and Pragmatism

by Dominique Bolignano, Daniel Le Métayer and Claire Loiseaux

Trusted Logic is a start-up company stemming from INRIA which was created in January 1999. Its core business is the development and validation of secure embedded systems.

IT security is an area with great opportunities thanks to the ever increasing use of embedded components in everyday life (payment cards and terminals, GSM SIM cards, electronic purses etc). It also involves technical challenges because of the very high expectations of the market regarding security (confidentiality, integrity etc) and the scarce resources of devices such as smart cards and small terminals. One of the reasons for Trusted Logic’s success is a pragmatic approach based on the combination of two complementary ingredients:

• the definition and the application of rigorous methodologies and
• the design and use of appropriate innovative tools.

Because security is by its nature a global concern, this combination of methodologies and tools covers all the steps of the design, development and validation of IT products. Here we provide some examples of key components of the security chain and briefly outline Trusted Logic solutions.

System Design: from Security Analysis to Design and Development
Relying on its experience in security evaluation, Trusted Logic has put forward a methodology covering the complete IT product lifecycle: from the risk analysis to the definition of the security architecture and the development of the product. This methodology is based on a precise definition of the model of the IT environment (including roles, assets to be protected, threats, etc.) and the different refinement levels of the product (from the functional specification to the implementation). Most importantly, this approach is in line with the Common Criteria which is the international standard for the evaluation of IT product security. In some sense, it can even be seen as an interpretation of the Common Criteria based on Trusted Logic complementary expertises in security, formal methods and software development.

Trusted Logic has developed a tool supporting its methodology for stepwise refinement. This tool, called TL-FIT, provides a variety of functionalities including modelisation, model consistency checking (both internal and refinement) and Common Criteria document generation. TL-FIT illustrates the pragmatic approach stressed in the introduction because it makes it possible to adapt the description style (informal, semi-formal, formal) and the associated verifications to the level of assurance stemming from the risk analysis. It is also representative of the need for innovation in this area since no other instrumented interpretation of the Common Criteria has been proposed so far and the proper integration of formal and semi-formal methods is still a very active research area.

Validation: Test, Analysis and Verification
Validation often boils down to testing in the traditional software engineering practice. Due to the very high requirements in the area of secure embedded systems, it is necessary to use a wider range of techniques and, most importantly, to justify their use and motivate their complementarity. First, testing itself has to be conducted in a systematic way. Trusted Logic's offer includes both security testing and functional testing. The first category is based on the potential vulnerabilities identified for the product and the second relies on its functional specification. Functional testing is supported by a tool, called TL-CAT, which provides different levels of automation (from the direct description of test suites in a high-level language to the automatic generation of test cases). The other validation techniques used by Trusted Logic are program analysis and program verification. Program analysers have been designed and developed by Trusted Logic to prove various properties of Java Card programs, from standard Java bytecode type correctness to specific security policies. Depending on the technical and economical context, such analysers can run either on the smart card itself, on hardware security modules, or on mundane workstations. The most ambitious verifications, which cannot be performed automatically by a program analyser, can be conducted within an interactive theorem prover. As an illustration, Trusted Logic has used Coq, the prover developed by Inria, to check the correctness of its byte code verifier and other key components of a Java Card virtual machine.

Conclusion: Innovation and Pragmatism
Trusted Logic's original market was the banking sector and smart card industry because this is where a strong need for secure embedded systems first appeared. This market is currently expanding to include terminal manufacturers, GSM, telecommunication operators, application providers etc, and Trusted Logic has become a leading actor in this area. Its reference list includes major players such as Visa, MasterCard, Schlumberger, Gemplus, Ingenico, France Telecom, Sun etc. We believe that the key factors for this success are the following:

1. Innovation: embedded systems have evolved extensively during the last decade and the rate of progress is not expected to slow in the next few years. One of the key technical factors here is the advent of open systems, especially through the rolling out of Java-based solutions. This facility introduces further challenges in terms of security and so far we have seen only a small number of the new possibilities offered by open systems. To meet these challenges, Trusted Logic devotes a substantial part of its manpower to innovation (as an illustration, most of the techniques sketched in this paper are patented and licensed) and this effort will continue to increase in the future.

2. Pragmatism: the first motto could be 'the use of the appropriate technique for the job'. The choice of a technique (method or tool) should ultimately be motivated by the risk analysis and by the identification of the key security components which warrant the strongest validation efforts (the top level being verification using a theorem prover). Another crucial issue is the compatibility with standards: as mentioned above, all the methodologies and tools described here are in line with the Common Criteria. This compatibility is of prime importance both from a business and a technical point of view; in particular, it makes it easier to factorise efforts and share a common body of knowledge and methods within the security community. Among the other standards which are at the core of Trusted Logic activities, we should mention the languages of the Java family (in particular Java Card), the GlobalPlatform services for secure card management and the emerging profiles for small terminal interoperability (STIP and MIDP).

In conclusion, we believe that it is necessary for Europe to foster new collaborative efforts between research centres and innovative companies on security for embedded systems. Trusted Logic already collaborates in different ways with several European research centres, including INRIA, and intends to reinforce and multiply these links in the future.

Link:
http://www.trusted-logic.fr/

Please contact:
Daniel Le Métayer,
Trusted Logic S.A., France
Tel: +33 1 30 97 25 14
E-mail: Daniel.Le_Metayer@trusted-logic.fr