La critique du langage ne peut éluder ce fait que nos paroles nous engagent et que nous devons leur être fidèles.

— Albert Camus

This post was originally written for the SecOPERA project’s blog.

A crucial, but often neglected aspect of formal software evaluation process, is how we specify the properties we want to verify. Indeed, while some points are obvious, notably the fact that we don’t want the code to lead to a runtime error (or to contain undefined behaviors in C parlance), and thus do not need to be explicitly told to the analyzer, most of the properties of interest are specific to the application under analysis, and require to be explained to Frama-C, usually in the form of annotations.

More precisely, Frama-C comes with a support for the ACSL specification language, based on the notion of function contracts and logic assertions, allowing to make extremely precise statements about how the memory state of the program should look like at specific program points. Such contract-based languages are very well-known in Formal Methods, and are extremely useful to state functional properties of the program. However, there are many other kinds of properties we may be interested in, and for which ACSL is less well-suited: we could in theory express such properties, but at the price of a heavy encoding, making it more likely that an error is introduced in the specification itself. This is an important issue, since the analyzers verify that the code is conforming to the specification: if the latter is wrong, we haven’t really proved anything, even when the analysis succeeds.

This is why some Frama-C plug-ins have been developed over the year to let users write specifications in domain-specific languages and have them automatically translated into ACSL for the main analysis plug-ins to take over. We present a few of them in the remainder of this post, with their main usages and security-inspired examples. More information can be found in the slides of an invited talk at LVP Working Group’s meeting in November 2024 and in Chap. 10 of the book “Guide to Software Verification with Frama-C”.

Aoraï

Aoraï is the oldest of such plug-ins, its original version having been developed by Nicolas Stouls in 2009. It is meant to let users specify temporal properties. More precisely, an Aoraï specification is an automaton which describes the sequences of function calls that might happen during the execution of the program. As an example, we can take a very simple program, which only authorizes to use write and/or read functions after a successful login, and until logout. Furthermore, 3 failed logins will lead to the termination of the program. The corresponding automaton can be depicted as such:

Given such an automaton, Aoraï’s instrumentation works by adding code at each function’s entry and return statements that checks that we are in an admissible state, and updates this state according to the fireable transition(s).

Typestates

The Typestates plug-in is much more recent than Aoraï, being currently developed by Sébastien Patte as part of his PhD. it has been presented at the FormaliSE conference this spring. Typestates specifications also take the form of automata, but while Aoraï describes the behavior of the program as a whole, Typestates focuses on the current state of each object of a particular datatype (hence the name). The automaton above could also serve as a typestate specification (maybe replacing login/logout with open and close respectively), where the system can grant access to each file individually instead of having a single authorization step at the beginning of the program, as is the case with Aoraï.

Rpp

The Relational Property Prover (RPP) plug-in was mainly developed by Lionel Blatter during his PhD. By contrast to function contracts, that specify what a single call to a single function is supposed to do, Relational Properties describe a relation between several calls of the same function or of several functions. Security-wise, non-interference represents an important class of relational properties: to establish non-interference, one has to split memory into a public and a private part, and to show that if two calls to the function f are done in two memory states where the public locations have the same content (but the private part might be different), then the public part of the memory will also be the same when the calls return, so that an attacker could not gain information about the private content by inspecting the public result.

The current implementation of Rpp uses a technique called self-composition, generating a wrapper function that simulates the calls to the function(s) involved in the relational property, and a plain ACSL contract for this wrapper whose validity implies the validity of the relational property in the first place. A more flexible method has been proposed, but remains to be implemented.

MetAcsl

Finally, the MetAcsl plug-in was mainly developed by Virgile Robles during his PhD. The goal of this plug-in is to provide a compact way to write pervasive properties that need to be checked at many program points. In MetAcsl, such properties are called HILAREs (High-Level ACSL Requirements) and are defined by three ingredients: their target, that is the set of functions where the property must hold, their context, defining the exact points where a verification must occur, and the actual property, expressed as an ACSL predicate that, depending on the context, may use one or more meta-variables. The two most important contexts are writing, denoting all write accesses and allowing to state integrity properties, and reading, denoting all read accesses and allowing to state confidentiality properties. An HILARE with writing (resp. reading) context can use the meta-variable written (resp. read) to denote the corresponding location. A typical integrity-related HILARE would state that for any write access in any function other than write_confidential_data, the written location is not within the confidential_data array. More patterns of HILARE for common kinds of properties have been proposed, and MetAcsl has played an important role in the certification of Thales’ JavaCard Virtual Machine at the highest Evaluation Assurance Level (EAL7) of the Common Criteria. The instrumentation performed by MetAcsl simply amounts to instantiating the HILAREs at each program point designated by the target and the context, and substituting the meta-variables by the relevant terms.

Conclusion

There are thus many ways of specifying your properties of interest and have them verified by Frama-C without resorting to a cumbersome and error-prone manual encoding in plain ACSL. However, this does not completely settle the question of whether what you specified is what you meant: what if there’s a bug in one of the plug-ins? While there’s no definitive answer yet, several works have made good progress in this direction.

• For Typestates, the FormaliSE article describes a formalization of the transformation made by the plug-in for a small (but significant) subset of C, using the Skel framework.
• For RPP, the new verification mechanism has been fully proved in Coq (now the Rocq Prover), again for a subset of C.
• For MetAcsl, a Why3 model of the instantiation mechanism based on the control-flow graph of the program has been developed and is used as a basis for performing deduction at meta-level instead of always resorting to ACSL instantiations, as described in a paper from ISoLA 2024.
• Finally, a longer-term goal is to have a complete mechanized semantics of ACSL itself as a basis for formalizing the whole transformations. Louis Gauthier’s PhD work, presented at FormaliSE’24, is paving the way for that.