The Dyade/FormalCard Action

Version 1.23 - Date 2021/02/07 09:27:46


1. Overview

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:

2. The Dyade/FormalCard Action

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:


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.

3. Publications

4. Related Links

See also the yearly activity reports of the VASY team, available from the Press Releases Page.

Back to the VASY Home Page