Software:Frama-C
From HandWiki
Short description: Libre Ocaml formal C verifier
 | |
| Developer(s) | Commissariat à l'Énergie Atomique (CEA-List) and Inria |
|---|---|
| Written in | OCaml |
| Operating system | Microsoft Windows, FreeBSD, OpenBSD, Linux, Mac OS X |
| Available in | English |
| Type | Formal verification, Static code analysis |
| License | mostly LGPL, some parts under BSD licenses |
| Website | frama-c |
Frama-C[1] stands for Framework for Modular Analysis of C programs. Frama-C is a set of interoperable program analyzers for C programs. Frama-C has been developed by the French Commissariat à l'Énergie Atomique et aux Énergies Alternatives (CEA-List)[2] and Inria. It has also received funding from the Core Infrastructure Initiative. Frama-C, as a static analyzer, inspects programs without executing them. Despite its name, the software is not related to the French project Framasoft.
Architecture
 | This section is missing information about use of Clang for C++ input at least since 2014. (September 2021) |
Frama-C has a modular plugin architecture[3] comparable to that of Eclipse or GIMP.
Frama-C relies on CIL (C Intermediate Language) to generate an abstract syntax tree. The abstract syntax tree supports annotations written in ANSI/ISO C Specification Language (ACSL).
Several modules can manipulate the abstract syntax tree to add ANSI/ISO C Specification Language (ACSL) annotations. Among frequently used[vague] plugins are:
- Value analysis – computes a value or a set of possible values for each variable in a program. This plugin uses abstract interpretation techniques and many other plugins make use of its results.
- Jessie – verifies properties in a deductive manner. Jessie relies on the Why[4] or Why3 back-end to enable proof obligations to be sent to automatic theorem provers like Z3, Simplify, Alt-Ergo or interactive theorem provers like Coq or Why. Using Jessie, an implementation of bubble-sort or a toy e-voting system can be proved to satisfy their respective specifications. It uses a separation memory model inspired by separation logic.
- WP (Weakest Precondition) – similar to Jessie, verifies properties in a deductive manner. Unlike Jessie, it focuses on parameterization with regards to the memory model. WP is designed to cooperate with other Frama-C plugins such as the value analysis plug-in, unlike Jessie that compiles the C program directly into the Why language. WP can optionally use the Why3 platform to invoke many other automated and interactive provers.
- Impact analysis – highlights the impacts of a modification in the C source code.
- Slicing – enables slicing of a program. It enables generation of a smaller new C program that preserves some given properties.[5]
- Spare code – removes useless code from a C program.
Other plugins are:
- Dominators – computes dominators and postdominators of statements.
- From analysis – computes functional dependencies.
Features
Frama-C can be used for the following purposes:
- To understand C code which you have not written. In particular, Frama-C enables one to observe a set of values, slice the program into shorter programs, and navigate in the program.
- To prove formal properties on the code. Using specifications written in ANSI/ISO C Specification Language enables it to ensure properties of the code for any possible behavior. Frama-C handles floating point numbers.[6]
- To enforce coding standards or code conventions on C source code, by means of custom plugin(s)[7]
- To instrument C code against some security flaws[8]
See also
References
- ↑ "Frama-C". http://frama-c.com.
- ↑ CEA LIST. "CEA LIST, Smart digital systems". http://www-list.cea.fr/en/.
- ↑ Pascal Cuoq (August 2009). "Experience report: OCaml for an industrial-strength static analysis framework". ACM SIGPLAN Notices 44 (9): 281–286. doi:10.1145/1631687.1596591.
- ↑ "Why homepage". http://why.lri.fr/.
- ↑ Benjamin Monate; Julien Signoles (2008). "Slicing for Security of Code". Trusted Computing - Challenges and Applications. Lecture Notes in Computer Science. 4968/2008. pp. 133–142. doi:10.1007/978-3-540-68979-9_10. ISBN 978-3-540-68978-2.
- ↑ Sylvie Boldo; Thi Minh Tuyen Nguyen (2010). "Hardware-independent proofs of numerical programs". Proceedings of NFM 2010. http://shemesh.larc.nasa.gov/NFM2010/papers/nfm2010_14_23.pdf.
- ↑ David Delmas; Stéphane Duprat; Victoria Moya Lamiel; Julien Signoles. "Taster, a Frama-C plug-in to enforce Coding Standards". Embedded Real Time Software and Systems 2010, Toulouse, France. http://web1.see.asso.fr/erts2010/Site/0ANDGY78/Fichier/PAPIERS%20ERTS%202010/ERTS2010_0003_final.pdf.
- ↑ Jonathan-Christofer Demay; Éric Totel; Frédéric Tronel (2009). "Automatic Software Instrumentation for the Detection of Non-control-data Attacks". Recent Advances in Intrusion Detection. Lecture Notes in Computer Science. 5758/2009. pp. 348–349. doi:10.1007/978-3-642-04342-0_19. ISBN 978-3-642-04341-3.
External links
 |  |
