Frama-C with wp-dynamic and function pointers

Introduction

Just as a reminder: What is static analysis and what does Frama-C and the weakest precondition (wp) plugin provide? Static analysis is an approach of analysing sourcecode and verify given behavior or extract information out of program code and the specified behaviour of the programming language. Static analysis can be used to reason about program behavior, learn about program flow and value analysis, it can be used to slice programs so one can extract a sub program that’s valid for a given set of parameters. Most of the time static analysis is used in conjunction with other test frameworks and analysis methods like debuggers, unit testing frameworks, memory leak checkers like valgrind, automated test frameworks, etc. Some of the more commonly used static analyzers are for example the clang sanitizers that are capable of catching invalid memory accesses, possible NULL dereferencing, accessing invalid array indices, memory leaks, problematic casts, undefined behaviour of C++ library calls, etc. - a list of currently supported static analyzers of clang can be seen at the clang analyzer documentation.

The other more often used static analyzer is the Frama-C framework. This tool consists of a myriad of functions as well. The tool can calculate call graphs, perform value analysis and compute dominators, can document and analyze functional dependencies, do impact analysis and program slicing, is capable of calculating various metrics, is capable of dead code detection and removal, etc. One of the most interesting features is the capability of doing runtime error annotation (RTE) that automatically generates ACSL annotations to catch undefined behaviour of the C language (for example accessing undefined memory locations, problematic numeric stuff like impossible mulitplication, etc.) and to evaluate own ACSL annotations that describe the desired behaviour of a function to guarantee that a function really does what the annotation claims it should do under all circumstances - these annotations are then verified by the weakest precondition module using the weakest precondition predicate transformer (i.e. basically Hoare logic). If the analyzer proofs that a program behaves like specified one can trust that - as long as the hardware and the compiler follows the specification - the application behaves strictly as specified and does not contain any undefined behavior. The last gap towards full verification can be bridged using verified compilers like CompCert and hardware like the RISC-V architecture and it’s formal specification.

Just as a word of caution: Developing using formal verification is really way slower than just hacking around by an order of magnitude and is really hard to get started (especially for complex programs that go beyond adding numbers, performing numerical calculations or simple sorting) - but if offers guarantees that cannot be made in any other way - i.e. a correctness proof of your software. If it’s possible and one wants to take that route one should start annotating functions from the early beginning of product development - and use the least possible amount of libraries since one would also have to annotate them too (if they aren’t already). This is definitely a huge amount of work.

Function pointers and wp-dynamic

Till recently (Frama-C 20 - Calcium) formal verification has had some problems when verifying behaviour / formally proofing behaviour of ANSI C programs when using function pointers. Since function pointers are an essential element of ANSI C that posed a huge limitations on which type of programs could be verified using Frama-C. I’ve used this static analysis tool to proof behaviour of microcontroller code and some math libraries as well as non hierarchical serializers and deserializers I’ve written. It also proofed to be really effective to discover possible bugs, undefined behaviour as well as accuracy or rounding errors in math code.

To solve that problem there has been an feature introduced in Frama-C that helps to verify code that uses function pointers. This includes an unofficial extension to ACSL, so the ACSL is not standards conformant any more when using these annotations. In many cases Frama-C is capable of determining which functions are called from following the program flow and is capable of deducing the Hoare tripples for the called functions when analyzing whole programs. This is a somewhat different situation when verifying libraries or under some more exotic cases. Then one needs to tell Frama-C which functions will be called (or at least provide a list of functions that have the same behaviour as expected from application functions when developing libraries).

One should always try to simply enable -wp-dynamic for the wp module without any modification at first.

When one now has a function pointer definition like

typedef int (*MyAdderFunction)(int a, int b);

with one or more implementation

/* Adder on the finite field of int */
/*@
    // some annotation
*/
int AdderFun1(int a, int b) { return a + b; }

/* Adder on a finite field of 256 elements */
/*@
    // some annotation
*/
int AdderFun2(int a, int b) { return (a + b) % 256; }

and one uses a function like

void testfun(MyAdderFunction lpfnAdder) {
    int result = lpfnAdder(1, 2);
}

One can add an @calls Annotation to tell frama-c which functions will be called by this function.

void testfun(MyAdderFunction lpfnAdder) {
    /*@
        calls AdderFun1, AdderFun2;
    */
    int result = lpfnAdder(1, 2);
}

When one then runs Frama-C using -wp and -wp-dynamic the weakest precondition module is now capable of validating that all requirements of the called functions are satisfied by the testfun function and check if all assumptions and requirements imposed by the function are fulfilled by the various functions pointed at.

Note that Frama-C ill still stry to trace any called functions when analyzing whole programs.

When moving to a new Frama-C version do not forget that one might has to enable a proof assistant first.

Obstacles while installing Frama-C Calcium on FreeBSD

Note that it’s pretty helpful to have the (at the time of writing way outdated) port at devel/frama-c already installed on the local machine to meet any binary dependencies.

As usual with software with long dependency chains and it’s own package manager installation of Frama-C wasn’t really flawless. Installation of all dependencies and Frama-C itself nearly works - the installation of the alt-ergo-lib OPAM package fails because of a - in my opinion - really really bad habit of the package author. The author referenced #!/bin/bash for a simple POSIX compliant shell script - because of this the build process of the whole package failed. Patching the configure shellscript to use the #!/bin/sh shell or temporarily symlinking /bin/bash to sh using ln -s /bin/bash /bin/sh solves that problem. Note that this is an common portability issue when porting software developed on Linux to other POSIX compliant Unix (or Unix based) systems. And it’s unnecessary. Please don’t do that. Write scripts using standards conformant #!/bin/sh

Besides that one simply requires devel/ocaml-opam package or port installed via

pkg install devel/ocaml-opam

or

cd /usr/ports/devel/ocaml-opam
make install clean

and then one can install the current version of Frama-C using

opam init
opam install frama-c

This will pull all necessary dependencies into a local opam switch (i.e. a virtual environment). To use everything installed one just has to execute the eval `opam env` command.

It might be necessary to create a new OPAM switch or upgrade the currently used switch if the local ocaml installation is too old. If one derived the current switch from the system opam from packages or ports one might simply want to upgrade to initial switch.

opam upgrade --unlock-base opam

After installation of frama-c one has to configure why3:

why3 config --detect-provers

This should detect alt-ergo as proof assistant and store this configuration inside the ~/.why3.conf configuration file.

One might be required to run frama-c while setting the FRAMAC_SHARE environment variable to ~/.opam/default/share/frama-c/. When running the UI one might use

env FRAMAC_SHARE=~/.opam/default/share/frama-c/ frama-c-gui

The same might be used when running frama-c from the CLI. When running from any automated build solution like a Makefile or from a Jenkinsfile one should solve that environment problem globally from any bootstrap scripts that initialized these environments.

Installation scripts used

The following scripts are used on my FreeBSD build cluster and workstation machines to deploy Frama-C 20.0 (Calcium) in this specific version - the deployment takes approx. 10 minutes to complete:

#!/bin/sh

# Fix broken scripts that use /bin/bash in shebang line
if [ ! -e /bin/bash ]; then
	RESTOREBASH=1
	ln -s /bin/sh /bin/bash
else
	RESTOREBASH=0
fi

pkg install gmake pkgconf autoconf gmp gtksourceview2 graphviz libgnomecanvas

# First update OPAM repository and create
# a new switch using ocaml 4.10.0

opam update
opam switch create framac20 4.10.0
eval $(opam env)
opam install frama-c.20.0

why3 config --detect-provers

# Restore expected behaviour ...
if [ ${RESTOREBASH} -eq 1 ]; then
	rm /bin/bash
fi

Frama-C is launched by me using the following script when one requests the GUI on workstations:

#!/bin/sh
opam switch framac20
eval $(opam env)
env FRAMAC_SHARE=${HOME}/.opam/framac20/share/frama-c frama-c-gui

And using the following script when running from the CLI:

#!/bin/sh
opam switch framac20
eval $(opam env)
env FRAMAC_SHARE=${HOME}/.opam/framac20/share/frama-c frama-c "$@"

This article is tagged: Programming, Math, Formal, Security, Frama C