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.

Not to be confused with Framasoft.
Frama-C
Developer(s)Commissariat à l'Énergie Atomique (CEA-List) and Inria
Written inOCaml
Operating systemMicrosoft Windows, FreeBSD, OpenBSD, Linux, Mac OS X
Available inEnglish
TypeFormal verification, Static code analysis
Licensemostly LGPL, some parts under BSD licenses
Websiteframa-c.com

Architecture

Frama-C has a modular plugin architecture[3] comparable to that of Eclipse (software) 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 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]
gollark: So that gets to be the most *annoying*, but spaghet is the *worst*, then? Hmm.
gollark: https://discordapp.com/channels/379850656191741952/392746465375551489/627276672718340106
gollark: I thought that was nano[LAST PART OF WORD REDACTED FOR RULES REASONS] or something.
gollark: "Unfortunately, a motor in your iLeg has failed. We'll need to remove and replace your leg. Since our diagnostics data says it was at one point repaired by an unauthorized provider, we'll be billing you the full £$10000."
gollark: I'll try imagemagicking it.

See also

References
  1. "Frama-C". frama-c.com. Retrieved 2016-11-05.
  2. CEA LIST. "CEA LIST, Smart digital systems". Retrieved 2016-11-05.
  3. Pascal Cuoq; et al. (August 2009). "Experience report: OCaml for an industrial-strength static analysis framework". Proceedings of the 14th ACM SIGPLAN International Conference on Functional Programming. 44 (9): 281–286. doi:10.1145/1631687.1596591.
  4. "Why homepage".
  5. Benjamin Monate; Julien Signoles (2008). "Slicing for Security of Code". Trusted Computing - Challenges and Applications. Lecture Notes in Computer Science. 4968/2008. doi:10.1007/978-3-540-68979-9_10. ISBN 978-3-540-68978-2.
  6. Sylvie Boldo; Thi Minh Tuyen Nguyen (2010). "Hardware-independent proofs of numerical programs" (PDF). Proceedings of NFM 2010.
  7. David Delmas; Stéphane Duprat; Victoria Moya Lamiel; Julien Signoles. "Taster, a Frama-C plug-in to enforce Coding Standards" (PDF). Embedded Real Time Software and Systems 2010, Toulouse, France.
  8. 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.
This article is issued from Wikipedia. The text is licensed under Creative Commons - Attribution - Sharealike. Additional terms may apply for the media files.