Rapport d'activité Dyade/FormalCard 2001

Sommaire

• Introduction
• Équipe
• Programme de travail
• Etat d'avancement

Introduction

Équipe

Programme de travail

La collaboration engagée en 1999 avec BULL SC&T (Smart Cards and Terminals), puis formalisée en juillet 2000 par le lancement de l'action FORMALCARD du GIE BULL-INRIA DYADE, s'est poursuivie en 2001 en dépit des changements liés au rachat de BULL SC&T par la société SCHLUMBERGER, à la fin du GIE DYADE et à l'arrêt du projet PAMPA (Rennes). Participent désormais à cette collaboration, à laquelle nous conservons le nom de FORMALCARD, les projets VASY et VERTECS de l'INRIA et la société SCHLUMBERGER.

FORMALCARD vise à réaliser des outils formels pour le développement des logiciels embarqués sur cartes à puces en vue de permettre leur certification. Cette certification répond à une demande croissante dans l'industrie, en raison de l'apparition de nouvelles normes (critères communs) qui préconisent, à partir d'un certain niveau de sécurité, l'utilisation de méthodes formelles. FORMALCARD comporte trois objectifs dont les deux premiers sont pris en charge par le projet VASY, le troisième étant confié au projet VERTECS :

• Conception d'un langage pour la spécification formelle d'applications pour cartes à puces

  En se basant sur l'expérience acquise par VASY au cours de la normalisation du langage E-LOTOS, il s'agit de définir un langage (sous-ensemble du langage LOTOS NT) satisfaisant plusieurs critères :

  • Il doit être simple et intuitif pour pouvoir être utilisé par des ingénieurs qui ne sont pas nécessairement familiers avec les méthodes formelles.
  • Il doit être suffisamment expressif pour permettre une description concise du système d'exploitation et des applications embarquées sur cartes à puces.
  • Il doit être exécutable pour permettre le déboguage, la simulation et la vérification énumérative (model checking).
  • Il doit avoir une sémantique formelle pour permettre l'analyse symbolique et l'utilisation de techniques de preuve.

• Vérification et génération de tests par des méthodes énumératives

  On cherche à spécialiser au domaine de la carte à puce certaines techniques bien établies pour lesquelles nous disposons d'outils efficaces. L'objectif est de réaliser, pour le langage de description formelle mentionné ci-dessus, un compilateur produisant du code C compatible avec l'interface OPEN/CAESAR. Ceci devrait permettre de réutiliser les outils de simulation et de vérification disponibles dans CADP pour valider les propriétés de sécurité des applications embarquées et d'utiliser l'outil TGV pour générer des tests (non symboliques) de conformité.

• Génération de tests symboliques

  Les techniques énumératives de génération de tests ont des limites inhérentes, dues à l'explosion combinatoire. De plus, les tests produits sont complètement instanciés, contrairement à la pratique industrielle qui veut que les cas de test soient de ``vrais'' programmes avec variables et paramètres. L'objectif est de proposer des méthodes de génération de test symboliques qui évitent ces inconvénients et de démontrer l'applicabilité de ces méthodes sur des études de cas industrielles.

État d'avancement

Les applications embarquées sur cartes à puces pouvant être représentées sous forme d'automates étendus avec des variables, nos travaux se sont donc focalisés sur les processus séquentiels présents dans les langages E-LOTOS et LOTOS NT. Pour les modéliser, nous avons conçu un formalisme appelé NTIF (New Technology Intermediate Form) destiné à servir de langage intermédiaire dans la compilation des processus E-LOTOS et LOTOS NT.

Dans son principe, NTIF permet de spécifier des automates définis par un ensemble d'états et de transitions et paramétrés par des variables d'état typées. A chaque transition sont attachés une action (permettant la communication avec l'environnement selon la sémantique du rendez-vous propre aux algèbres de processus) ainsi qu'un fragment de code séquentiel permettant de consulter et/ou de modifier la valeur des variables d'états ; ce fragment de code est exprimé avec les structures de contrôle usuelles des langages algorithmiques et fonctionnels.

Nous avons défini la syntaxe et la sémantique du langage NTIF, puis montré que NTIF était suffisamment expressif pour généraliser un grand nombre de formalismes pré-existants pour la spécification des automates étendus.

Nous avons ensuite conçu deux logiciels (appelés NT2IF et NT2DOT) pour traiter les descriptions NTIF modélisant des applications embarquées sur cartes à puces. Développés à l'aide du générateur de compilateurs SYNTAX et du compilateur TRAIAN, ces deux logiciels (6500 lignes de code) ont en commun les analyseurs lexicaux et syntaxiques, ainsi que les différentes phases de construction, de vérification et de transformation d'arbres abstraits. Leurs fonctionnalités sont les suivantes :

• NT2IF traduit les descriptions NTIF vers un formalisme de plus bas niveau, le modèle IOSTS (Input Output Symbolic Transition Systems), qui est utilisé en entrée du générateur de tests symboliques STG développé par le projet VERTECS. Le modèle IOSTS - qui, concrètement, est représenté à l'aide du formalisme IF développé au laboratoire VERIMAG - permet de décrire des automates étendus, dont chaque transition est étiquetée par une condition de franchissement portant sur la valeur des variables d'état, suivie d'une action de communication, d'une modification de l'état global par affectation des variables d'états, et enfin d'un branchement vers l'état suivant. La traduction s'effectue par ``dépliage symbolique'', en décomposant les transitions NTIF en transitions IF plus élémentaires.

  Grâce à l'existence du traducteur NT2IF, NTIF s'est rapidement imposé comme le langage d'entrée approprié pour l'utilisation de l'outil STG en milieu industriel. En effet, NTIF pallie les principales limitations du modèle IOSTS/IF : il possède des structures de contrôle évoluées (instructions ``case'', ``if-then-else'', ``while'', etc.) dont l'absence en IOSTS/IF oblige l'utilisateur à introduire de nombreux états et transitions intermédiaires, ainsi qu'à dupliquer de nombreuses conditions booléennes, ce qui constitue une source d'erreurs fréquentes. De plus, NTIF possède une sémantique plus intuitive, plus facile à apprendre, car très proche de la sémantique des langages algorithmiques.

• NT2DOT permet de visualiser sous forme graphique les descriptions NTIF en les traduisant vers le format DOT utilisé par les outils graphiques GRAPHVIZ développés par AT&T.

  Bien que l'outil STG dispose également de fonctionnalités de visualisation pour les modèles IOSTS/IF, l'expérience a démontré que les graphiques produits par NT2DOT étaient plus lisibles, car mieux structurés et de plus petite taille. Ce résultat s'explique par le fait que, d'une part, les modèles NTIF comportent moins d'états et de transitions que leurs équivalents IOSTS/IF, et que, d'autre part, STG attache les fragments de code séquentiels aux transitions du diagramme, alors que NT2DOT regroupe ces fragments sous une forme structurée à l'intérieur des états. Cette comparaison graphique a confirmé l'intérêt d'inclure des structures de contrôle évoluées en NTIF.

• Nous avons traduit en NTIF une spécification de porte-monnaie électronique multi-devises (EMV Common Electronic Purse Standard version 2.2 5-2000) à partir de la formalisation en IOSTS/IF (1140 lignes de code) qu'en avait faite Duncan Clarke (projet VERTECS). Cette expérience a permis de convaincre nos partenaires des qualités du langage NTIF : la description NTIF est beaucoup plus claire, plus concise (56% d'états et 50% de transitions en moins) et plus fiable (plusieurs erreurs ont été découvertes au cours de la traduction en NTIF). La description NTIF a ensuite été traduite en IOSTS/IF grâce à l'outil NT2IF, ce qui nous a permis d'améliorer notre traducteur et de détecter des erreurs résiduelles dans l'outil STG.
• François-Xavier Ponscarme (stagiaire SCHLUMBERGER) a décrit en NTIF les commandes administratives d'un système d'exploitation destiné aux cartes à puces pour la téléphonie mobile 3GPP (3rd Generation Partnership Project). Cette description NTIF (910 lignes de code), reprise et complétée par Elena Zinovieva (projet VERTECS), a été traduite en IOSTS/IF à l'aide de l'outil NT2IF (38% d'états et 56% de transitions en plus). Des tests symboliques ont été produits automatiquement par l'outil STG.

Back to the VASY Home Page