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 Logics success is a pragmatic approach based on the combination of two complementary ingredients:
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
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
Conclusion: Innovation and Pragmatism
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.