Lecturer: Pascal Cuoq.

Frama-C is a framework for combining analysis techniques towards the analysis or verification of C code.

Why C? C is widely use for embedded programming. In a tiny number of cases, the embedded software is critical: lives depend on it functioning as expected. These applications do, and will increasingly, take advantage of formal methods.

Why combining techniques? Because each of them still has limitations on its own (in some cases, the limitation is intrinsic to the approach and will not be removed with any amount of research). In Frama-C, each technique, implemented as a plug-in, can complement the others, take advantage of the results they have computed, and provide its own results to other plug-ins.

In this course, we will explore the different plug-ins that have already been implemented within the framework.

Frama-C is available for download.

• Frama-C Value Analysis Tutorial.
• Frama-C Jessie Plugin Tutorial.
• IMPORTANT NOTE: make sure you download the files from the English version of the wiki. For some reason they are not linked correctly from the Chinese version. Click “English” at the top of the webpage where you are now.
• Exercises:
  • Day 1
    • first.c
    • div.c
    • abs.c
    • Skein: ZIP file .tar.gz file
    • Homework: continue the analysis of the Skein library to remove the last alarm that was left at the end of the class (assuming it is a false alarm). Download the main() function we had arrived at in class.
    • The Verisec suite is a benchmark for static analyzers: local mirror
    • Homework: From the Verisec benchmark, study the files that compose the case CVE-2006-6876 (from OpenSER), and a few other cases if you wish. Your goal is to find the bug(s) in the files that have them and show there aren't any in the files where the bugs are corrected.
    • If you have had success in either the first homework (removing the last alarm in Skein256) or the second homework (Verisec), send your results, outlining very precisely what you did so that they can be reproduced, before 2010/07/06 at 12:00 to Pascal.Cuoq@gmail.com.
  • Day 2
    • spare.c with commandlines “frama-c -sparecode-analysis spare.c” and “frama-c -pdg -dot-pdg spare spare.c” to generate the PDG in file spare.main.dot (visualize it with any dot visualization tool).
    • Bug report for the bug found in class (now fixed in the development version).
    • Homework: Finish the exercise started in class. If you were not in class or did not have a computer or were sleeping, adapt the instructions provided for the case loops_bad.c to the case istrstr_ok.c and determine that the alarm inside r_strcpy is a true alarm. In order to show that it is a true alarm, you must provide an input vector, which is in this case a value for the buffer answer that causes the problem to appear. Send your results, outlining very precisely what you did so that they can be reproduced, before 2010/07/07 at 12:00 to Pascal.Cuoq@gmail.com.
  • Day 3
    • compare.c solution_compare.c
    • array_ex.c solution_array.c
    • saturation_ex.c solution_saturation.c
    • Homework: Your choice between:
      • If you do not already have Jessie working properly on your computer, your homework is to get Jessie working. Google the error message that you get. Ask a friend. Do whatever it takes.
      • OR: read the value analysis manual. Try out the examples. Most (or all) of the examples should be in this archive if you do not want to type them (or you can probably copy and paste them from the electronic version). Report the bugs that you found (options that do not work, results that are significantly different) to Pascal.Cuoq@gmail.com before 2010/07/08 at 12:00. Example: several sections refer to option ”-lib-entry f”. This option has changed, and correct usage is now ”-lib-entry -main f” to do the same thing. Also please read the ACSL mini tutorial up to chapter 6 (no reporting necessary)
      • OR: read the entire ACSL mini tutorial, trying out the examples in Jessie, and report bugs to Pascal.Cuoq@gmail.com before 2010/07/08 at 12:00.
  • Day 4
    • Example max_seq() from ACSL mini-tutorial chap6_orig.c chap6_simple.c
    • Bloom filters Wikipedia page
    • Constant execution time for cryptographic functions: blog post with ideas using Valgrind, NaCl verified cryptography library
    • String functions

In order to take full advantage of this course, it is strongly recommended

• to have already installed Frama-C, Why, alt-ergo and as many other automatic provers as possible in the following list: Simplify, Z3, CVC3. The versions to use are Frama-C 20100401 (Boron), Why 2.26, and alt-ergo 0.91.

• to be familiar with the C programming language and its pitfalls.

• Abstract-interpretation based Value analysis

• Inputs, outputs, dependencies, slicing

• ACSL is the specification language being developed at the same time as Frama-C.

• Using plug-in Jessie

• ACSL by example: http://www.first.fraunhofer.de/owx_download/acsl-by-example-5_1_0.pdf
• Links to documentation and introductory tutorials are at http://frama-c.com/support.html in the “Documentation” section.

One dependency chain is ACSL mini-tutorial → ACSL by example → Jessie documentation → ACSL reference manual.

Another dependency chain is Value analysis mini-tutorial → Value analysis manual → Slicing and navigation plug-ins documentation.