Frama-C, l’analyse sans faille de code source en C

Frama-C est une plateforme open source d’analyse de programmes écrits en langage C, en vue d’en vérifier la sûreté et la sécurité. Elle combine différentes techniques pour garantir l’absence de bugs ou de vulnérabilités.

Frama-C peut garantir l’absence de défauts logiciels susceptibles de générer une erreur lors de l’exécution ou de permettre des actions malveillantes, mais aussi de garantir le respect de propriétés spécifiques (fonctionnelles, temporelles, relationnelles, contraintes globales, confidentialité, intégrité, etc.) décrites par l’utilisateur.

La principale particularité de Frama-C est que ses analyseurs ne restent jamais silencieux quand un problème peut apparaître. Ils sont basés sur les méthodes formelles, des méthodes d’analyses mathématiques, comme l’interprétation abstraite, la vérification déductive, la vérification dynamique de propriétés, etc. Ces analyseurs coopèrent pour garantir l’absence de bugs ou vulnérabilités en échangeant des informations via un langage de spécification dédié.

Frama-C est adapté aux contextes critiques (aéronautique, nucléaire, ferroviaire, …), où de très hauts niveaux de garantie sont exigés, mais également pour des contextes de cybersécurité pour garantir certaines classes de propriétés de sécurité (confidentialité et intégrité).

Reconnu au niveau national et mondial, l’outil est utilisé par un grand nombre de partenaires institutionnels, tels que l’ANSSI ou la DGA, et industriels tels qu’AIRBUS, EDF, Thales ou Sandia Labs.

• Systèmes critiques et/ou embarqués : vérification formelle de l’absence de défauts logiciels, vérification des propriétés fonctionnelles, (DO 178-C, ISO 60880, …).
• Cybersécurité : détection de vulnérabilités dans les programmes, vérification de la fiabilité de contre-mesures, vérification de propriétés de sécurité (reconnaissance sur le schéma français pour les certifications les plus exigeantes en sécurité à savoir les certifications critères Communs EAL6/7).
• Enseignement : utilisation du logiciel par des universités, en France et à l’étranger pour des formations sur le test, l’analyse et/ou la preuve de programme et plus généralement de génie logiciel.

Parmi les évolutions prévues de l’outil :

• ouverture de la plateforme vers d’autres langages de programmation pour traiter des bases de codes toujours plus complexes et hétérogènes,
• création de nouvelles extensions au langage de spécification pour pouvoir exprimer et vérifier de nouveaux types de propriétés,
• amélioration continue des techniques de visualisation pour garantir que les résultats d’analyse restent exploitables malgré des bases de codes toujours plus grandes et complexes,
• utilisation de techniques d’apprentissage pour faciliter la configuration des analyseurs et réduire l’effort utilisateur.