Résumé du projet CASTLES:
Conception d'Analyses Statiques et
de Tests
pour le Logiciel Embarqué Sécurisé
INRIA Sophia-Antipolis AQL IRISA Oberthur
Proposition pour un projet RNTL exploratoire de 36 mois
Nature et durée du projet
Projet exploratoire d'une durée
de 36 mois.
Objectifs et positionnement par rapport à l'appel
L'objectif principal du projet est de définir un environnement
pour l'automatisation de la certification de la plateforme et des
applications JavaCard, et d''evaluer cet environnement dans le
contexte de la certification industrielle selon les Critères Communs.
Deux exigences majeures émergent dans cette perspective:
-
l'environnement doit fournir un niveau d'automatisation élevé
pour réduire les coûts liés à de telles certifications;
- l'environnement doit intégrer dans un cadre unifié les différents
aspects formels d'une certification: spécification de haut niveau,
preuves formelles, tests et implémentation.
Cet objectif s'inscrit dans le Thème 1 de l'appel: ``Concevoir des
logiciels enfouis, critiques ou temps réel pour les objets et les
systèmes'', et plus précisément aux mots clés 1.8 ``Modélisation,
vérification de comportement, validation'', 1.9 ``Transformations de
spécifications / programmes'' et 1.6 ``Processus, organisation,
sûreté de fonctionnement et métriques de développement logiciel''.
Les objectifs du projet sont en adéquation avec plusieurs priorités de
l'appel. En particulier les recherches proposées visent à faciliter,
dans un domaine où s'exprime une forte demande industrielle, la
validation de systèmes par:
-
le passage à l'échelle des méthodes formelles, en s'appuyant sur
des techniques modulaires de spécification, de vérification et d'analyses
statiques;
- l'intégration des différents aspects liés à la validation:
abstractions automatiques de spécifications, preuves formelles,
génération de tests, passage d'une spécification de haut niveau à une
mise en oeuvre logicielle.
Enjeux industriels et état de l'art
Les cartes à puce ouvertes offrent les garanties techniques
nécessaires à la généralisation du commerce électronique, et leur
utilisation accrue est largement soutenue par des initiatives
européennes (e-Europe SmartCards, etc) ou mondiales (JavaCard
Platform, Global Platform, etc). Néanmoins leur déploiement
massif est conditionné par la réalisation d'évaluations Critères
Communs à des niveaux élevés (EAL5-EAL7), afin de fournir les plus
hautes garanties de qualité pour les plateformes (implantées par les
industriels de la carte à puce), et les applettes (conçues par les
fournisseurs d'applications). Toutefois l'industrie de la carte à puce
souffre d'un manque aigu de techniques, d'outils et d'environnements
leur permettant une utilisation accrue des méthodes formelles:
-
il n'existe à ce jour aucun environnement automatisé qui
intègre tous les aspects d'une certification de la plateforme
JavaCard (notamment la vérification formelle et le test), et
qui soit accessible aux industriels de la carte à puce;
- la vérification formelle de la plateforme JavaCard
nécessite un effort très important, dû à l'absence dans
ce contexte de méthodes de vérification modulaires et
automatiques;
- la validation des applettes JavaCard repose sur des analyses
statiques complexes, qui doivent être justifiées au regard de la
certification. A notre connaissance, la vérification de bytecode
est la seule analyse statique ayant été vérifiée formellement.
Malgré l'importance de l'enjeu économique, il n'existe pas de projet
d'envergure sur ces problématiques qui requièrent des compétences en
développement et évaluation sécuritaire des logiciels pour les cartes
à puce, et en méthodes formelles (spécifications formelles, preuves,
tests, et analyses statiques).
Partenariat
Constitution du consortium
Le consortium est constitué de deux équipes de recherche, Everest
(INRIA Sophia-Antipolis, chef de file) et Lande (IRISA),
spécialisées dans l'application des méthodes formelles au code
mobile et embarqué, d'un industriel, Oberthur, ayant une position
forte sur le marché de la carte à puce, et d'une SSII, AQL, dont
le laboratoire de sécurité est agréé pour la conduite
d'évaluations Critères Communs.
Intérêt du partenariat
Le consortium est motivé par le développement de techniques et outils
pour la certification de logiciels pour la carte à puce. Les
partenaires ont une expertise reconnue et complémentaire dans les
domaines des machines virtuelles, des applications JavaCard, des
évaluations Critères Communs, des environnements de spécification et
de preuve, et des méthodes et outils d'analyse statique et de test.
Ainsi, le consortium dispose d'atouts importants pour concevoir un
environnement de certification pour JavaCard, et pour l'appliquer dans
un cadre industriel.
Mise en oeuvre
La mise en oeuvre de l'environnement s'appuie sur les travaux
antérieurs de l'INRIA Sophia-Antipolis, qui a conçu d'une part une
méthodologie de vérification de machines virtuelles qui repose sur
l'interprétation abstraite, et d'autre part un environnement de
spécification Jakarta qui permet la spécification de langages de bas
niveau, et la transformation automatique de ces spécifications par des
techniques d'abstraction. Cet environnement a été utilisé pour
valider un modèle simplifié de la plateforme JavaCard.
Le format restreint du langage de spécification de Jakarta JSL s'est
avéré déterminant dans l'automatisation des abstractions. La première
partie du projet a pour but d'exploiter le format restreint du JSL
pour le développement de techniques de spécification modulaires, puis
de génération automatique de tests et de preuves automatiques. Un
prototype intégrant ces techniques sera réalisé et utilisé dans un
contexte industriel pour (1) la spécification et vérification formelle
de la JCVM; (2) la validation par le test d'une machine virtuelle
embarquée fournie par Oberthur.
La seconde partie du projet a pour but de concevoir et de valider des
analyses pour la vérification de politiques de sécurité d'applications
JavaCard. Ces analyses s'attacheront à approximer le flot de données
des programmes et en garantiront des propriétés de confidentialité et
de disponibilité. Elles seront vérifiées formellement à l'aide
d'assistants à la preuve et instrumentées par des prototypes. Ces
prototypes seront évalués sur des cas d'étude fournis par Oberthur.
Ruptures technologiques
En concentrant ses efforts sur JavaCard, le consortium dispose d'un
cadre applicatif ciblé qui lui permettra de lever les verrous
technologiques suivants:
-
La mécanisation d'un processus de validation intégrant
spécification et vérification formelle, tests et génération
de code, et utilisable dans un contexte de certification;
- La conception et validation d'analyses statiques garantissant
des propriétés non-fonctionnelles et sécuritaires de programmes;
Retombées du projet et possibilités d'exploitation
L'environnement développé par le projet pourra être exploité par
Oberthur dans son processus de développement logiciel et dans le cadre
d'une certification Critères Communs. De plus, l'industrialisation et
la commercialisation d'un environnement de certification constituent
pour AQL des perspectives intéressantes si les résultats du projet
confirment l'intérêt industriel d'un tel environnement.
This document was translated from LATEX by
HEVEA.