Frama-C is a platform for analyzing programs written in C for critical systems in the nuclear energy, aeronautics, rail, health and other industries. It can guarantee the absence of any software errors and prove the conformity of code to formal properties. This tool has also recently been augmented with modules for verifying cybersecurity properties.
Frama-C is a code analysis platform for programs written in C, capable of ensuring that code is safe and free of any cybersecurity vulnerabilities. It brings two notable qualities to the equation:
These two qualities make the tool particularly well-suited for nuclear energy, aeronautics, rail, health, and other contexts where there are very stringent requirements for verification, or contexts involving a volume of cases to test that exceeds what conventional tools can handle.
The software is built around a core that manages the code being analyzed and added modules that are specialized for various functionalities. Some are dedicated to a certain analysis technique (such as abstract interpretation, deductive analysis, dynamic property verification, etc.), while others verify specific types of properties, such as temporal and relational properties or global constraints. Still others help users navigate code to identify the causes of a problem, such as data or control dependency. The modules cooperate to diagnose software bugs by exchanging information (partial or final results, annotations, etc.) in a language dedicated for the purpose. They can do this both sequentially and simultaneously.
Recently, Frama-C was augmented with several modules, including one for cybersecurity specifications and verification.
The tool is known around the world and used by a large number of public-sector partners like ANSSI and partner companies like EDF and Thales Dassault Aviation also uses it for technology research.
Main advantages:
Frama-C is one of the few tools in the world to have passed the NIST (National Institute of Standards and Technology) Ockham Sound Analysis Criteria, satisfying the strictest of all requirements, guaranteed code immunity.
Thales needed to certify the virtual machines—the code that executes applications—onboard its smart cards. The company identified two properties—integrity and privacy—that needed to be formally validated. Frama-C helped Thales reach this goal at the end of 2021, a first in the world of mass-produced smart cards.
Planned updates:
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, and Nicky Williams. 2021.. Commun. ACM 64, 8 (August 2021), 56–68.
Structuring Abstract Interpreters Through State and Value Abstractions, Sandrine Blazy, David Bühler and Boris Yakobowski. In Verification, Model Checking, and Abstract Interpretation (VMCAI), 2019
Logic against ghosts: Comparison of two Proof Approaches for a List Module SAC 2019, Allan Blanchard, Nikolai Kosmatov, Frédéric Loulergue. The 34th ACM/SIGAPP Symposium On Applied Computing, Apr 2019.
How testing helps to diagnose proof failures, Guillaume Petiot, Nikolaï Kosmatov, Bernard Botella, Alain Giorgetti, Jacques Julliand. Springer Verlag, 2018, 30 (6), pp.629 – 657.
Shadow state encoding for efficient monitoring of block-level properties, Kostyantyn Vorobyov Julien Signoles Nikolai Kosmatov, Proceedings of the 2017 ACM SIGPLAN International Symposium on Memory Management.
MetAcsl: Specification and Verification of High-Level Properties Virgile Robles, Nikolai Kosmatov, Virgile Prevosto, Pascale Le Gall
TACAS (25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems), Avril 2019.
Go to Frama-C website
