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 :
Guide to Sofware Verification with Frama-C: Core Components, Usages and Applications. Nikolai Kosmatov, Virgile Prevosto, Julien Signoles, Springer Cham, July 2024.
Reusing Caches and Invariants for Efficient and Sound Incremental Static Analysis. Mamy Razafintsialonina, David Bühler, Antoine Miné, Valentin Perrelle, Julien Signoles. European Conference on Object-Oriented Programming (ECOOP), June 2025.
Sound Runtime Assertion Checking for Memory Properties via Program Transformation. Dara Ly, Nikolai Kosmatov, Frédéric Loulergue, Julien Signoles. Formal Aspects of Computing, 2024.
High-Level Program Properties in Frama-C: Definition, Verification and Deduction. Virgile Robles, Nikolai Kosmatov, Virgile Prevosto, Pascale Le Gall. ISoLA 2024.
A Bottom-Up Formal Verification Approach for Common Criteria Certification:
Application to JavaCard Virtual Machine. Adel Djoudi, Martin Hána, Nikolai Kosmatov, Milan Kříženecký, Franck Ohayon, Patricia Mouy, Arnaud Fontaine and David
Féliot. ERTS 2022, Best paper award.
The dogged pursuit of bug-free C programs: the Frama-C software analysis platform. Patrick Baudin, François Bobot, David Bühler, Loïc Correnson, Florent Kirchner, Nikolai Kosmatov, André Maroneze, Valentin Perrelle, Virgile Prevosto, Julien Signoles, Nicky Williams. Communications of the ACM, 2021.
Pour en savoir plus, visiter le site Frama-C