Frama-C est une plateforme d’analyse de programmes écrits en C, adapté notamment aux contextes critiques (nucléaire, aéronautique, ferroviaire, santé, etc.). Elle permet de garantir l’absence d’erreurs logicielles et de prouver la conformité du code à des propriétés formelles.
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.
Ses forces principales :
Frama-C est l’un des rares outils au monde à avoir passé les tests d’évaluation des analyseurs de code du NIST (National Institute of Standards and Technology) et à avoir satisfait au critère le plus exigeant, à savoir la capacité à garantir l’immunité du code.
Thales doit certifier les machines virtuelles de ses cartes à puce, c’est-à-dire le code chargé d’exécuter les applications sur celles-ci. L’objectif est, en particulier, de vérifier leurs propriétés d’intégrité et de confidentialité. L’industriel y est parvenu grâce à Frama-C. Réalisée fin 2021, l’opération a été une première dans le monde des cartes à puce de grande diffusion amenant en 2022 jusqu’au plus haut niveau de certification Critères Communs, le CC EAL7.
Pour en savoir plus, lire la publication.
Cela fait de Frama-C le troisième outil reconnu par la centre de certification de l’ANSSI, connu pour son exigence, pour les certifications Critères Communs aux niveaux EAL6 et EAL7, aux côtés de Rocq et Atelier B. De plus Frama-C est le seul de ces trois outils à travailler directement sur le code cible du produit certifié et donc augmentant encore la confiance dans l’analyse faite.
Parmi les évolutions prévues de l’outil :
Pour en savoir plus, visiter le site Frama-C.
