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

Frama-C est un logiciel open source d‘analyse de programmes écrits en langage C, en vue d’en vérifier la sûreté et l’absence de vulnérabilités au sens cybersécurité. Il se caractérise par deux qualités :

• sa capacité à garantir l’absence de défauts logiciels susceptibles de générer une erreur lors de l’exécution,
• la possibilité pour l’utilisateur de tester et prouver la conformité du programme à des propriétés formelles.

Ces deux qualités rendent l’outil particulièrement adapté à des contextes critiques (aéronautique, nucléaire, ferroviaire, santé…), où de très hauts niveaux de garantie sont exigés, et pour lesquels le nombre de cas de tests à réaliser s’avère en général rédhibitoire.

Le logiciel est construit autour d’un noyau, qui gère le code sous analyse, et de modules, ou greffons, spécialisés dans diverses fonctions. Certains sont dédiés à une technique d’analyse : analyse par interprétation abstraite, analyse déductive, vérification dynamique de propriétés, etc. D’autres servent à vérifier des classes de propriétés spécifiques (temporelles, relationnelles, contraintes globales, etc.). D’autres encore ont vocation à aider les utilisateurs à naviguer dans le code pour identifier les causes d’un problème (dépendances de données, de contrôle, …). Les greffons coopèrent pour dépister les bugs en échangeant des informations (des résultats partiels ou finaux, des annotations etc.) dans un langage dédié. Cela, en collaborant séquentiellement ou simultanément.

Parmi ses évolutions récentes, Frama-C s’est enrichi de fonctions permettant de spécifier et de vérifier des propriétés liées à la cybersécurité.

Reconnu au niveau mondial, l’outil est utilisé par un grand nombre de partenaires institutionnels, tel que l’ANSSI, et industriels tels qu’Airbus, EDF, Thales et, dans un contexte R&T, par Dassault Aviation.

• Systèmes critiques et/ou embarqués : vérification formelle de l’absence de défauts logiciels, vérification des propriétés fonctionnelles, vérification des propriétés de sécurité (confidentialité, intégrité, disponibilité).
• Intelligence Artificielle : Analyse de bibliothèques.
• Cybersécurité : détection de vulnérabilités dans les programmes, vérification de la fiabilité de contre-mesures.
• Génération de tests.
• 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 :

• l’analyse de programmes qui incorporent des techniques d’apprentissage machine,
• l’utilisation de techniques d’intelligence artificielle pour faciliter la mise en œuvre des analyses (sujet abordé par le projet H2020 Decoder, avec la génération de spécifications formelles à partir de documentation en langage naturel, et poursuivi dans le projet du Grand Défi Cyber LEIA),
• la prise en compte des nouvelles méthodes de développement et de déploiement de logiciels (intégration continue) par la possibilité de réutiliser les résultats existants pour l’analyse d’une nouvelle version d’un code (sujet également abordé dans le cadre du projet LEIA).