From: Richard W.M. Jones Date: Tue, 13 Oct 2020 15:16:25 +0000 (+0100) Subject: Add notes for talk on Frama-C. X-Git-Url: http://git.annexia.org/?p=libguestfs-talks.git;a=commitdiff_plain;h=54595cfdd8aa441edb5e4738e4643f3c5fbbe471 Add notes for talk on Frama-C. --- diff --git a/2020-frama-c/notes.txt b/2020-frama-c/notes.txt new file mode 100644 index 0000000..edd3143 --- /dev/null +++ b/2020-frama-c/notes.txt @@ -0,0 +1,584 @@ +16th Nov 2020 +Formally proving tiny bits of qemu using Frama-C + +[in medias res] + +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 +my radar to learn for a long time, and I'm a co-maintainer of the +package in Fedora. I tried to follow one tutorial but never really +got past installation and UI issues. But the developer pointed me to +a very good, short set of blog postings about using the command line +tool. + +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 +smallest pieces of code in the "util/" subdirectory: + + $ wc -l util/*.c | sort -nr | tail -20 + +Actually there are two files: + + $ 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: + + /* + * Operations on 64 bit address ranges. + * Notes: + * - Ranges must not wrap around 0, but can include UINT64_MAX. + */ + struct Range { + /* + * Do not access members directly, use the functions! + * A non-empty range has @lob <= @upb. + * An empty range has @lob == @upb + 1. + */ + uint64_t lob; /* inclusive lower bound */ + uint64_t upb; /* inclusive upper bound */ + }; + typedef struct Range Range; + + +-----------+-----------+------------- - - - - - + | | | + +-----------+-----------+------------- - - - - - + ^ ^ + lob ----- upb + +Using the tutorial as my guide I wrote some simple predicates, a +"predicate" being a statement which can be true or false: + + * A non-empty range has @lob <= @upb. + * An empty range has @lob == @upb + 1. + + /*@ + predicate valid_range(struct Range range) = + range.lob <= range.upb + 1; + + predicate empty_range(struct Range range) = + range.lob == range.upb + 1; + */ + +Notice a few things here: + + - These are statements written in a formal language. + + - I'm using structs directly from the C code. + + - The comments in the upstream code translate into predicates. + +The first upstream function is: + + /* Is range empty? */ + static inline bool range_is_empty(const Range *range) + { + return range->lob > range->upb; + } + +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; + } + +And we can compile and prove that: + + $ frama-c -wp -wp-rte snippets/range_is_empty.c + +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 = + +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; + */ + + /* 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; + } + + $ 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 +specification and C code were translated into first-order logic +statements and passed to the Alt-Ergo SMT prover to see if it could +find a Proof Obligation (PO). + +We need to be very clear about what happened: + + - The preconditions must be fulfilled in order for the proof to be + correct. If you are checking a whole program then that would check + that all callers of this function are fulfilling the preconditions, + but if you check only single functions then you are not doing that. + + - The proof only shows that the post-condition holds. + + - This only shows that the source code is correct. The compiler + could still compile the program incorrectly. If you really want to + get into this you have to use a verified C compiler like CompCert, + and there are even verified CPU implementations. + + - Given those assumptions, the code is bug free - you don't need to + write any tests. + +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: + + /* Does range contain val? */ + static inline bool range_contains(const Range *range, uint64_t val) + { + return val >= range->lob && val <= range->upb; + } + +This is similarly easy to prove after adding another predicate at the +top of the file: + + /*@ + predicate value_in_range(struct Range range, uint64_t value) = + range.lob <= value <= range.upb; + */ + + /* Does range contain val? */ + /*@ + requires \valid_read(range); + requires valid_range(*range); + assigns \nothing; + ensures \result <==> value_in_range(*range, val); + */ + static inline bool range_contains(const Range *range, uint64_t val) + { + return val >= range->lob && val <= range->upb; + } + +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: + + /* Initialize range to the empty range */ + /*@ + requires \valid(range); + requires valid_range(*range); + assigns *range; + ensures empty_range(*range); + */ + static inline void range_make_empty(Range *range) + { + *range = range_empty; + assert(range_is_empty(range)); + } + +I'm going to skip forward a few functions to get to an interesting one. +This seems trivial: + + /* Get the size of range. */ + static inline uint64_t range_size(const Range *range) + { + return range->upb - range->lob + 1; + } + +My first attempt at a proof was: + + /*@ + logic integer size_of_bounds(integer lob, integer upb) = + upb - lob + 1; + + logic integer size_of_range(struct Range range) = + size_of_bounds(range.lob, range.upb); + */ + + /* Get the size of range. */ + /*@ + requires \valid(range); + requires valid_range(*range); + assigns \nothing; + ensures \result == size_of_range(*range); + */ + static inline uint64_t range_size(const Range *range) + { + return range->upb - range->lob + 1; + } + +A few things to notice about this: + + - I'm using ACSL "logic" statements, which are similar to functions. + + - ACSL has an "integer" type which is an unbounded integer. + +Let's try to prove this one: + + $ frama-c ... snippets/range_size.c + XXX 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 +looks equally trivial and yet it cannot be proven. Why? + +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 +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. + +So this is the counterexample which I worked out myself: + + /*@ + logic integer size_of_bounds(integer lob, integer upb) = + upb - lob + 1; + + logic integer size_of_range(struct Range range) = + size_of_bounds(range.lob, range.upb); + */ + + /* Get the size of range. */ + /*@ + requires \valid(range); + requires valid_range(*range); + assigns \nothing; + ensures \result == size_of_range(*range); + */ + static inline uint64_t range_size(const Range *range) + { + return range->upb - range->lob + 1; + } + + +-------------------------------------------------------+ + |XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX| + +-------------------------------------------------------+ + range->lob == 0 range->upb == UINT64_MAX + +In this case size_of_range() returns an integer. Recall that integers +are an unbounded type. So it returns UINT64_MAX + 1 (a 65 bit +number). Our C function on the other hand returns 0. + +This is a bug in the function. There are really two ways to +look at this: + +(1) The function shouldn't be called on empty ranges (size 0), and so +if the function returns 0 it means "the total range". Or: + +(2) The function should have a different signature so it can return a +separate indication for "empty range" vs "total range". + +I went with the first, so the final working specification is this. If +we were proving the entire program then we could statically verify +that callers do not try to call range_size() on the empty range. + + /*@ + requires \valid(range); + requires valid_range(*range); + requires !empty_range(*range); + assigns \nothing; + // case UINT64_MAX+1 -> 0 + ensures \result == (uint64_t)size_of_range(*range); + */ + static inline uint64_t range_size(const Range *range) + { + return range->upb - range->lob + 1; + } + +On to the next function. Again this seems very simple, but in fact it +contains a serious problem: + + /* + * Initialize range to span the interval [lob,lob + size - 1]. + * size may be 0. Range must not overflow. + */ + static inline void range_init_nofail(Range *range, uint64_t lob, + uint64_t size) + { + range->lob = lob; + range->upb = lob + size - 1; + } + +What does lob == 0, size == 0 mean? It will create a total range. + + +-------------------------------------------------------+ + |XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX| + +-------------------------------------------------------+ + range->lob == 0 range->upb == UINT64_MAX + +What does lob == 1, size == 0 mean? It will create an empty range. + +Because I didn't want to change the code, that makes the proof very +long, and it demonstrates another feature of ACSL specifications +("behaviors"): + + /*@ + requires \valid(range); + requires lob + (integer)size <= UINT64_MAX; + assigns *range; + behavior empty: + assumes lob > 0 && size == 0; + ensures empty_range(*range); + behavior non_empty: + assumes size > 0; + ensures range->lob == lob; + ensures size_of_bounds(lob, range->upb) == size; + behavior total: + assumes lob == 0 && size == 0; + ensures total_range(*range); + complete behaviors; + disjoint behaviors; + */ + +I also had to modify my earlier empty_range predicate: + + /*@ // before: + predicate empty_range(struct Range range) = + range.lob == range.upb + 1; + */ + + /*@ // after: + predicate empty_range(struct Range range) = + range.lob > 0 && range.lob == range.upb + 1; + */ + +What can we say about this? If you were developing the Range type and +the proof at the same time, you probably wouldn't define the Range +type in this way, and you probably wouldn't choose an initialization +function which had this complex set of behaviours. + +I did prove most of the rest of the Range functions, but I wanted to +point out a few things about the final proof: + + - The original file includes glib headers, but those cannot be parsed + by Frama-C's parser. The problem appears to be some unsupported + __attribute__s. Some attributes seem to work, and others are not + supported, and this of course limits what you can prove if it + depends on any external library that might use these. + + - For the same reason I had to exclude a glib function for operating + on lists of ranges from the proof. + + - You can run frama-c on the original source file, with a few #ifdef + modifications, so it would be possible to maintain the annotations + upstream, and run the proof checker as a CI test. + + - It probably doesn't make sense for qemu right now though, unless we + could prove more substantial pieces of code. + += POWER OF 2 = + +This is a function from nbdkit: + + /* Returns true if v is a power of 2. + * + * Uses the algorithm described at + * http://graphics.stanford.edu/~seander/bithacks.html#DetermineIfPowerOf2 + */ + static inline bool + is_power_of_2 (unsigned long v) + { + return v && ((v & (v - 1)) == 0); + } + +and my initial specification started by defining: + + /*@ + predicate positive_power_of_2 (integer i) = + i > 0 && + (i == 1 || ((i & 1) == 0 && positive_power_of_2 (i >> 1))); + + lemma positive_power_of_2 (1); + lemma positive_power_of_2 (2); + lemma positive_power_of_2 (4); + lemma !positive_power_of_2 (7); + */ + +I was using the lemmas (which are like assertions, except statically +verified), to test my predicate, but sadly Frama-C was not able to +prove them even though they appear to be trivial. + +This led to some discussion on stackoverflow: + + https://stackoverflow.com/questions/64268418/how-do-i-write-an-is-power-of-2-predicate-in-acsl + +Ultimately it was possible to fix this, but I discovered a few things +about Alt-Ergo (the default prover): + + - It can't handle bitwise operations very well. + + - You can guide Alt-Ergo, but it requires using the Frama-C GUI which + is very non-intuitive. You do end up with a script but I couldn't + work out how to integrate this with the command line. + + - Z3 should be able to solve this, but I was not able to get + Z3 working with Frama-C on Fedora. + +Essentially bitwise tricks like this are a hard case for automated +theorem proving. I gave up. + += TIMEVAL DIFFERENCE = + +This is another nbdkit function: + + /* Return the number of µs (microseconds) in y - x. */ + static inline int64_t + tvdiff_usec (const struct timeval *x, const struct timeval *y) + { + int64_t usec; + + usec = (y->tv_sec - x->tv_sec) * 1000000; + usec += y->tv_usec - x->tv_usec; + return usec; + } + +My first attempt at a proof was: + + /*@ + predicate valid_timeval (struct timeval tv) = + tv.tv_sec >= 0 && tv.tv_usec >= 0 && tv.tv_usec < 1000000; + logic integer tv_to_microseconds (struct timeval tv) = + tv.tv_sec * 1000000 + tv.tv_usec; + */ + + /* Return the number of µs (microseconds) in y - x. */ + /*@ + requires \valid_read (x) && \valid_read (y); + requires valid_timeval (*x) && valid_timeval (*y); + ensures \result == tv_to_microseconds (*y) - tv_to_microseconds (*x); + */ + static inline int64_t + tvdiff_usec (const struct timeval *x, const struct timeval *y) + { + int64_t usec; + + usec = (y->tv_sec - x->tv_sec) * 1000000; + usec += y->tv_usec - x->tv_usec; + return usec; + } + +This is not provable, and again the problem is integer overflow. The +tv_sec field is a 64 bit integer so it's quite easy to construct two +inputs which overflow the output. + +Fixing this involves a considerably more complex specification: + + /*@ + requires \valid_read (x) && \valid_read (y); + requires valid_timeval (*x) && valid_timeval (*y); + requires \valid (r); + assigns *r; + behavior success: + ensures \result == 0; + ensures \let diff = tv_to_microseconds (*y) - tv_to_microseconds (*x); + INT64_MIN <= diff <= INT64_MAX && + *r == diff; + behavior failure: + ensures \result == -1; + ensures *r == 0; + ensures \let diff = tv_to_microseconds (*y) - tv_to_microseconds (*x); + !(INT64_MIN <= diff <= INT64_MAX); + complete behaviors; + disjoint behaviors; + */ + static inline int + tvdiff_usec (const struct timeval *x, const struct timeval *y, + 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 +simple. + +A few things I learned from this: + + - This is a function we have had and used for years, and I don't + think anyone ever thought it had a problem. + + - Co-developing the specification alongside the code could help + here. + + - You can end up with functions that are much harder to use. If we + were proof-checking the whole program we could check all callers. + + - GCC has __builtin_add_overflow and similar which can be used to do + mathematical operations and detect overflow, but Frama-C does not + understand them. We could contribute these to the Frama-C standard + library. + + + + + + + + += IN CONCLUSION = + +* Frama-C is a real open source tool used by companies to verify + safety-critical software. If you've flown in an Airbus or used + electricity from a French nuclear power plant then you've used this + software already. + +* 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. + +* Forces you to think very hard about assumptions and corner cases, + but that's the nature of the problem. + +* Very well documented, questions answered quickly on stackoverflow. + +But it has its limits: + +* Typed Memory Model turns out to be restrictive. + +* No support for malloc. + +* Not good at bitwise ops (can Z3 help?). + +* Cannot parse some non-standard __attribute__s (glib).