Slides for 3xxx.

[libguestfs-talks.git] / 2020-frama-c / notes.txt

diff --git a/2020-frama-c/notes.txt b/2020-frama-c/notes.txt
index 2fbb76d..d41e161 100644 (file)
--- a/2020-frama-c/notes.txt
+++ b/2020-frama-c/notes.txt
@@ -13,6 +13,7 @@ tool.
 
 I will provide links to tutorials etc at the end.
 
+\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:
@@ -69,7 +70,7 @@ Notice a few things here:
 
  - 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:
 
@@ -81,7 +82,7 @@ The first upstream function is:
 
 and using the predicates we can write a specification:
 
-  $ less snippets/range_is_empty.c
+  $ cat snippets/range_is_empty.c
 
 And we can compile and prove that:
 
@@ -90,21 +91,21 @@ 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.
 
+\f
 = OVERVIEW OF FRAMA-C ECOSYSTEM =
 
+Let's interrupt this and talk about Frama-C.  The name stands
+for "Framework for Static Analysis of the C language".
 
-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
-
+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
 = BACK TO RANGE.C =
 
 Going back to what we proved so far:
@@ -153,6 +154,7 @@ We need to be very clear about what happened:
  - 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:
@@ -183,6 +185,7 @@ top of the file:
       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:
@@ -200,6 +203,7 @@ 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:
 
@@ -314,6 +318,7 @@ that callers do not try to call range_size() on the empty range.
 
   $ 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:
 
@@ -398,6 +403,7 @@ point out a few things about the final proof:
  - 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:
@@ -449,6 +455,7 @@ about Alt-Ergo (the default prover):
 Essentially bitwise tricks like this are a hard case for automated
 theorem proving.  I gave up.
 
+\f
 = TIMEVAL DIFFERENCE =
 
 This is another nbdkit function:
@@ -539,6 +546,7 @@ A few things I learned from this:
    understand them.  We could contribute these to the Frama-C standard
    library.
 
+\f
 = STRING FUNCTIONS =
 
 Uli sent me this function from glibc:
@@ -589,6 +597,7 @@ 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:
 
@@ -596,8 +605,9 @@ 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
+  [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:
@@ -630,6 +640,7 @@ 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
@@ -671,3 +682,28 @@ Alternatives and related programs:
 
 * 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