ANNEXE TECHNIQUE DU PROJET CAT

C Analysis Toolbox

Analyse de programmes C critiques embarqués

1) Introduction

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 :

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 :


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) Objectifs de recherche technologique du projet

2-1) État de l'art et intérêt du projet

État de l'art

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 :

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.

Expérience des partenaires académiques

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.

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 :

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

3) Objectifs industriels du projet

3-1) Marché et intérêt du projet

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é :

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é.

3-2) Types d'exploitation envisagés, diffusion des résultats et retombées économiques

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.

4) Organisation du projet

4-1) Partenariat

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 :

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).


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.


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.

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.

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 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 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.


4-2) Organisation du partenariat dans le projet








5) Description technique du projet

Les sous-projets sont décrits précisément dans l'annexe située à la fin de ce document.

6) Résultats du projet et retombées

À 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.


7) Présentation des ressources et des dépenses et aide demandée

7.1) Estimation et justification des coûts par tape et par partenaire

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



7.2) Estimation des coûts globaux du projet

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.