Partager

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

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.

L’usage

Valider la qualité d’un 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.

Ses atouts

De multiples techniques d'analyse, son architecture modulaire...

Ses forces principales :

  • ses performances liées à l’exhaustivité de ses techniques d’analyse,
  • ses capacités de vérification de l’absence de vulnérabilités
  • ses capacités à vérifier des propriétés définies par l’utilisateur,
  • l’interaction entre ses différents greffons, qui offre une grande souplesse d’utilisation,
  • des opportunités de développement pour répondre aux enjeux de cybersécurité, de souveraineté numérique.

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.

Applications

Systèmes critiques, cybersécurité…

  • 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.
Success story

Thales utilise Frama-C pour certifier l'OS de ses cartes à puces

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.

Evolution

La prise en compte de nouvelles tendances logicielles

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.

Publications

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

À lire également

Avancées technologiques

12 décembre 2024 | Démantèlement nucléaire : réussite de la démonstration sur site des technologies du CEA-List

Découvrez comment le CEA-List sécurise le démantèlement nucléaire, avec ses technologies innovantes de détection et mesure des rayonnements ionisants.
Lire la suite
Plateformes technologiques

Plateforme de Contrôle Non Destructif : développer et valider des technologies innovantes de contrôle industriel

Un plateau de 500m2 pour expérimenter les procédés d’inspection à base d’ultrasons et ondes guidées, méthodes électromagnétiques, radiographie et tomographie.
Lire la suite
Programmes de recherche

Instrumentation numérique

Le développement de systèmes ou de techniques d’acquisition de ces données, couplé à des algorithmes de traitement avancés répond à des enjeux majeurs dans différents secteurs d’activité...
Lire la suite
Use Cases

Inspecter des pièces réalisées en fabrication additive

Le CEA-List développe des méthodes de Contrôle Non Destructif (CND) pour l’inspection de pièces issues de la fabrication additive.
Lire la suite