-16th Nov 2020
+Monday 16th Nov 2020
Formally proving tiny bits of qemu using Frama-C
-[in medias res]
+\f
In early October I was talking to one of the developers of Frama-C,
which is a modular framework for verifying C programs. It's been on
I will provide links to tutorials etc at the end.
-I decided to spend a day or two seeing if I could formally prove some
-production code inside qemu, and I arbitrarily picked one of the
+\f
+= OVERVIEW OF FRAMA-C ECOSYSTEM =
+
+The name stands for "Framework for Static Analysis of the C language".
+
+It's modular, with a core program that reads C source code
+and turns it into Abstract Syntax Trees. And a set of plugins
+to do static analysis by annotating these syntax trees.
+Plugins can cooperate, so analysis can be passed between
+plugins.
+
+The following slides are taken from David Mentré‘s 2016 presentation.
+
+\f
+I decided to spend a day or two last month seeing if I could formally
+prove some code inside qemu, and I arbitrarily picked one of the
smallest pieces of code in the "util/" subdirectory:
$ wc -l util/*.c | sort -nr | tail -20
$ ls -l util/range.c include/qemu/range.h
-This is what the Range type looks like. This is the complete
-definition upstream, with comments which are supposed to explain how
-it works:
+This is what the Range type from the header file looks like. This is
+the complete definition upstream, with comments which are supposed to
+explain how it works:
/*
* Operations on 64 bit address ranges.
- I'm using structs directly from the C code.
- - The comments in the upstream code translate into predicates.
+ - The upstream comments translate into machine-checkable code.
The first upstream function is:
and using the predicates we can write a specification:
- /* Is range empty? */
- /*@
- requires \valid_read(range);
- requires valid_range(*range);
- assigns \nothing;
- ensures \result <==> empty_range(*range);
- */
- static inline bool range_is_empty(const Range *range)
- {
- return range->lob > range->upb;
- }
+ $ cat snippets/range_is_empty.c
And we can compile and prove that:
Frama-C parsed the C code and the formal specification and machine
checked it, and it's correct - the code is bug-free.
-= OVERVIEW OF FRAMA-C ECOSYSTEM =
-
-
-XXX Modular Framework for analysis of C
-
-XXX Take some slides from David Mentre's presentation.
-
-XXX Explain which companies are using Frama-C.
-
-XXX WP plugin
-
-XXX ACSL language
-
-
-
-= BACK TO RANGE.C =
-
+\f
Going back to what we proved so far:
/*@
predicate valid_range(struct Range range) =
range.lob <= range.upb + 1;
-
predicate empty_range(struct Range range) =
range.lob == range.upb + 1;
*/
}
$ frama-c -wp -wp-rte snippets/range_is_empty.c
- XXX OUTPUT OF FRAMA-C XXX
The "@"-comments are ACSL. The C code is parsed by Frama-C into an
abstract syntax tree. We told Frama-C to apply the WP plugin. The
- Given those assumptions, the code is bug free - you don't need to
write any tests.
+\f
Obviously this is a single line, very trivial function, but I was
quite pleased that I was able to prove it quickly. I kept going on
the range file. The next function is:
return val >= range->lob && val <= range->upb;
}
+\f
The next function is range_make_empty, again easy to prove using the
already existing empty_range predicate. Notice how we declare which
memory locations this function assigns to:
assert(range_is_empty(range));
}
+\f
I'm going to skip forward a few functions to get to an interesting one.
This seems trivial:
Let's try to prove this one:
- $ frama-c ... snippets/range_size.c
- XXX It fails!
+ $ frama-c -wp -wp-rte snippets/range_size.c
+ It fails!
This was confusing to me because at this point I'd probably spent an
hour, and I'd proven about 5 functions successfully, and this function
One way to find the problem would be to find a COUNTEREXAMPLE. A
counterexample is an instance of an input that satisfies all of the
-preconditions, but makes the postcondition false. Now Frama-C has
+preconditions, but makes the postcondition false. Frama-C has
pluggable provers, and one prover called Z3, originally written by
Microsoft, can be used with Frama-C and can sometimes find
-counterexamples. However for some reason the version of Z3 in Fedora
-does not like to work with the version of Frama-C in Fedora and I
-don't know why.
+counterexamples.
+
+ $ frama-c -wp -wp-rte snippets/range_size.c -wp-prover alt-ergo,why3:z3-ce
+
+Unfortunately Z3 cannot find a counterexample in this case. I even
+upped the timeout to run Z3 longer but it still couldn't find one.
+
+[Z3 model_compact issue: https://git.frama-c.com/pub/frama-c/-/issues/33]
So this is the counterexample which I worked out myself:
return range->upb - range->lob + 1;
}
+ $ frama-c -wp -wp-rte snippets/range_size-good.c
+
+\f
On to the next function. Again this seems very simple, but in fact it
contains a serious problem:
/*@ // after:
predicate empty_range(struct Range range) =
range.lob > 0 && range.lob == range.upb + 1;
+
+ predicate total_range(struct Range range) =
+ range.lob == 0 && range.upb == UINT64_MAX;
*/
What can we say about this? If you were developing the Range type and
- It probably doesn't make sense for qemu right now though, unless we
could prove more substantial pieces of code.
+\f
= POWER OF 2 =
This is a function from nbdkit:
Essentially bitwise tricks like this are a hard case for automated
theorem proving. I gave up.
+\f
= TIMEVAL DIFFERENCE =
This is another nbdkit function:
int64_t *r)
...
-
and of course that is not sufficient because I also had to fix the
code so it can return an overflow indication. And actually writing
that code is left as an exercise for the reader as it is not at all
understand them. We could contribute these to the Frama-C standard
library.
+\f
+= STRING FUNCTIONS =
+
+Uli sent me this function from glibc:
+ [https://sourceware.org/git/?p=glibc.git;a=blob;f=string/strverscmp.c]
+To be honest I had problems even fully understanding the semantics of
+this function, let alone trying to translate that into ACSL.
+So I thought I'd look at a simpler function:
+ [https://sourceware.org/git/?p=glibc.git;a=blob;f=string/strlen.c]
+I want to point out first that this "strlen" is a fallback which is
+only used if you don't have an optimized function for your hardware,
+and for the vast majority of users they'll be using something like an
+AVX-optimized strlen, not this one.
+This function works in two halves, the first part iterates over single
+characters until we reach an aligned boundary. And then the second
+part looks at whole words and uses a clever trick to determine if any
+byte in the word is zero.
+In theory a simple specification which would apply to any strlen-style
+function would be:
+
+ /*@
+ requires valid_read_string (str);
+ assigns \nothing;
+ ensures (\forall integer i; 0 <= i < \result ==> str[i] != '\0') &&
+ str[\result] == '\0';
+ */
+ size_t strlen (const char *str)
+ {
+ ...
+
+It would be possible to use this to prove a simple strlen
+implementation that just worked character by character.
+
+Unfortunately for the actual glibc function we hit another limitation
+of the WP plugin, called the Typed Memory Model.
+
+WP models memory as a set of cells, with a type attached to each cell.
+So a string for example is a set of char cells, each cell being typed
+as char. You cannot cast these cells to something like a word and try
+to do a proof over that. Simply a limitation which is well
+documented.
+
+So a proof of the glibc function eludes me.
+
+\f
+There is a set of open source licensed string functions with Frama-C
+proofs available:
+
+https://github.com/evdenis/verker
+
+and this is what the strlen function with proof looks like from that:
+
+ [https://github.com/evdenis/verker/blob/master/src/strlen.c]
+
+\f
+Now you might be asking what happens when you write a function that
+uses strlen, for example this trivial function with a working
+specification:
+
+ $ cat snippets/last_char.c
+ $ frama-c -wp -wp-rte snippets/last_char.c
+
+The questions here are:
+
+ - Is this proving the glibc strlen function?
+
+ - Are we calling glibc strlen() from the specification?
+
+ $ less /usr/share/frama-c/libc/string.h
+ $ less /usr/share/frama-c/libc/__fc_string_axiomatic.h
+
+And the answers are no and no. In fact what's happening here is we
+are using Frama-C's own "string.h" header. This header defines and
+contains a specification for how strlen. But this is also not a proof
+of strlen: in fact a second file defines what's known as an "axiomatic
+definition" or theory of how strlen works.
+
+Essentially what's happening is we're assuming that strlen in your
+standard library (which might not even be glibc) works. To make a
+complete proof you'd also need to additionally prove all libraries you
+depend on.
+
+Another little fun thing is Frama-C's strlen function can return -1,
+which is used to represent an unbounded string. Of course unbounded
+strings cannot exist on real computers, but they can exist on
+theoretical ones!
+
+\f
= IN CONCLUSION =
* Frama-C is a real open source tool used by companies to verify
* Not as hard to use as I imagined. I spent about 6-12 hours from
zero to being able to fully prove a whole file of production code.
- (But I did study logic under Prof Crispin Wright at university).
* Mostly useful for small functions. There are other tools, like TLA+
for proving distributed algorithms.
* Not good at bitwise ops (can Z3 help?).
* Cannot parse some non-standard __attribute__s (glib).
+
+* Lacks some __builtin_* functions.
+
+Alternatives and related programs:
+
+* Ada SPARK Pro (https://www.adacore.com/sparkpro) is a formally
+ verified subset of the Ada programming language
+ (tagline: "You simply can't write better code").
+
+* KLEE (http://klee.github.io/) has similarities but is not a formal
+ proof system.
+
+* CompCert (http://compcert.inria.fr/) is INRIA's verified C compiler
+ (not open source).
+
+Resources:
+
+* Tutorial that I followed in October which I thought was a good
+ introduction:
+ https://maniagnosis.crsr.net/2017/06/AFL-brute-force-search.html
+ https://maniagnosis.crsr.net/2017/06/AFL-bug-in-quicksearch.html
+ https://maniagnosis.crsr.net/2017/07/AFL-correctness-of-quicksearch.html
+
+* Frama-C on Stack Overflow:
+ https://stackoverflow.com/questions/tagged/frama-c
+
+* Allan Blanchard's tutorial:
+ https://allan-blanchard.fr/publis/frama-c-wp-tutorial-en.pdf
+
+* David Mentre's introduction:
+ https://www.cs.umd.edu/class/spring2016/cmsc838G/frama-c/introduction-to-frama-c_v2.pdf
+
+* Upstream documentation:
+ Manual: https://frama-c.com/download/frama-c-user-manual.pdf
+ WP manual: https://frama-c.com/download/frama-c-wp-manual.pdf
+ ACSL: https://frama-c.com/acsl.html
+
+* ACSL specifications for various string functions:
+ https://github.com/evdenis/verker
git.annexia.org / libguestfs-talks.git / blobdiff