2 Formally proving tiny bits of qemu using Frama-C
6 In early October I was talking to one of the developers of Frama-C,
7 which is a modular framework for verifying C programs. It's been on
8 my radar to learn for a long time, and I'm a co-maintainer of the
9 package in Fedora. I tried to follow one tutorial but never really
10 got past installation and UI issues. But the developer pointed me to
11 a very good, short set of blog postings about using the command line
14 I will provide links to tutorials etc at the end.
16 I decided to spend a day or two last month seeing if I could formally
17 prove some code inside qemu, and I arbitrarily picked one of the
18 smallest pieces of code in the "util/" subdirectory:
20 $ wc -l util/*.c | sort -nr | tail -20
22 Actually there are two files:
24 $ ls -l util/range.c include/qemu/range.h
26 This is what the Range type from the header file looks like. This is
27 the complete definition upstream, with comments which are supposed to
31 * Operations on 64 bit address ranges.
33 * - Ranges must not wrap around 0, but can include UINT64_MAX.
37 * Do not access members directly, use the functions!
38 * A non-empty range has @lob <= @upb.
39 * An empty range has @lob == @upb + 1.
41 uint64_t lob; /* inclusive lower bound */
42 uint64_t upb; /* inclusive upper bound */
44 typedef struct Range Range;
46 +-----------+-----------+------------- - - - - -
48 +-----------+-----------+------------- - - - - -
52 Using the tutorial as my guide I wrote some simple predicates, a
53 "predicate" being a statement which can be true or false:
55 * A non-empty range has @lob <= @upb.
56 * An empty range has @lob == @upb + 1.
59 predicate valid_range(struct Range range) =
60 range.lob <= range.upb + 1;
62 predicate empty_range(struct Range range) =
63 range.lob == range.upb + 1;
66 Notice a few things here:
68 - These are statements written in a formal language.
70 - I'm using structs directly from the C code.
72 - The comments in the upstream code translate into predicates.
74 The first upstream function is:
77 static inline bool range_is_empty(const Range *range)
79 return range->lob > range->upb;
82 and using the predicates we can write a specification:
84 $ less snippets/range_is_empty.c
86 And we can compile and prove that:
88 $ frama-c -wp -wp-rte snippets/range_is_empty.c
90 Frama-C parsed the C code and the formal specification and machine
91 checked it, and it's correct - the code is bug-free.
93 = OVERVIEW OF FRAMA-C ECOSYSTEM =
96 XXX Modular Framework for analysis of C
98 XXX Take some slides from David Mentre's presentation.
100 XXX Explain which companies are using Frama-C.
110 Going back to what we proved so far:
113 predicate valid_range(struct Range range) =
114 range.lob <= range.upb + 1;
115 predicate empty_range(struct Range range) =
116 range.lob == range.upb + 1;
119 /* Is range empty? */
121 requires \valid_read(range);
122 requires valid_range(*range);
124 ensures \result <==> empty_range(*range);
126 static inline bool range_is_empty(const Range *range)
128 return range->lob > range->upb;
131 $ frama-c -wp -wp-rte snippets/range_is_empty.c
133 The "@"-comments are ACSL. The C code is parsed by Frama-C into an
134 abstract syntax tree. We told Frama-C to apply the WP plugin. The
135 specification and C code were translated into first-order logic
136 statements and passed to the Alt-Ergo SMT prover to see if it could
137 find a Proof Obligation (PO).
139 We need to be very clear about what happened:
141 - The preconditions must be fulfilled in order for the proof to be
142 correct. If you are checking a whole program then that would check
143 that all callers of this function are fulfilling the preconditions,
144 but if you check only single functions then you are not doing that.
146 - The proof only shows that the post-condition holds.
148 - This only shows that the source code is correct. The compiler
149 could still compile the program incorrectly. If you really want to
150 get into this you have to use a verified C compiler like CompCert,
151 and there are even verified CPU implementations.
153 - Given those assumptions, the code is bug free - you don't need to
156 Obviously this is a single line, very trivial function, but I was
157 quite pleased that I was able to prove it quickly. I kept going on
158 the range file. The next function is:
160 /* Does range contain val? */
161 static inline bool range_contains(const Range *range, uint64_t val)
163 return val >= range->lob && val <= range->upb;
166 This is similarly easy to prove after adding another predicate at the
170 predicate value_in_range(struct Range range, uint64_t value) =
171 range.lob <= value <= range.upb;
174 /* Does range contain val? */
176 requires \valid_read(range);
177 requires valid_range(*range);
179 ensures \result <==> value_in_range(*range, val);
181 static inline bool range_contains(const Range *range, uint64_t val)
183 return val >= range->lob && val <= range->upb;
186 The next function is range_make_empty, again easy to prove using the
187 already existing empty_range predicate. Notice how we declare which
188 memory locations this function assigns to:
190 /* Initialize range to the empty range */
192 requires \valid(range);
193 requires valid_range(*range);
195 ensures empty_range(*range);
197 static inline void range_make_empty(Range *range)
199 *range = range_empty;
200 assert(range_is_empty(range));
203 I'm going to skip forward a few functions to get to an interesting one.
206 /* Get the size of range. */
207 static inline uint64_t range_size(const Range *range)
209 return range->upb - range->lob + 1;
212 My first attempt at a proof was:
215 logic integer size_of_bounds(integer lob, integer upb) =
218 logic integer size_of_range(struct Range range) =
219 size_of_bounds(range.lob, range.upb);
222 /* Get the size of range. */
224 requires \valid(range);
225 requires valid_range(*range);
227 ensures \result == size_of_range(*range);
229 static inline uint64_t range_size(const Range *range)
231 return range->upb - range->lob + 1;
234 A few things to notice about this:
236 - I'm using ACSL "logic" statements, which are similar to functions.
238 - ACSL has an "integer" type which is an unbounded integer.
240 Let's try to prove this one:
242 $ frama-c -wp -wp-rte snippets/range_size.c
245 This was confusing to me because at this point I'd probably spent an
246 hour, and I'd proven about 5 functions successfully, and this function
247 looks equally trivial and yet it cannot be proven. Why?
249 One way to find the problem would be to find a COUNTEREXAMPLE. A
250 counterexample is an instance of an input that satisfies all of the
251 preconditions, but makes the postcondition false. Now Frama-C has
252 pluggable provers, and one prover called Z3, originally written by
253 Microsoft, can be used with Frama-C and can sometimes find
254 counterexamples. However for some reason the version of Z3 in Fedora
255 does not like to work with the version of Frama-C in Fedora and I
258 So this is the counterexample which I worked out myself:
261 logic integer size_of_bounds(integer lob, integer upb) =
264 logic integer size_of_range(struct Range range) =
265 size_of_bounds(range.lob, range.upb);
268 /* Get the size of range. */
270 requires \valid(range);
271 requires valid_range(*range);
273 ensures \result == size_of_range(*range);
275 static inline uint64_t range_size(const Range *range)
277 return range->upb - range->lob + 1;
280 +-------------------------------------------------------+
281 |XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX|
282 +-------------------------------------------------------+
283 range->lob == 0 range->upb == UINT64_MAX
285 In this case size_of_range() returns an integer. Recall that integers
286 are an unbounded type. So it returns UINT64_MAX + 1 (a 65 bit
287 number). Our C function on the other hand returns 0.
289 This is a bug in the function. There are really two ways to
292 (1) The function shouldn't be called on empty ranges (size 0), and so
293 if the function returns 0 it means "the total range". Or:
295 (2) The function should have a different signature so it can return a
296 separate indication for "empty range" vs "total range".
298 I went with the first, so the final working specification is this. If
299 we were proving the entire program then we could statically verify
300 that callers do not try to call range_size() on the empty range.
303 requires \valid(range);
304 requires valid_range(*range);
305 requires !empty_range(*range);
307 // case UINT64_MAX+1 -> 0
308 ensures \result == (uint64_t)size_of_range(*range);
310 static inline uint64_t range_size(const Range *range)
312 return range->upb - range->lob + 1;
315 $ frama-c -wp -wp-rte snippets/range_size-good.c
317 On to the next function. Again this seems very simple, but in fact it
318 contains a serious problem:
321 * Initialize range to span the interval [lob,lob + size - 1].
322 * size may be 0. Range must not overflow.
324 static inline void range_init_nofail(Range *range, uint64_t lob,
328 range->upb = lob + size - 1;
331 What does lob == 0, size == 0 mean? It will create a total range.
333 +-------------------------------------------------------+
334 |XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX|
335 +-------------------------------------------------------+
336 range->lob == 0 range->upb == UINT64_MAX
338 What does lob == 1, size == 0 mean? It will create an empty range.
340 Because I didn't want to change the code, that makes the proof very
341 long, and it demonstrates another feature of ACSL specifications
345 requires \valid(range);
346 requires lob + (integer)size <= UINT64_MAX;
349 assumes lob > 0 && size == 0;
350 ensures empty_range(*range);
353 ensures range->lob == lob;
354 ensures size_of_bounds(lob, range->upb) == size;
356 assumes lob == 0 && size == 0;
357 ensures total_range(*range);
362 I also had to modify my earlier empty_range predicate:
365 predicate empty_range(struct Range range) =
366 range.lob == range.upb + 1;
370 predicate empty_range(struct Range range) =
371 range.lob > 0 && range.lob == range.upb + 1;
373 predicate total_range(struct Range range) =
374 range.lob == 0 && range.upb == UINT64_MAX;
377 What can we say about this? If you were developing the Range type and
378 the proof at the same time, you probably wouldn't define the Range
379 type in this way, and you probably wouldn't choose an initialization
380 function which had this complex set of behaviours.
382 I did prove most of the rest of the Range functions, but I wanted to
383 point out a few things about the final proof:
385 - The original file includes glib headers, but those cannot be parsed
386 by Frama-C's parser. The problem appears to be some unsupported
387 __attribute__s. Some attributes seem to work, and others are not
388 supported, and this of course limits what you can prove if it
389 depends on any external library that might use these.
391 - For the same reason I had to exclude a glib function for operating
392 on lists of ranges from the proof.
394 - You can run frama-c on the original source file, with a few #ifdef
395 modifications, so it would be possible to maintain the annotations
396 upstream, and run the proof checker as a CI test.
398 - It probably doesn't make sense for qemu right now though, unless we
399 could prove more substantial pieces of code.
403 This is a function from nbdkit:
405 /* Returns true if v is a power of 2.
407 * Uses the algorithm described at
408 * http://graphics.stanford.edu/~seander/bithacks.html#DetermineIfPowerOf2
411 is_power_of_2 (unsigned long v)
413 return v && ((v & (v - 1)) == 0);
416 and my initial specification started by defining:
419 predicate positive_power_of_2 (integer i) =
421 (i == 1 || ((i & 1) == 0 && positive_power_of_2 (i >> 1)));
423 lemma positive_power_of_2 (1);
424 lemma positive_power_of_2 (2);
425 lemma positive_power_of_2 (4);
426 lemma !positive_power_of_2 (7);
429 I was using the lemmas (which are like assertions, except statically
430 verified), to test my predicate, but sadly Frama-C was not able to
431 prove them even though they appear to be trivial.
433 This led to some discussion on stackoverflow:
435 https://stackoverflow.com/questions/64268418/how-do-i-write-an-is-power-of-2-predicate-in-acsl
437 Ultimately it was possible to fix this, but I discovered a few things
438 about Alt-Ergo (the default prover):
440 - It can't handle bitwise operations very well.
442 - You can guide Alt-Ergo, but it requires using the Frama-C GUI which
443 is very non-intuitive. You do end up with a script but I couldn't
444 work out how to integrate this with the command line.
446 - Z3 should be able to solve this, but I was not able to get
447 Z3 working with Frama-C on Fedora.
449 Essentially bitwise tricks like this are a hard case for automated
450 theorem proving. I gave up.
452 = TIMEVAL DIFFERENCE =
454 This is another nbdkit function:
456 /* Return the number of µs (microseconds) in y - x. */
457 static inline int64_t
458 tvdiff_usec (const struct timeval *x, const struct timeval *y)
462 usec = (y->tv_sec - x->tv_sec) * 1000000;
463 usec += y->tv_usec - x->tv_usec;
467 My first attempt at a proof was:
470 predicate valid_timeval (struct timeval tv) =
471 tv.tv_sec >= 0 && tv.tv_usec >= 0 && tv.tv_usec < 1000000;
472 logic integer tv_to_microseconds (struct timeval tv) =
473 tv.tv_sec * 1000000 + tv.tv_usec;
476 /* Return the number of µs (microseconds) in y - x. */
478 requires \valid_read (x) && \valid_read (y);
479 requires valid_timeval (*x) && valid_timeval (*y);
480 ensures \result == tv_to_microseconds (*y) - tv_to_microseconds (*x);
482 static inline int64_t
483 tvdiff_usec (const struct timeval *x, const struct timeval *y)
487 usec = (y->tv_sec - x->tv_sec) * 1000000;
488 usec += y->tv_usec - x->tv_usec;
492 This is not provable, and again the problem is integer overflow. The
493 tv_sec field is a 64 bit integer so it's quite easy to construct two
494 inputs which overflow the output.
496 Fixing this involves a considerably more complex specification:
499 requires \valid_read (x) && \valid_read (y);
500 requires valid_timeval (*x) && valid_timeval (*y);
504 ensures \result == 0;
505 ensures \let diff = tv_to_microseconds (*y) - tv_to_microseconds (*x);
506 INT64_MIN <= diff <= INT64_MAX &&
509 ensures \result == -1;
511 ensures \let diff = tv_to_microseconds (*y) - tv_to_microseconds (*x);
512 !(INT64_MIN <= diff <= INT64_MAX);
517 tvdiff_usec (const struct timeval *x, const struct timeval *y,
521 and of course that is not sufficient because I also had to fix the
522 code so it can return an overflow indication. And actually writing
523 that code is left as an exercise for the reader as it is not at all
526 A few things I learned from this:
528 - This is a function we have had and used for years, and I don't
529 think anyone ever thought it had a problem.
531 - Co-developing the specification alongside the code could help
534 - You can end up with functions that are much harder to use. If we
535 were proof-checking the whole program we could check all callers.
537 - GCC has __builtin_add_overflow and similar which can be used to do
538 mathematical operations and detect overflow, but Frama-C does not
539 understand them. We could contribute these to the Frama-C standard
544 Uli sent me this function from glibc:
546 [https://sourceware.org/git/?p=glibc.git;a=blob;f=string/strverscmp.c]
548 To be honest I had problems even fully understanding the semantics of
549 this function, let alone trying to translate that into ACSL.
551 So I thought I'd look at a simpler function:
553 [https://sourceware.org/git/?p=glibc.git;a=blob;f=string/strlen.c]
555 I want to point out first that this "strlen" is a fallback which is
556 only used if you don't have an optimized function for your hardware,
557 and for the vast majority of users they'll be using something like an
558 AVX-optimized strlen, not this one.
560 This function works in two halves, the first part iterates over single
561 characters until we reach an aligned boundary. And then the second
562 part looks at whole words and uses a clever trick to determine if any
563 byte in the word is zero.
565 In theory a simple specification which would apply to any strlen-style
569 requires valid_read_string (str);
571 ensures (\forall integer i; 0 <= i < \result ==> str[i] != '\0') &&
572 str[\result] == '\0';
574 size_t strlen (const char *str)
578 It would be possible to use this to prove a simple strlen
579 implementation that just worked character by character.
581 Unfortunately for the actual glibc function we hit another limitation
582 of the WP plugin, called the Typed Memory Model.
584 WP models memory as a set of cells, with a type attached to each cell.
585 So a string for example is a set of char cells, each cell being typed
586 as char. You cannot cast these cells to something like a word and try
587 to do a proof over that. Simply a limitation which is well
590 So a proof of the glibc function eludes me.
592 There is a set of open source licensed string functions with Frama-C
595 https://github.com/evdenis/verker
597 and this is what the strlen function with proof looks like from that:
599 [https://github.com/evdenis/verker/blob/master/src/strlen.c
601 Now you might be asking what happens when you write a function that
602 uses strlen, for example this trivial function with a working
605 $ cat snippets/last_char.c
606 $ frama-c -wp -wp-rte snippets/last_char.c
608 The questions here are:
610 - Is this proving the glibc strlen function?
612 - Are we calling glibc strlen() from the specification?
614 $ less /usr/share/frama-c/libc/string.h
615 $ less /usr/share/frama-c/libc/__fc_string_axiomatic.h
617 And the answers are no and no. In fact what's happening here is we
618 are using Frama-C's own "string.h" header. This header defines and
619 contains a specification for how strlen. But this is also not a proof
620 of strlen: in fact a second file defines what's known as an "axiomatic
621 definition" or theory of how strlen works.
623 Essentially what's happening is we're assuming that strlen in your
624 standard library (which might not even be glibc) works. To make a
625 complete proof you'd also need to additionally prove all libraries you
628 Another little fun thing is Frama-C's strlen function can return -1,
629 which is used to represent an unbounded string. Of course unbounded
630 strings cannot exist on real computers, but they can exist on
635 * Frama-C is a real open source tool used by companies to verify
636 safety-critical software. If you've flown in an Airbus or used
637 electricity from a French nuclear power plant then you've used this
640 * Not as hard to use as I imagined. I spent about 6-12 hours from
641 zero to being able to fully prove a whole file of production code.
643 * Mostly useful for small functions. There are other tools, like TLA+
644 for proving distributed algorithms.
646 * Forces you to think very hard about assumptions and corner cases,
647 but that's the nature of the problem.
649 * Very well documented, questions answered quickly on stackoverflow.
651 But it has its limits:
653 * Typed Memory Model turns out to be restrictive.
655 * No support for malloc.
657 * Not good at bitwise ops (can Z3 help?).
659 * Cannot parse some non-standard __attribute__s (glib).
661 * Lacks some __builtin_* functions.
663 Alternatives and related programs:
665 * Ada SPARK Pro (https://www.adacore.com/sparkpro) is a formally
666 verified subset of the Ada programming language
667 (tagline: "You simply can't write better code").
669 * KLEE (http://klee.github.io/) has similarities but is not a formal
672 * CompCert (http://compcert.inria.fr/) is INRIA's verified C compiler
677 * Tutorial that I followed in October which I thought was a good
679 https://maniagnosis.crsr.net/2017/06/AFL-brute-force-search.html
680 https://maniagnosis.crsr.net/2017/06/AFL-bug-in-quicksearch.html
681 https://maniagnosis.crsr.net/2017/07/AFL-correctness-of-quicksearch.html
683 * Frama-C on Stack Overflow:
684 https://stackoverflow.com/questions/tagged/frama-c
686 * Allan Blanchard's tutorial:
687 https://allan-blanchard.fr/publis/frama-c-wp-tutorial-en.pdf
689 * David Mentre's introduction:
690 https://www.cs.umd.edu/class/spring2016/cmsc838G/frama-c/introduction-to-frama-c_v2.pdf
692 * Upstream documentation:
693 Manual: https://frama-c.com/download/frama-c-user-manual.pdf
694 WP manual: https://frama-c.com/download/frama-c-wp-manual.pdf
695 ACSL: https://frama-c.com/acsl.html
697 * ACSL specifications for various string functions:
698 https://github.com/evdenis/verker