|
|
|
|
Certification using formal methods responds to an increasing demand from the industry, on the one hand, because of the appearance of new norms that ask for formal methods when a certain level of security is required, on the other hand, because of the augmentation of the complexity of operating systems and embedded software.
Dyade is a joint venture between Bull and Inria for advanced research. Within the framework of Dyade, FormalCard is a project targeted at the application of formal methods and tools developed at INRIA to the design of Smart Cards developed by Bull.
The action FormalCard targets at producing an environment for formal specification, verification, and symbolic test generation for software applications embedded on smart cards. There are three sub-projects:
The aim is to give a formal description (syntax, static and dynamic semantics) of the language to be used to describe the applications. The language must satisfy several distinct criteria:
it must be simple and intuitive, to be usable even by software engineers unfamiliar with formal methods;
it must be expressive enough to allow a concise description of the operating systems and the smart card software;
it must be executable, to allow debugging, simulation, and verification by model checking;
its constructs must have a formal semantics to allow symbolic analysis and the use of proof techniques.
We base the design of this language on the standardization work done within ISO between 1992 and 2000 for the definition of the E-LOTOS language. A subset of the LOTOS NT language matching the needs of Bull developers and allowing to describe a (sequential) input/output automaton with guarded commands will be selected.
The aim is to specialize to the domain of smart cards some trusty techniques for enumerative verification and test generation. For this purpose we plan to reuse efficient tools that already exist, such as CADP for model-checking and TGV for test generation.
A compiler for the formal description language defined in the previous sub-project will be produced. It will generate C code in order to enable a connection with the Open/Caesar interface. This will allow to reuse the simulation and verification tools available in CADP in order to validate security properties of the embedded software. This will also allow to use the TGV tool for generating (non symbolic) conformance tests.
Enumerative test generation techniques suffer limitations due to combinatoric blow up. Moreover, the produced test cases are completely instantiated, unlike industrial practice, for instance the language TTCN [ISO standard 9646], in which test cases are ``real'' programs with variables and parameters.
Symbolic test generation explores a complementary way, which consists in producing test cases parameterized with variables. It relies on the ability to discover and use, in the specification of the system under test, relations between control and data. These relations (or invariants) are searched automatically using static analysis techniques.
We selected the IF toolset developed at the Verimag laboratory, which provides such static analysis algorithms. Other tools will be used, namely the PVS and ICS decision procedures from the Stanford Research Institute. The specification language defined above will be translated into IF's input formalism. The next steps will be to calculate a product of automata between the specification and the test purpose, then to compute closures, determinizations, and selections of the reachable part of the product that satisfy the test purpose.
Starting date: July 2000
Ending date: December 2001
Client within Bull: Bull Smart Cards and Terminals (also known as CP8)
INRIA hosting projects: Vasy (INRIA Rhône-Alpes), Pampa (INRIA Rennes)
Operational supervision: Sébastien Gelgon (Bull) [1999-June 2000], Nicolas Lasselin (Bull) [July 2000-October 2000], Jean-Michel Ravon (Bull) [since November 2000]
Scientific supervision: Hubert Garavel (INRIA Rhône-Alpes) and Vlad Rusu (INRIA Rennes)
Team Members:
| Duncan Clarke | Ingénieur Expert | INRIA Rennes |
| Hubert Garavel | Chargé de Recherche | INRIA Rhône-Alpes |
| Sébastien Gelgon | Ingénieur | Bull [1999-June 2000] |
| Thierry Jéron | Chargé de Recherche | INRIA Rennes |
| Frédéric Lang | Ingénieur Expert | INRIA Rhône-Alpes |
| Nicolas Lasselin | Ingénieur | Bull [July 2000-October 2000] |
| Jean-Michel Ravon | Ingénieur | Bull |
| Vlad Rusu | Chargé de Recherche | INRIA Rennes |
| Kafia Zemerli | Ingénieur | Bull |
| Massimo Zendri | Ingénieur | Bull [1999-April 2000] |
| Elena Zinovieva | Doctorante | INRIA Rennes |
In 1999, Hubert Garavel, Sébastien Gelgon, and Massimo Zendri performed a feasibility study: a simplified operating system embedded on a smart card (between the physical layer and the embedded applications running on the card) was selected as the target for the case study. This operating system was a significant example containing almost all the functionalities to execute several applications simultaneously, including a hierarchical filesystem and primitives for reading/writing files, authentication, software reset, etc.
This operating system was specified using both LOTOS (130 lines of code) and C (1700 lines). The LOTOS code defines an input/output automaton expressing the interactions between the operating system and its environment. The C code defines the data types, state variables, boolean guards, and computations of transitions between states (this approach allowed to reuse C code already developed by Bull).
Then, the CADP tool was used to establish several "good" properties: some of which were simple (e.g., absence of deadlocks) whilst others were more complex (e.g., the fact that a card cannot be authenticated without generating a random number). The TGV tool was also used to generate a collection of tests automatically.
Following this feasibility study, the Dyade/FormalCard action was officially launched in May 2000.
V. Rusu, L. du Bousquet, and T. Jéron.
An approach to symbolic test generation.
In 2nd International Conference on Integrated Formal Methods,
Schloss Dagstuhl (Germany), November 2000. LNCS 1945, pages 338-357.
Mihaela Sighireanu (revision by Frédéric Lang).
LOTOS NT User's Manual (Version 2.1).
November 2000, 105 pages.
D. Clarke, T. Jéron, V. Rusu, and E. Zinovieva.
Automated test and oracle generation for Smart-Card applications.
In International Conference on Research in Smart Cards (e-Smart'01), LNCS 2140, pp. 58-70, 2001.
D. Clarke, T. Jéron, V. Rusu, and E. Zinovieva.
STG: A tool for generating symbolic test programs and oracles from operational specifications.
In Joint 8th European Software Engineering Conference (ESEC) and 9th ACM SIGSOFT Symposium on the Foundations of Software Engineering (FSE-9), pp. 301-302, 2001.
H. Garavel, F. Lang, and R. Mateescu.
An Overview of CADP 2001.
INRIA Technical Report number RT-0254, 15 pages, December 2001.
D. Clarke, T. Jéron, V. Rusu, and E. Zinovieva.
STG: A Symbolic Test Generation tool.
In Tools and Algorithms for the Construction and Analysis of Systems (TACAS'02), LNCS 2280, 2002.
Hubert Garavel and Frédéric Lang.
NTIF: A General Symbolic Model for Communicating Sequential Processes with Data.
In 22nd IFIP WG 6.1 International Conference on Formal Techniques for Networked and Distributed Systems FORTE'2002 (Houston, Texas, USA), November 2002.
Rapport d'activité VASY 1999 (French) [PostScript or PDF file available]
Rapport d'activité Dyade/FormalCard 2000 (in French)
Rapport d'activité Dyade/FormalCard 2001 (in French)
The TRAIAN compiler Web Page
The E-LOTOS Web Page at INRIA Rhône-Alpes
Back to the VASY Home Page