ANNEXE TECHNIQUE DU PROJET CAT
C Analysis Toolbox
Analyse de programmes C critiques embarqués
Les activités de vérification et de maintenance corrective ou évolutive représentent une part considérable du coût total de développement des logiciels. L'évolution croissante du nombre de fonctionnalités et de la complexité des applications et des systèmes tend à augmenter la part dédiée à ces activités. Les coûts engagés sont plus importants encore lorsque les logiciels sont critiques et doivent être certifiés auprès des autorités compétentes.
L'objectif de ce projet est de développer une boîte à outils d'analyse de codes C de taille industrielle et comportant une dimension de criticité tels que les applications embarquées dans le domaine de l'aéronautique et de l'automobile. Tout au long du cycle de développement du logiciel, cette boîte à outils d'analyse permettra :
de disposer de fonctionnalités de compréhension du code, pour améliorer sa réutilisabilité et déterminer l'impact de modifications, par application de techniques d'extraction de flots de contrôle et de flots de données,
de garantir des propriétés fonctionnelles (notamment de type sûreté de fonctionnement, en vue de la certification de logiciel critique) et de robustesse (détection d'erreurs potentielles à l'exécution telles que la division par zéro, le débordement de tableau, ...).
C'est en regard de considérations largement connues, relatives aux méthodes classiques d'analyse de code, que le projet CAT a pour objectif :
de délivrer des outils et méthodes innovants diminuant les coûts (d'investissement, d'espace mémoire, de temps d'exécution, ....) souvent jugés prohibitifs,
d'offrir aux utilisateurs les moyens de combiner différentes stratégies d'analyse, pour parvenir à établir la preuve de propriétés, synthétiser des propriétés ou évaluer l'impact d'une modification sur des applications de taille industrielle, par l'interaction de différentes techniques d'analyse.
Une méthodologie d'utilisation des techniques et outils développés, suivie d'une expérimentation sur des cas industriels réels ou suffisamment représentatifs, permettra d'assurer la viabilité de la mise en œuvre de la boîte à outils.
Les fonctionnalités génériques de cette boîte à outils seront mises à disposition sous forme de logiciel libre. Les outils complémentaires dénommés greffons dans la suite de ce document seront distribués suivant des modalités définies par leurs concepteurs. Ces greffons implanteront les principales techniques d'analyse de code et de vérification de propriétés : interprétation abstraite, preuve automatique, réduction de code, preuve de programme suivant la logique de Hoare. Ces greffons sauront coopérer à l'obtention de propriétés grâce à l'utilisation d'un langage commun et se combiner suivant des stratégies pilotées par l'utilisateur. Pour assurer la pluridisciplinarité nécessaire à cet objectif, des équipes de recherche aux vocations et compétences complémentaires participeront aux sous-projets concernés.
L'orientation du projet est
clairement exploratoire sur un certain nombre de sujets applicatifs
et de recherche (réduction de code, coopération entre
prouveurs de théorèmes, combinaison de techniques de
vérification, ...). Concernant d'autres domaines, tels que
l'analyse statique, la preuve automatique ou la résolution de
contrainte, la démarche consistera à intégrer au
projet les outils et méthodes existants.
Logique de déroulement du projet :
Un état de l'art des méthodes et outils issus de la recherche et des pratiques industrielles (revue manuelle de code, génération automatique de tests, analyse statique, ...) constituera le point de départ de l'expression des besoins en matière d'analyse de programmes. Cet état de l'art mettra l'accent sur les limitations précises que rencontrent les utilisateurs industriels dans leur mise en œuvre.
Dès le début du projet, un langage commun de spécification constituera pour l'essentiel le moyen d'interface et de communication entre l'utilisateur et la boîte à outils, et entre les différents outils développés. Des évolutions de ce langage seront à prévoir au cours du déroulement du projet afin de prendre en compte les spécificités propres aux méthodes et outils implémentés. Ce langage aura vocation à jouer un rôle similaire au Java Modeling Language (JML : un langage de spécification de comportements, de « design by contract » et de « model based specification » ) mais pour le C.
Après la mise au point d'un ensemble de fonctionnalités génériques, nous développerons un ensemble de greffons offrant les techniques traditionnelles d'analyse de code et capables de communiquer entre eux à l'aide du langage de spécification.
Une méthodologie de vérification, dont les prémisses auront été abordées durant la phase d'expression des besoins, sera consolidée en fin de projet. Cette méthodologie et la boîte à outils d'analyse seront dûment validées par un ensemble d'expérimentations et d'évaluations concrètes sur la base de cas réels fournis par les industriels participant au projet. Compte tenu des objectifs visés par le projet CAT, l'obtention de l'adhésion des industriels aux méthodes et outils développés, et leur compatibilité avec les processus existants de développement de logiciels critiques sont des impératifs. Ces évaluations permettront de valider l'ensemble des résultats du projet.
Également évoqués durant l'expression des besoins sous la forme de préconisations, les objectifs de qualification de tout ou partie des éléments de la boîte à outils seront abordés dans le cadre d'un sous-projet à part entière. Obtenir cette qualification des outils d'analyse s'inscrit dans la démarche de certification des logiciels critiques. Il est donc essentiel d'identifier les besoins et ressources et d'établir la démarche nécessaire à cette qualification, dans le cadre de ce projet.
Domaine concerné : vérification des systèmes embarqués critiques
Les mots clés sont : vérification, preuve, systèmes critiques embarqués, automobile, aéronautique, télécommunications, programmes C, interprétation abstraite, logique de Hoare, contraintes, spécialisation de code, méthodes formelles
2-1) État de l'art et intérêt du projet
Il existe aujourd'hui une offre importante en termes d'outils de vérification de code C. On peut distinguer au moins quatre types de technologies sous-jacentes à ces outils.
Outils à base d'interprétation abstraite
La société Polyspace Technologies http://www.polyspace.com propose par exemple un outil d'analyse statique très largement déployé qui utilise des techniques d'interprétation abstraite avancées. Cet outil est complètement automatique et produit des rapports permettant de savoir pour chaque instruction dans le code si elle est susceptible de causer une erreur à l'exécution de façon certaine, de façon possible ou jamais. De plus l'instruction ayant causé cette erreur peut être localisée dans le code original. La principale limitation de cet outil est l'absence d'interactivité avec l'utilisateur. L'outil est considéré comme “presse-bouton”. Il devient donc difficile d'éliminer un certain nombre de fausses alertes pointées par l'outil du fait des approximations qu'il doit faire. Afin de lever en partie les limitations liées à ces fausses alertes, des techniques d'interprétation abstraite sophistiquées ont été développées pour traiter des programmes typiques de l'aéronautique (contrôle-commande) au sein du projet RNTL Astrée http://www.astree.ens.fr. Le succès, tant en terme de précision des résultats qu'en terme de performances, de l'outil développé dans ce projet montre qu'il est fondamental de pouvoir décliner un analyseur abstrait en fonction du domaine d'application. Astrée a pour unique objectif de détecter les erreurs à l'exécution. Pourtant il restera toujours des propriétés qui ne pourront être déduites automatiquement. De plus le diagnostic, quand il est imprécis, ne suffit pas à retrouver la cause de l'erreur : par exemple, si une certaine instruction calcule une division par une variable que l'outil ne parvient pas à estimer assez précisément pour éliminer « zéro » des valeurs possibles, il sera impossible de localiser automatiquement la section du code original à l'origine de cette valeur « zéro » . Ce type de limitation peut être étudié selon deux axes :
avec des outils de preuve de propriétés à base de logique de Hoare, on peut déterminer sous quelles conditions cette valeur peut-être nulle,
avec des outils de spécialisation, on peut trouver d'où vient la valeur zéro potentielle.
Outils à base de logique de Hoare
L'outil Caduceus http://caduceus.lri.fr est un outil de preuve de programme C. Il est fondé sur la logique de Hoare. Il possède un langage de propriété riche et permet d'invoquer des prouveurs externes interactifs ou automatiques. Par contre, il ne traite qu'un sous-ensemble du langage C afin de pouvoir interpréter les programmes C dans un modèle mémoire d'assez haut niveau. Son utilisation nécessite l'écriture d'une spécification précise de l'ensemble du programme : en effet la méthode de Hoare souffre de la nécessité de fournir des invariants de boucle et des spécifications pour toutes les fonctions appelées. L'utilisation de l'interprétation abstraite doit permettre de réduire les interventions de l'utilisateur. C'est la raison pour laquelle l'outil Caveat http://www-list.cea.fr/fr/programmes/sys_embarques/labo_lsl/caveat/index.html combine des techniques d'interprétation abstraite très élémentaires et un calcul à la Hoare afin de donner à l'utilisateur un outil de vérification interactif. L'interprétation abstraite est utilisée pour synthétiser automatiquement la liste des variables modifiées, les dépendances fonctionnelles entre les données, des invariants de boucles et l'ensemble des erreurs d'exécution potentielles. Ces propriétés sont alors utilisables par les méthodes de preuves de l'outil. Si les analyses abstraites se sont révélées trop imprécises, il n'est pas possible de les raffiner. De plus, seul un fragment du C est traité, en particulier on interdit la présence d'alias entre des pointeurs. Ces restrictions ne permettent pas de traiter des programmes embarqués complexes.
Outils à base modèle
Dans des domaines d'application particuliers, une autre technique peut porter ses fruits : l'extraction et la vérification de modèle. Le projet Blast http://www-cad.eecs.berkeley.edu/~rupak/blast/ utilise des méthodes de vérification de modèle afin d'établir qu'un logiciel respecte un certain nombre de contraintes imposées par les bibliothèques qu'il utilise. Cet outil automatique fournit des traces permettant d'exhiber des façons de violer ces contraintes. Les contraintes des bibliothèques sont spécifiées sous forme de motifs à reconnaître dans le code C. Cette méthode permet d'imposer des règles strictes de codage, mais risque de donner des fausses alarmes si les propriétés sont garanties par des constructions difficiles à reconnaître à l'aide d'un filtre. Le projet SLAM http://www.research.microsoft.com/slam/ montre comment ces techniques peuvent s'appliquer avec succès sur les pilotes de matériels. Ces derniers sont en effet très contraints dans leur interaction avec le système d'exploitation. Ces méthodes conviennent donc parfaitement pour ce type d'application.
Outils à base de flot de données
Il existe des outils qui, en utilisant des analyses de type flot de données, donnent des résultats intéressants. Le projet CCured http://manju.cs.berkeley.edu/ccured/ fournit un outil qui transforme un source C en un autre source C dans lequel à chaque fois que l'outil ne sait pas garantir qu'une opération est légale, il met une assertion. Le source produit se trouve instrumenté de façon importante et ne peut donc plus être embarqué. De plus cette technique ne permet pas de résoudre les problèmes potentiels détectés. La société Coverity http://www.coverity.com commercialise un outil qui permet de détecter statiquement la présence d'erreurs d'exécution et de violation de règles de codage, mais ne permet pas de spécifier et vérifier des propriétés arbitraires.
L'ensemble de ces techniques est confronté au problème du passage à l'échelle sur les grands programmes. Cependant, il existe des méthodes pour réduire la taille des codes et les simplifier, fondées sur les techniques de spécialisation (slicing).
Outils de spécialisation
La société Grammatech http://www.grammatech.com/ commercialise l'outil CodeSurfer qui permet de réaliser des analyses et de la visualisation assistée de code source C. En particulier, il fournit des analyses de flots de données et de contrôle dont la visualisation assistée est une forme de spécialisation de logiciel. Ces analyses ne sont pas utilisables par des outils de preuve et ne sont pas très précises. Par exemple l'analyse des pointeurs se fait hors contexte et hors flot de contrôle. C'est très insuffisant pour procéder à l'analyse de codes C embarqués, mais cela montre l'intérêt de cette approche pour étudier l'impact d'une modification d'une ligne de code.
Au delà des limitations propres à chaque système existant, il n'existe pas d'intégration entre ces systèmes alors que de toute évidence cette coopération est pertinente. C'est précisément l'objectif de ce projet : permettre une interaction et une inter-opérabilité entre les techniques existantes. Nous nous proposons ainsi d'intégrer des analyses par interprétation abstraite et des analyses interactives qui communiqueront leurs résultats dans un langage de propriété commun : les propriétés seront alors centralisées dans un noyau générique qui sera chargé de stocker toutes les propriétés et de fournir un accès abstrait aux codes sources. Ces propriétés seront prouvées en utilisant une combinaison des prouveurs disponibles sur le marché puisqu'un prouveur individuel ne peut être efficace sur toutes les propriétés. Afin de pouvoir modulariser la vérification, nous intégrerons un spécialiseur de code qui utilisera les propriétés stockées dans le noyau et nous proposerons une méthodologie garantissant la cohérence de l'ensemble des vérifications faites sur les codes spécialisés. En combinant les différents prouveurs existants, nous obtiendrons un meilleur taux d'automatisation des preuves, et nous offrirons aussi une passerelle entre les prouveurs interactifs et automatiques. Le projet prendra en compte un sous-ensemble du C réaliste, et en particulier devra pouvoir traiter le cas des programmes qui utilisent des propriétés de la plate-forme d'exécution et de la chaîne de compilation : c'est très fréquemment le cas des programmes embarqués étant donné leur spécificité et les contraintes d'optimisation auxquelles ils sont soumis.
Les partenaires académiques possèdent toutes les compétences pour relever les défis de la vérification : de l'interprétation abstraite à la preuve automatique en passant par l'extraction de modèle et l'analyse de flots de données.
CEA : Le Laboratoire pour la Sûreté du Logiciel (http://www-list.cea.fr/fr/programmes/sys_embarques/labo_lsl/index.html) est un acteur majeur dans le monde la vérification. Son activité est centrée autour de la production de prototypes et d'outils dans le but de les transférer à l'industrie. Sa double compétence en analyse statique (interprétation abstraite, preuve, analyse de flots) et en analyse dynamique (génération de tests, simulation) lui a permis d'acquérir une solide culture dans le domaine de la sûreté du logiciel. Nous disposons à ce jour d'un outil de preuve de programmes C (Caveat) combinant faiblement interprétation abstraite et preuve à la Hoare, d'analyse de programmes manipulant des flottants (Fluctuat, CEP) pour évaluer la précision en utilisant l'interprétation abstraite, de synthèse de modèles pour des programmes (Miel) et d'interprétation de modèles (Alcool). Ces outils sont déployés chez des acteurs majeurs du logiciel critique (Airbus France, EDF, IRSN, ...) avec qui nous avons des relations pérennes.
INRIA PROVAL : La création de l'équipe de recherche PROVAL de l'INRIA Futurs est la concrétisation récente d'une activité, née en 2001, de ses membres autour de la preuve de programmes impératifs. L'équipe PROVAL développe des outils de vérification de programmes Java et C, selon une méthodologie originale consistant à traduire ces programmes vers un langage intermédiaire unique adapté au calcul de plus faibles préconditions. Le programme intermédiaire est alors passé à un troisième outil spécialisé dans la génération des obligations de preuve. Celles-ci peuvent être produites pour un grand nombre d'outils de preuve formelle existants, tant interactifs (Coq, PVS, Isabelle/HOL, HOL4, HOL Light, Mizar) qu'automatiques (Simplify, CVC Lite, haRVey). Les langages de spécification utilisés sont, d'une part JML (Java Modeling Language) pour Java, et d'autre part un langage conçu dans l'équipe PROVAL pour le C. L'originalité de l'approche réside dans une modélisation de la mémoire qui est spécifiquement conçue dans le but de faciliter les preuves. Les outils associés, Krakatoa pour Java et Caduceus pour le C, sont distribués sous licence open-source aux adresses http://krakatoa.lri.fr/ et http://caduceus.lri.fr/.
IRISA
LANDE : Le thème de recherche central du projet Lande est la
conception d'outils d'aide au développement et à la
validation de logiciels. Notre approche est fondée sur une
collection de méthodes formelles permettant de spécifier
ou d'extraire des propriétés de programmes impératifs
par des techniques d'analyse statique ou dynamique précises.
Habituellement, nous nous appuyons sur des techniques de résolution
de contraintes symboliques ou numériques pour produire les
résultats d’une analyse. Plusieurs outils qui
supportent cette approche ont été développés
dans le projet parmi lesquels Reqs, un solveur de système
d'équations récursives utilisées dans les
analyses statiques (www.irisa.fr/lande/reqs),
FPSE un outil d’exécution symbolique pour programmes C
manipulant des nombres flottants (http://lifc.univ-fcomte.fr/~v3f)
ainsi qu’une extension du logiciel INKA pour le traitement des
pointeurs C vers des zones nommées de la mémoire.
Lande
est un projet commun avec le CNRS, l'université de Rennes 1
et l'Insa de Rennes.
2-2) Innovation technologique et recherche développées pour le projet
Enjeux scientifiques
L'outil Caduceus met en œuvre une modélisation très poussée des programmes avec pointeurs et sait bien gérer les alias potentiels : il met en œuvre des nouveautés scientifiques récentes sur la modélisation des programmes avec pointeurs [R. Bornat, Proving pointer programs in Hoare logic, In Mathematics of Program Construction, pages 102--126, 2000] [J.-C. Filliâtre et C. Marché, Multi-prover verification of C programs, In Sixth International Conference on Formal Engineering Methods, volume 3308 of Lecture Notes in Computer Science, pages 15--29, Seattle, WA, USA, Nov. 2004] [Thierry Hubert et Claude Marché, A case study of C source code verification : the Schorr-Waite algorithm, In 3rd IEEE International Conference on Software Engineering and Formal Methods (SEFM'05), Koblenz, Germany, September 2005] mais il demande l'ajout manuel de beaucoup d'annotations de code. Par contre, l'outil Caveat est capable d'inférer beaucoup de propriétés des programmes mais gère mal les pointeurs. L'enjeu scientifique général est de combiner les différentes approches actuellement utilisées par les partenaires.
De manière générale, l'analyse formelle d'un programme nécessite trois composants : au centre, une modélisation de l'exécution des programmes dans le langage considéré (en l'occurrence le langage C), en amont un langage de propriétés dans lequel on exprime les propriétés voulues et les propriétés intrinsèques pour le programme étudié, et en aval une ou plusieurs méthodes de preuves qui établissent, avec la modélisation choisie, la validité du programme vis-à-vis de ces propriétés. Des enjeux scientifiques existent au sein de ces trois composants, ainsi que dans leurs interactions :
Adapter la modélisation
Il s'agit de pouvoir adapter la modélisation en fonction du niveau d'abstraction du programme. Un programme de très bas niveau, qui travaille au niveau des bits, a besoin d'une modélisation elle-même de bas niveau, qui sera même dépendante de l'architecture sur laquelle l'exécution se fera. Sur des programmes de taille conséquente, on a pu déjà constater des problèmes de passage à l'échelle, montrant qu'il y a un fort besoin de raffiner la modélisation, en particulier de modéliser la mémoire par blocs, selon une analyse de régions d'aliasing préalable, en s'inspirant de techniques classiques d'analyse statique [J.C. Reynolds, Separation logic: a logic for shared mutable data structures, In 17h Annual IEEE Symposium on Logic in Computer Science, 2002].
Générer automatiquement des propriétés
Les vérifications en aval nécessitent en général de nombreuses insertions de propriétés dans le code, comme cela a été constaté sur un programme embarqué de Dassault Aviation. Sur des programmes de grandes tailles, ajouter manuellement ces propriétés devient très difficile, il faudrait être capable de les générer automatiquement dans la mesure du possible. Comme décrit dans l'état de l'art, l'outil Caveat utilise des techniques d'interprétation abstraite pour synthétiser des informations pouvant servir à produire de telles annotations. Notre but est donc de mettre en place un formalisme clair pour cette génération d'annotations. Les techniques utilisées dans l'outil Astrée pourront être également reprises et adaptées dans notre cadre.
Opérer les vérifications avec le plus d'automatisation possible
Les vérifications en aval peuvent être effectuées a priori avec ou sans aide de l'utilisateur. Les méthodes automatiques de vérification ont l'inconvénient d'être incomplètes, donc de générer des fausses alarmes. Par contre, les méthodes assistées sont évidemment rapidement très lourdes pour des gros programmes. L'enjeu est donc de faire coopérer le mieux possible les deux approches, en particulier nous souhaitons mettre en place l'utilisation en parallèle de multiples outils de preuve
Aider à la mise au point des spécifications
Dans le cas où une vérification échoue, il ne s'agit pas nécessairement d'une erreur du programme, mais plutôt d'une incomplétude des spécifications. L'enjeu est donc de boucler le cycle pour faire remonter les échecs de vérification au niveau de la spécification.
Extension des langages de spécifications
Le langage de spécification de l'outil Caduceus pour les programmes C aurait besoin d'être étendu pour permettre d'exprimer les propriétés de sûretés recherchées dans les applications industrielles. De plus il existe un véritable enjeu dans la mise au point d'un langage de spécification général pour le C. En effet contrairement au langage Java, l'architecture cible et la chaîne de compilation possèdent des propriétés dont une spécification de programme ne peut que rarement faire abstraction.
La résolution de ces enjeux devra se concrétiser dans une plate-forme intégrant l'ensemble des outils, en amont (spécifications), au centre (génération des obligations de preuve) comme en aval (outils de preuve).
Innovations technologiques
L'ensemble
du projet sera développé autour d'une infrastructure
générique à greffons innovante. Développée
en OCaml http://www.ocaml.org en
utilisant comme base une bibliothèque d'analyse du C
existante librement mise à disposition par l'université
de Berkeley : CIL (C Intermediate Language).
CIL propose une représentation de haut niveau de programmes
C, sous la forme d'un sous-ensemble du langage C, très
structurée, sans ambiguïté ni redondance, ainsi
qu'un ensemble d'outils permettant l'analyse et la transformation de
"code source" vers "code source". Notre
infrastructure offrira des services essentiels en proposant en
particulier un système permettant de développer
facilement des extensions spécialisées appelées
greffons. Cette infrastructure qui sera distribuée sous forme
de Logiciel Libre offrira un langage logique de spécification
pour le C inspiré de JML. Les propriétés du
programme analysé seront centralisées dans cette
partie générique dans une structure de type base de
données. L'architecture à greffons permettra des modes
de distribution différents suivant les pratiques courantes
des partenaires. De plus, le langage de spécification
permettra à des outils d'analyse de C indépendants du
projet CAT d'offrir une certaine inter-opérabilité
avec notre boîte à outils.
Il existe un défi technologique et théorique dans la mise en relation d'analyses de natures différentes. La mise au point d'un langage de propriétés permettra d'utiliser pendant une analyse donnée les résultats d'une autre analyse : chacune pourra traduire les propriétés de la base dans son formalisme propre si cela est possible. Par exemple un résultat issu d'une analyse d'intervalle pourra être utilisé dans une analyse utilisant des octogones. Certaines analyses automatiques qui procèdent par sur-approximation pourraient bénéficier d'une annotation manuelle du code, annotation qui serait ensuite à vérifier à l'aide d'une combinaison des techniques de preuve interactive et automatique. L'ensemble des analyses devra donc pouvoir être interrompu et repris après l'intégration d'informations provenant de sources externes (utilisateur ou autre analyse).
Une innovation technologique majeure du projet CAT est la mise au point d'une méthodologie de vérification globale qui en procédant à des sous-analyses et en composant les résultats permet de déduire des propriétés générales des logiciels. Les sous-analyses pourront être effectuées sur des versions spécialisées du code original selon des critères sémantiques à l'aide de techniques de spécialisation de code (slicing). La maîtrise de ces spécialisations permettra de comprendre quelles sont les propriétés qui seront vérifiées par construction sur le code original. Par exemple, on pourra étudier l'ensemble d'un système en le forçant à n'être que dans un mode particulier, puis en étudiant successivement chaque mode possible, on en déduira des propriétés globales du système et des propriétés spécifiques à chaque mode. C'est exactement la transposition des méthodes de preuve par cas.
Le marché visé est celui des acteurs du développement, de la maintenance corrective ou évolutive et de la validation des codes embarqués écrits dans le langage C. Historiquement, on observe une évolution des codes embarqués critiques : leur taille a considérablement augmenté pour atteindre quelques centaines de milliers de lignes de codes et la complexité du code lui-même a augmenté aussi. Les premiers codes embarqués étaient de simples boucles sans fin ne manipulant pas de pointeurs. Progressivement, des pointeurs ont été introduits pour aboutir aujourd'hui à des codes utilisant de nombreux pointeurs et exécutant de multiples tâches en parallèle de façon synchrone ou asynchrone : ce sont des codes complets de systèmes d'exploitation modernes qui doivent maintenant être analysés. Les outils d'aide à la compréhension ou à la recherche d'erreurs ont toujours eu un impact fort sur les acteurs du marché. Les dévermineurs (debugger) sont aujourd'hui livrés en standard avec les compilateurs et possèdent des possibilités d'interaction très évoluées. Les compilateurs eux-mêmes garantissent de plus en plus que les codes respectent certaines normes. Quand les premiers outils d'analyse statique indépendants des compilateurs ont été introduits sur le marché, le succès en terme de pénétration du marché a été incontestable. La société Polyspace en est un exemple tout-à-fait représentatif. Nous pouvons segmenter ce marché suivant le type d'activité de analyse qui est mené :
Réutilisation de composants : la vérification qu'un composant logiciel est utilisé en respectant ses spécifications est un problème d'ingénierie logicielle récurrent. De plus, les codes génériques peuvent avoir besoin d'être spécialisés pour des raisons de performance ou de sécurité (élimination de code mort dans le contexte d'une réutilisation par exemple).
Mise au point en développement : la vérification au plus tôt dans le cycle de développement permet de résoudre des problèmes à moindre coût. C'est ce type d'activité qu'Airbus France mène en utilisant les techniques de preuves en lieu et place des techniques de test unitaire.
Vérification a posteriori : les sociétés qui sous-traitent les développements ont un besoin crucial de vérification. Par exemple, EDF recherche à l'aide des techniques d'analyse statique à trouver des erreurs susceptibles de se produire à l'exécution. Une autre cible pour ce type d'analyse est les experts techniques qui doivent émettre des avis sur des logiciels avant leur mise en service : l'IRSN pour le nucléaire et le CEAT pour l'aéronautique.
Analyse de sûreté : la tolérance aux fautes et plus généralement la sensibilité au contexte sont des propriétés qui sont au cœur des préoccupation des industriels. Tous les grands groupes d'aéronautique, les constructeurs et les équipementiers automobiles cherchent à établir des propriétés de sûreté. Certains ont à constituer des dossier à présenter à une autorité (nucléaire, aéronautique,...). Cette dernière va pousser plus loin les analyses pour essayer de mettre en défaut les démonstrations.
Sécurisation : la sécurité des systèmes embarqués est devenue critique. Les cartes à puces de troisième génération et les terminaux de lecture de ces cartes sont susceptibles d'être attaqués par des utilisateurs malveillants. Les techniques d'analyse statique permettent d'étudier ces propriétés. Le marché est ici celui des fabriquants de systèmes sécurisés (France Télécom, Trusted-Logic, RATP) et des experts de certification comme le CESTI pour les cartes à puces.
Maintenance, évolution : tous les développeurs de systèmes sont confrontés aux problèmes de maintenance et d'évolution de leur logiciels. Cela représente même une part largement prépondérante dans la vie d'un logiciel et contribue de façon importante à son coûts. Un outil fournissant une aide dans ces tâches est susceptible d'une dissémination rapide.
Notre projet se place clairement sur l'ensemble de ces segments en apportant une réponse tant en terme d'infrastructure logicielle que d'outils et de méthodologies.
Les partenaires industriels impliqués directement dans le projet CAT ont tous une pratique importante des outils existants et un connaissance du tissu industriel concerné.
AIRBUS FRANCE est un des acteurs industriels majeurs dans le secteur de l'aéronautique. Son expertise dans les domaines techniques touchant à son secteur d'activité est largement reconnue. Cela est dû notamment à son engagement et aux efforts soutenus en matière de recherche et développement. La sûreté de fonctionnement est au cœur des activités Airbus. La tendance des systèmes avioniques est orientée vers la prépondérance des technologies logicielles. Le développement des méthodes et des outils pour la vérification et la démonstration de sûreté des logiciels constitue un axe majeur de recherche comme en témoignent sa contribution au développement de l'outil de preuve Caveat (CEA) dans le cadre de projets de recherche à financement aéronautique ainsi que ses participations aux projets DAEDALUS (5ème PCRD), ASTREE (RNTL), pour ce qui concerne l'interprétation abstraite. Airbus France prend une part active dans l'élaboration et l'évolution des normes internationales relatives à l'aéronautique (DO-178-B et futur DO-178-C).
DASSAULT AVIATION est un utilisateur final
d'outils de vérification de code. Certains logiciels
critiques embarqués sur avion, dont le logiciel de commande
de vol, sont développés en interne afin de garantir la
visibilité totale sur le processus et la qualité du
développement. Ces codes en langage C sont écrits
manuellement ou générés automatiquement à
partir de spécifications formelles à flots de contrôle
(automates à états finis) ou flots de données.
Les outils existants de vérification de code, de générations
de tests ou encore de simulation sont utilisés de façon
intensive tout au long du processus de développement.
La
mise en œuvre des
résultats attendus du projet CAT au sein des processus de
développement de logiciels critiques embarqués
contribuera aux travaux de certification de ces logiciels vis-à-vis
des autorités aéronautiques. Les preuves formelles de
propriétés fonctionnelles de haut niveau, obtenues à
l'aide de la méthodologie définie et des outils
développés dans CAT, permettront de garantir la
conformité de l'ensemble de l'application critique analysée
vis-à-vis de ses propriétés de sûreté
de fonctionnement.
SIEMENS VDO est un des fournisseurs majeurs du monde automobile. Siemens VDO développe des produits automotives pour les constructeurs automobiles dans l'objectif de favoriser la sécurité des passagers et des véhicules, promouvoir les solutions sécuritaires, améliorer le confort des passagers, augmenter les performances des moteurs, contribuer à la protection de l'environnement, favoriser le plaisir et l'ergonomie de la conduite, gérer les idées innovantes dans les systèmes communicants et multimédia. Siemens VDO est positionné sur le marché automobile comme fournisseur de produits innovants en électronique et informatique embarquées, dont la partie logicielle prend de plus en plus d'importance. Le développement de méthodes et outils pour la vérification et la validation du logiciel représentent donc un axe majeur de recherche dans sa stratégie. Siemens VDO est aussi un acteur majeur dans le projet AUTOSAR (milieu industriel automotive) en charge d'établir un standard d'architecture automotive ouvert supposé devenir le standard dominant des plate-formes logicielles automobiles. SIEMENS VDO est partenaire du pôle de compétitivité AESE avec certains acteurs du projet, et est notamment engagé sur plusieurs projets tel que TOPCASED et OVALIE.
FRANCE TELECOM : L'unité de recherche et développement MAPS/AMS/VVT (Vérification, Validation, Test) de la division R&D de France Télécom regroupe un peu moins d'une vingtaine de chercheurs (dont plusieurs thésards) spécialisés dans l'utilisation des méthodes formelles et les techniques de test. Elle contribue à l'amélioration globale de la qualité des logiciels embarqués dans les terminaux de France Télécom en participant à la définition des objectifs de sûreté de fonctionnement, en participant à la définition des procédures de validation, à la définition des plans de test, et en expérimentant et sélectionnant des outils d'analyse statique pour les codes C/C++ (Coverity, Polyspace). Nous développons par ailleurs des outils d'analyse statique dédiés aux besoins d'Orange. MAPS/AMS/VVT et le projet LANDE de l'INRIA mènent en commun des recherches sur l'utilisation des méthodes formelles pour la sûreté de fonctionnement dans le cadre d'un partenariat entre France Télécom et l'INRIA. Ces activités concernent principalement l'analyse statique des programmes Java téléchargeables sur des terminaux, la vérification de protocoles cryptographiques mais aussi les techniques de test.
Suivant les parties du projet, différents types d'exploitation sont prévus.
L'infrastructure logicielle de base sera distribuée sous forme de logiciel libre sous une licence ouverte qui sera à préciser. Par contre, chaque greffon pourra être muni d'une licence différente, libre ou non, suivant le choix de chaque partenaire participant directement au développement. Pendant toute la durée du projet, les participants pourront bien sûr utiliser librement l'ensemble des logiciels à des fins de recherche et développement. Après la fin du projet, le noyau restera libre, et les différents greffons pourront être commercialisés au gré de leurs concepteurs (c'est-à-dire le ou les partenaires ayant eu une activité de développement et de spécification prépondérante dans un sous-projet). Une activité de type service pourra être proposée autour du logiciel et de ses greffons par les partenaires.
Les résultats pourront être publiés dans le milieu académique sous réserve de la non-divulgation des éléments jugés confidentiels par les partenaires. Chaque document aura un niveau de confidentialité qui sera déterminé par ses auteurs.
Il pourra être envisagé un transfert vers d'autres acteurs industriels concernés à l'issue du projet. Dans ce cas, le CEA pourra se charger d'une distribution sous forme de licence, de partenariat ou de service combinés. En effet la complexité des outils mis en œuvre nécessite un support important de la part du distributeur et une connaissance suffisamment précise des technologies sous-jacentes pour pouvoir en proposer des évolutions adaptées aux besoins et au domaine d'application.
Ce projet aura un impact économique majeur puisqu'il sera la première suite complète française pour la vérification à la carte munie d'un langage de spécification “standardisé” et possédant une architecture adaptable aux besoins du marché. Comme tous les fournisseurs d'outils qui ont permis de détecter des erreurs dans les programmes, nous pourrons prétendre à réduire de façon significative les coûts des activité décrites dans le paragraphe 3.1.
Le consortium se compose de quatre acteurs majeurs de l'industrie automobile, aéronautique et des télécommunications et de trois acteurs académiques complémentaires reconnus qui ont tous déjà une expérience dans les domaines concernés par le projet. De plus, ces acteurs ont tous collaboré avec au moins un des autres partenaires du projet. CAT est donc la réunion et l'harmonisation de plusieurs collaborations bilatérales indépendantes autour de la thématique de la vérification en vue de dépasser les limites rencontrées auparavant.
La liste des partenaires avec le sigle que nous utiliserons dans la suite de ce document pour les mentionner entre parenthèses est :
CEA-List Laboratoire pour la Sûreté du Logiciel (CEA)
L'outil Caveat développé par le CEA List pour effectuer des preuves unitaires a été utilisé par Airbus pour vérifier en développement des parties critiques du logiciel de commande de vol de l'A380. Un sous-ensemble assez restreint du langage C a été utilisé par permettre les preuves par logique de Hoare.
L'outil a aussi été utilisé par EDF pour vérifier a posteriori des logiciels déjà écrits. Cette utilisation a conduit à introduire des techniques d'interprétation abstraite pour synthétiser des propriétés qui servent à détecter des menaces. Le sous-ensemble du langage C est ici moins restreint.
Le CEA List a effectué pour l'IRSN des travaux exploratoires sur les applications de la spécialisation de logiciel à l'aide à la compréhension et à l'analyse d'impact (étude de la version n+1 d'un logiciel).
Projet ProVal du PCRI-Université Paris-Sud, INRIA-Futurs (PROV)
Le projet ProVal développe l'outil de spécification et de preuve de logiciels C Caduceus qui est expérimenté dans le cadre de collaborations avec Dassault-Aviation et Axalto. Dans le cadre de l'initiative Digiteo-Labs, le CEA List et le projet ProVal ont démarré une coopération informelle pour développer une souche théorique et technique commune à leurs outils d'analyse statique et de preuve de logiciels C.
Projet Lande de l'IRISA, INRIA-Rennes (LANDE)
D’une part, un contrat cadre de recherche collaborative a été signé par le projet LANDE de l’INRIA et la division recherche et développement de France Télécom sur le thème de l’utilisation de méthodes formelles pour la sécurité et la sûreté de fonctionnement, formalisant ainsi plusieurs collaborations en cours. D’autre part, le projet LANDE est impliqué dans l’ACI V3F avec le CEA List pour le développement de techniques de résolution de contraintes pour l’analyse de programmes qui manipulent des nombres flottants.
Airbus FRANCE (AF)
L'objectif de l'effort de R&D consenti par Airbus est le transfert de technologies de vérification issues de la recherche fondamentale en informatique vers l'atelier de développement de ses logiciels avioniques. Ainsi Caveat est employé à la vérification unitaire (propriétés spécifiées par l'utilisateur) - désormais appelée Preuve unitaire - d'un logiciel critique embarqué dans l'A380, soumis à certification (DO 178-B), donc. Idem pour les analyseurs par Interprétation abstraite suivants : Fluctuat (CEA), Stackanalyzer (utilisation de la pile, AbsInt) et aiT (temps d'exécution au cas pire, AbsInt). Sur la base, notamment, de sa première utilisation industrielle de Caveat (Preuve unitaire d'un logiciel avionique), Airbus souhaite, dans le cadre de ce projet, partager son expérience et ainsi améliorer sa méthodologie, augmenter le taux de preuves automatiques en Preuve unitaire, passer à la Preuve d'intégration tout en maintenant un fort taux de preuves automatiques, tout en étant conscient de l'enjeu que cela représente également en termes de spécification formelle des propriétés, pouvoir réaliser des analyses d'impact de modifications grâce au "slicing", que soit développée significativement durant le projet la notion de validation des outils de CAT.
Dassault Aviation (DA)
Depuis
1990, DASSAULT AVIATION a réalisé un ensemble d'études
dans le domaine des méthodes formelles. Les premières
ont porté sur les langages synchrones à flots de
contrôle (Esterel), puis à flots de données
(Lustre), le model-checking (par automates explicites, puis à
l'aide de model-checking symbolique à base de BDD), en
collaboration avec des équipes de recherche qui assuraient le
développement de ces outils.
Parallèlement, des
techniques de preuve de théorème, à l'aide de
l'assistant de preuve Coq de l'INRIA, ont été mises en
œuvre afin de prouver des
propriétés de sûreté de fonctionnement sur
des algorithmes critiques.
Ces dernières années, un
effort conséquent a été fourni afin d'introduire
la modélisation UML et les méthodes et outils de
spécification formelle (outils SCADE et Esterel Studio
d'Esterel Technologies, et MatLab/Simulink de The MathWorks) dans nos
processus de développement d'applications critiques temps-réel
embarquées (dont les logiciels de commande de vol). La
vérification automatique de certaines propriétés
de sûreté sur nos modèles SCADE a été
établie avec succès à l'aide d'outils de preuve
de type model-checker (outil Prover de Prover Technologies).
Depuis
deux ans, DASSAULT AVIATION porte un intérêt croissant
aux outils et méthodes d'analyse statique et de preuve de
propriétés fonctionnelles sur des codes critiques
écrits en C ou générés automatiquement à
partir de spécifications formelles. L'objectif est d'obtenir
la preuve formelle de la validité de propriétés
de haut niveau portant sur l'ensemble du logiciel embarqué.
Dans ce sens, des coopérations ont été établies
avec le CEA-List (sur l'outil CAVEAT), puis plus récemment
avec le LRI de l'université Paris-Sud - ProVal / INRIA Futurs
(sur l'outil CADUCEUS).
Dans le cadre du projet CAT, DASSAULT
AVIATION participera activement à l'expression des besoins du
point de vue industriel en matière de preuve de programme,
interprétation abstraite, slicing, et preuve automatique,
ainsi qu'à la définition d'une méthodologie de
vérification. L'identification de codes source C réels
ou représentatifs de nos applications critiques fournira une
base d'expérimentation et d'évaluation de la
méthodologie et des outils développés dans CAT.
Les résultats attendus de ce projet doivent contribuer aux
travaux de certification de nos logiciels critiques embarqués,
dans le cadre du processus DO178-B, auprès des autorités
aéronautiques de certification.
Siemens-VDO (SVDO)
Siemens VDO souhaite investir ses efforts de R&D dans le transfert de technologies innovantes issues du monde académique et de ses applications dans divers contextes industriels afin de les adapter pour le milieu automobile. À ce titre, une première expérience sur la vérification par analyse statique est en cours chez Siemens VDO avec l'outil Caveat sur une application industrielle de contrôle moteur. L'objectif est de définir les zones d'applicabilité de Caveat au logiciel de type contrôle moteur et de faire un bilan sur la syntaxe du code C non supporté par l'outil (couche basse et applicative du logiciel). Un autre objectif est la prise en compte des retombées de ce projet pour promouvoir ces solutions innovantes dans le cadre du projet AUTOSAR en vue d'améliorer la qualité et la sûreté du processus de développement logiciel.
France Télécom (FT)
France Télécom commercialise des offres de service intégrant des équipements clients spécifiques (passerelles, set-top-boxes, terminaux mobiles) développés selon les spécifications de l'opérateur. Ces terminaux intègrent de nombreux logiciels d'origines diverses (développement interne ou à façon, logiciels commerciaux ou open-source). Ces logiciels doivent être validés lors de leur intégration pour assurer des propriétés minimales de sécurité et de disponibilité pour le client final. En particulier, il est nécessaire d'avoir des garanties fortes sur l'absence de vulnérabilités permettant la prise de contrôle du terminal par un acteur malveillant. Le niveau de garantie recherché est d'autant plus grand que le code source du logiciel est librement disponible. L'importance prise par les délais de commercialisation dans l'industrie des télécommunications implique qu'une analyse statique automatique sera souvent la seule technique de vérification utilisée de manière réaliste en plus des tests. Vu l'origine diverse des logiciels, les outils d'analyse statique produits doivent pouvoir traiter des codes écrits de manière variée, donc ne respectant pas nécessairement des règles de codage strictes. C'est ce que permet un outil commercial tel que Coverity aux dépens de la présence de garanties fortes. Les logiciels soumis par France Télécom dans le projet seront typiquement des logiciels open-source présents dans des terminaux (par exemple, les librairies BusyBox, microLibC, voire des noyaux Linux). Les résultats du projet CAT permettront de disposer d'outils traitant des codes réalistes, tout en ayant une garantie forte sur l'absence de vulnérabilité.
Le CEA List coordonnera les acteurs académiques et industriels afin d'aboutir à une interaction entre les différentes techniques et expériences. Il sera procédé à 4 réunions pléniaires par an pour faire le point sur l'état d'avancement des sous-projets.
Pilotage : CEA-LIST
Calendrier et phasage du projet :
M0-M6 : Évaluation des besoins et synthèse des expériences passées (sous-projet 1)
M6-M24 : Mise au point du langage, prototypage du noyau et des analyses élémentaires en interaction forte avec les industriels (sous-projets 2,3,4,5,6,7)
M24-M36 : Définition des méthodologies d'utilisation et qualification (sous-projets 8,9)
Calendrier de validation :
M7-M24 : Expérimentation sur des cas réels provenant des partenaires dès M7
M24-M35 : Évaluation par les utilisateurs des avancées par rapport aux outils existants sur des cas réels
M36 : Évaluation finale
Qualité : le CEA gérera un processus qualité ISO9001 pour l'ensemble des activités du projet. Le CEA est lui-même certifié suivant cette norme et possède toute l'expérience et les moyens humains nécessaires dans ce domaine pour gérer au mieux ce processus.
Répartition globale des tâches (le responsable du sous-projet est en gras):
Sous projet 1 : Évaluation des besoins CEA,AF,SVDO,DA, FT, PROV, LANDE
Sous projet 2 : Infrastructure générique CEA,PROV
Sous projet 3 : Greffons d'interprétation abstraite CEA, PROV, LANDE
Sous projet 4 : Greffons de preuve automatique PROV, CEA
Sous projet 5 : Greffon de réduction de code CEA, AF, DA, SVDO
Sous projet 6 : Greffon de preuve à la Hoare PROV, CEA
Sous projet 7 : Langage de spécification PROV, CEA, AF
Sous projet 8 : Méthodologie de vérification CEA, AF, DA, SVDO, FT
Sous projet 9 : Définition des objectifs de qualification des outils CEA, AF, DA, SVDO
Sous projet 10 : Évaluation de la méthodologie et des outils développés CEA, AF, DA, SVDO, FT
L'interaction entre les sous-projets se fera à travers le langage de propriétés et l'infrastructure générique qui contiendra une base de données de toutes les propriétés écrites dans ce langage. Chaque analyse pourra consulter cette base et interpréter les propriétés dans son formalisme propre.
On notera que chaque sous-projet fait intervenir au moins deux partenaires complémentaires tant en terme de compétences scientifique et technique qu'en terme de connaissance du domaine d'application étudié. Chaque sous-projet a un lien direct avec une expérience passée des partenaires sur le même thème, mais l'originalité consiste en la combinaison de ces thèmes et de ces partenaires. Cette combinaison est une source d'enrichissement mutuel en soi, qui s'ajoute à l'intérêt propre du projet.
Les sous-projets sont décrits précisément dans l'annexe située à la fin de ce document.
À l'issue de ce projet, nous disposerons d'une suite d'outils intégrés permettant une approche globale de la vérification. Cette suite sera pourvue d'une architecture extensible qui pourra simplement se décliner en outils adaptés aux besoins individuels des entreprises.
Nous aurons aussi défini un langage de spécification pour les programmes C, dans lequel il est possible d'exprimer des propriétés aussi précises que possible sur un programme C quelconque.
Le noyau du projet sera disponible sous forme de code Open Source, et en particulier tout ce qui touche au langage de spécification. L'ensemble sera exploitable par les partenaires du projet à des fins de recherche et développement. Les auteurs de chaque délivrable préciseront les modalités de diffusion de leur production au cas par cas (publication, diffusion sous licence libre ou propriétaire, confidentiel, etc...). Le noyau sera librement disponible sur une page web ainsi que le langage de spécification. L'exploitation commerciale des résultats du projet pourra se faire après établissement d'accords spécifiques entre les parties concernées. Les partenaires se réservent la possibilité, à l'issue du projet, de proposer des services autour des prototypes développés dans le cadre du projet ou de se tourner vers un éditeur d'outil.
L'enjeu économique est majeur : il n'existe à ce jour pas de solution de vérification flexible et ouverte, alors que le besoin est manifeste. Une telle infrastructure serait un atout pour l'ensemble des producteurs et des vérificateurs de code C sûr, qui pourraient simplement adapter ou faire adapter CAT à leurs besoins ou même simplement utiliser le langage de spécification comme passerelle vers d'autres outils ou comme outil de communication pour leurs analyses.
Le tableau suivant donne la répartition des frais de personnel, en hommes*mois, par sous-projet et par partenaire.
Sous Projet |
CEA |
PROV |
LANDE |
AF |
SVDO |
DA |
FT |
---|---|---|---|---|---|---|---|
SP1 |
6 |
2 |
2 |
6 |
2 |
6 |
4 |
SP2 |
10 |
10 |
|
|
|
|
|
SP3 |
14 |
20 |
62 |
|
|
|
|
SP4 |
10 |
18 |
|
|
|
|
|
SP5 |
14 |
|
|
3 |
1 |
2 |
|
SP6 |
14 |
10 |
|
|
|
|
|
SP7 |
12 |
12 |
|
2 |
|
|
|
SP8 |
12 |
|
|
9 |
1 |
4 |
4 |
SP9 |
4 |
|
|
3 |
|
2 |
|
SP10 |
12 |
|
|
13 |
5 |
12 |
4 |
Total |
108 |
72 |
64 |
36 |
9 |
26 |
12 |
Le tableau suivant donne en kilo-euros et pour chaque partenaire :
- le coût des hommes*mois,
- le coût matériel,
- le coût des missions,
- le coût de revient total en incluant les frais de personnel, les déplacements divers, et les investissements matériels (stations de développement, ),
- l'aide demandée.
Coûts k€ |
CEA |
PROV |
LANDE |
AF |
DA |
SVDO |
FT |
TOTAL |
---|---|---|---|---|---|---|---|---|
Hommes mois |
1278,18 |
413,322 |
329,315 |
501,12 |
450,58 |
127,8 |
176,61 |
3391,6 |
Matériel |
9 |
4 |
9 |
|
|
|
|
22 |
Missions |
|
30 |
14,328 |
1,8 |
|
7,5 |
9,6 |
63,23 |
Total |
1287,18 |
447,32 |
352,643 |
502,92 |
450,58 |
135.3 |
186,2 |
3361.83 |
Aide demandée |
643,59 |
161,408 |
60,528 |
125,73 |
112,645 |
33,8 |
46,55
|
1184.251 |
Les frais de personnel pour l'ensemble du projet sont de : 327 hommes*mois.
Le coût global, tout compris, de l'ensemble du projet a été estimé à 3 361 830 Euros.
L'aide globale demandée pour l'ensemble du projet est de 1 184 251 Euros.