Résumé du projet CAT (C Analysis Toolbox)
Analyse de programmes C issus de l'aéronautique et de l'automobile
L'objectif de ce projet est de développer une boîte à outils en logiciel libre permettant d'analyser des codes de taille industrielle écrits en C pendant les phases de :
développement, afin de garantir la réutilisabilité de composants
vérification, pour étudier la robustesse (détection d’opérations indésirables telles que division par zéro…), pour établir la propagation des fautes et pour établir des propriétés globales (par exemple pour une certification)
maintenance et évolution pour mettre en évidence les liens de dépendance (flots de contrôle, flots de données,…) pour trouver l'impact de modifications ou aider à la compréhension du code
Ces activités représentent une part largement prépondérante dans le coût du développement d'un logiciel, en particulier quand celui-ci est destiné à être embarqué dans un système critique. Notre projet se propose d'aider à réduire les coûts liés à ces activités à travers la mise en place d'une infrastructure générique qui permettra une interaction des différentes techniques.
Cette infrastructure sera utilisée pour construire des outils spécialisés répondant aux besoins précis des utilisateurs industriels. Ces outils se distingueront des outils existants par la levée des restrictions quant au fragment du langage C supporté et des performances accrues. Cela sera permis par l’expérience acquise, une meilleure coopération entre chercheurs, l’évolution de la technologie et de la théorie. En particulier on s’appuiera sur des outils existants puissants de large diffusion.
Nous fournirons aussi un outil de spécialisation de logiciel intégré dans l'infrastructre globale qui permettra aux techniques qui ne s'appliquent pas bien à des codes complets génériques de donner des résultats pertinents.
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, programmes C, interprétation abstraite, logique de Hoare, contraintes, spécialisation de code, méthodes formelles
Il existe aujourd'hui une offre concernant les outils de vérification de code C (PolySpace, Astrée, Caveat, Caduceus, etc).
L'originalité de notre boîte à outils est :
d'une part d'intégrer les différentes techniques existantes (interprétation abstraite, preuve à la Hoare, spécialisation de code) en permettant de les faire collaborer de façon très fine. Les outils existants utilisent chacun une technique unique et les utilisateurs industriels ayant opté pour une technique regrettent souvent l'absence d'intégration des autres techniques ;
d'autre part de lever les limitations habituelles concernant le fragment du langage C traité par certains outils (traitement des casts, dépendance envers le schéma de compilation, traitement des pointeurs de fonctions, des alias, ...) ;
de mener des analyses sur les parties pertinentes du code (en procédant par spécialisation). Après spécialisation, on peut appliquer des techniques qui ne pourraient s'appliquer sur le code complet ;
et enfin d'augmenter l'automatisation des preuves en utilisant les idées de la résolution de contraintes et les dernières avancées en matière de preuve automatique.
Ces objectifs exigent à la fois des travaux théoriques justifiant la correction de cette approche hybride de la vérification et des travaux technologiques pointus afin de mettre en oeuvre ces techniques de façon suffisament efficace pour que la boîte à outils puisse analyser des codes de taille importante.
Le premier objectif est de tirer partie de la combinaison des techniques d'analyse et de spécialisation de code afin de vérifier des logiciels de taille réelle. Il s'agit de définir des méthodologies qui garantissent que l'ensemble de l'activité de vérification est cohérente et apporte des éléments de confiance dans les logiciels étudiés.
Le second objectif est de mener une réflexion sur la qualification des outils de vérification développés. C'est une étape absolument fondamentale pour pouvoir intégrer ces outils dans les chaînes de production en obtenant l'accord des organismes de certification.
Le CEA List a développé l'outil Caveat qui a été utilisé par Airbus pour la vérification en développement de parties critiques du logiciel de commande de vol de l’A380.
L’outil Caveat a aussi été utilisé par EDF pour vérifier a posteriori des logiciels déjà écrits et pour constituer des dossiers de sûreté. 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 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 pour la certification de la version n+1 d’un logiciel.
Le projet ProVal du PCRI (Université Paris-Sud, INRIA-Futurs) développe l'outil de spécification et de preuve de logiciels C Caduceus qui est experimenté dans le cadre de collaborations avec Dassault-Aviation et Axalto.
Le projet ProVal possède une grande expériences dans le développement d'outils de preuves automatiques (CiME) et interactives (Coq).
Le CEA List et le projet ProVal coopèrent pour développer une souche théorique et technique commune à leurs outils d’analyse statique et de preuve de logiciels C.
Le CEA List et l'IRISA coopèrent sur l’exploitation des techniques de résolution de contraintes pour la génération de tests et la preuve de propriétés (action V3F de l’ACI-SI).
Le CEA List coordonnera les acteurs académiques et industriels afin d'aboutir à une interaction entre les différentes techniques. Ces techniques seront développées autour d'un noyau technologique centré sur l'analyseur CIL et comportant les services de base pour garantir une possibilité d'interaction entre les différents développements. Le noyau sera distribué sous une licence libre mais chaque analyse restera la propriété de ses concepteurs.
Les frais de personnel pour l'ensemble du projet sont de : 311 hommes*mois.
Le coût global, tout compris, de l'ensemble du projet a été estimé à 3 476 800 Euros.
L'aide globale demandée pour l'ensemble du projet est de 1 184 251 Euros.