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
+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.
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;
- }
+ $ less snippets/range_is_empty.c
And we can compile and prove that:
/*@
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
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
return range->upb - range->lob + 1;
}
+ $ frama-c -wp -wp-rte snippets/range_size-good.c
+
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
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.
+= 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.
+
+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
+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!
= IN CONCLUSION =
* 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).
git.annexia.org / libguestfs-talks.git / commitdiff