Experience Report: Teaching Code Analysis and Verification Using Frama-C

The course was initially divided into four parts: 6 weeks devoted to the course introduction, basic concepts of ACSL and deductive verification with Frama-C/WP (and RTE), 2 weeks for the foundational aspects: axiomatic semantics (and the reference for this part was [14]), 5 weeks for additional concepts of ACSL and deductive verification with application on case studies and finally 2 weeks for an introduction to static analysis with Frama-C/EVA. The three first parts took longer than planned, and the fourth part was removed. The second and third parts were swapped.

ACSL is basically first-order logic with typed C expressions, typed logical expressions and specific predicates. After presented Frama-C as a whole and basic usage of the tool, the course presented the concept of function contract with pre- and post-conditions. The first contracts contained only non-quantified annotations, and without specific predicates. In ACSL annotations mathematical types are used: a C variable containing an integer is thus considered as a mathematical integer. The plugin RTE adds assertions into the code to verify there is not any runtime error. This includes for example signed integer overflows. The use of RTE was introduced at this point in the course. Then the \old predicate, to be used in post-conditions, was introduced. Finally, the assign operator, which indicates which parts of the memory are potentially modified was explained. Note that up to this point, pointers were not used in the examples and exercises. How contracts are used in function calls was included in this introductory presentation. This was completed by the presentation of ACSL behaviors which allow to define contracts for sub-parts of the input space, the pointer-specific predicate \valid, and for expressing properties on arrays, quantifiers. This introductory part ended with set expressions in ACSL, to express memory validity more concisely. The final example was the specification, using behaviors, of a find function on an array of integers, that returns the index of a searched value, or -1. Contrary to previous examples and exercises, Frama-C/WP is unable to check the correctness of the implementation with respect to this contract: loop annotations are necessary. The first part of the class ended with all the concepts related to loop annotations: invariants, variants, loop assigns. Loop annotations were related to mathematical induction, and a significant part was devoted to methods to find invariants.

The second part introduced additional ACSL concepts in order to make the project doable: labels, user-defined predicates, the statement of lemmas, logic functions, and finally ghost code.

The goal of the third part was to present axiomatic semantics in a formal way and weakest precondition calculus in an informal way (as a method to prove axiomatic semantics judgments). It however started with the informal presentation of a small imperative language called nano-C (similar to the usual IMP or While languages but with a C syntax) and its structural operational semantics, with a small modification with respect to IMP/While: sequence is not a command in nano-C, but there are lists of commands (the main program, branchs of conditionals, loop body). This makes the rules of the operational semantics all axioms.

Unlike the version of the course described above, the time dedicated in INSA did not allow an application of a classic detailed presentation of the different ACSL concepts, deductive verification and static analysis. For this specific reason and knowing the background of the students, we took a tutorial-style approach. The idea was to present the different concepts of ACSL and steps of code specification by relying on a concrete small example presented and tested live by the instructor, then a different example for the students to do in class and corrected during the same session. This was a way for the students to practice using the Frama-C tools from the very first sessions, get more familiar with the ACSL specification language as well as keep them invested and attentive throughout the session. We focused on utilizing and presenting, in this order, the RTE, WP and EVA plug-ins as well.

As demonstration of the effectiveness and usability of code specification and verification, we proposed a project that aims to specify and verify the memb module of the Contiki OS. The subject of this project was inspired from the work presented in [13].

Contiki is an operating system for networked, memory-constrained systems with a focus on low-power wireless Internet of Things devices. Uses for Contiki include systems for street lighting, sound monitoring for smart cities, radiation monitoring, and alarms. It is open-source software. Contiki was developed in 2002, the main focus was on enabling communication in the most constrained devices, with no particular attention given to security. As it matured and as commercial applications arose, communication security was added at different layers, via standard protocols such as IPsec or DTLS. The security of the software itself, however, did not receive much attention.

The memb module is Contiki’s main memory management module. To avoid fragmentation in long-lasting systems, Contiki does not use dynamic allocation. Memory is pre-allocated in blocks on a per-feature basis, and the memb module helps the management of such blocks. It offers a simple API, enabling to initialize a memb store, to allocate a block, to free a block, to check if a pointer refers to a block inside the store and to count the number of allocated blocks. The memb.c file consists in about 100 lines of C code but is one of the most critical elements of Contiki, as the kernel and many modules rely on it. The Contiki code base involves a total of 56 instances of memb. Not all are included in a given Contiki firmware, but a subset is included depending on the application and configuration. memb is used for instance for HTTP, CoAP, IPv6 routes, the MAC protocol TSCH, packet queues, etc.

The goal of the project was to formally specify – in ACSL – and verify – using Frama-C/WP – the memb module. The API studied in this project is extremely close to the actual Contiki-NG API, but the provided implementation differs for some functions, to make the verification easier for students. Elements to guide them through the different phases were detailed in the document they received at the beginning of each phase. The files that were provided to students were: logic_defs.h containing user-defined predicates and logic functions; lemmas.h to help the provers to verify the functions with respect to their contracts; memb.h headers of the memb API; and memb.c the full implementation.

The project was divided into three phases in order to better structure the work and have tangible intermediate deliverables. This also eased the amount of work for students and helped them get organized. When faced with a global project description without some guidance, they tend to either be overwhelmed, not knowing where to start, or to push it off to the last minute.

At NAU, at the very beginning of the class, a reminder of propositional calculus truth tables was necessary for some students. On one hand, some students were not acquainted with mathematical notations for logical connectors: ASCL code is written using C syntax for common operations, for example && for conjunction, or specific ACSL syntax, for example ==> for implication, but by default Frama-C pretty prints these symbols as $\wedge$ and $\Rightarrow$ which was confusing to some students. In the other hand, when presenting the ACSL \valid predicate, some students were not comfortable with C-specific features such a pointers, because they essentially programmed using language with automated memory management. In the class CS 396 Principles of Programming Languages, parameter-passing modes are presented. But a significant subset of the students had not taken this class yet, so it was actually necessary also to take some time for C reminders about pointers but also parameter passing.

For an array of size n, two usual ACSL patterns are \forall integer k; 0<= k < n ==> P[k] and \exists integer k; 0<= k < n && P[k] to express that all cells of the array satisfy a property P and there exists a cell that satisfies a property P. Understanding that using && instead of ==> in the universal quantification case and vice-versa in the existential case does not work was a challenge for a significant number of students. Most of the students who failed the class were lost at this point.

Loop invariants are of course challenging. We encouraged the students to write loop annotations incrementally. First the loop assigns annotation and simple invariants about the loop counter when there is one. Most students were able to do so. Writing annotations needed to prove post-conditions was of course more difficult. Related to the challenged described in the previous paragraph, in the find example (and similar cases) writing a loop invariant that is the negation of an existential in the post-condition was a problem. Making the students explain informally why the loop runs rather than stops helped.

The final grades are given in the following table. 76% of the enrolled students passed the course.

All the passing students were able to read and write a function contract including behaviors, and user-defined predicates. They were also able to write loop annotations, but students with a C grade had difficulties in obtaining a strong enough invariant to allow the proof of post-conditions and some form of logical functions may be challenging. Students with a B grade had problems with writing additional annotations to guide the SMT solvers, when students with a C grade were not able to write such annotations. While all passing students were able to write correct contracts, and were able to check whether pre-conditions contain a logical contradiction, they had sometimes difficulties to write strong enough contracts of called functions to allow the verification of calling functions.

At INSA, the students were assessed based on their final work in the project. The first phase was a test phase to make sure that the majority of the students understood the task at hand and have a good comprehension of the different aspects presented during the class. The second and third phases were the ones taken into consideration in their final grade. The following table summarizes the students grades.

While most of the students were able to write function contacts as well as loop annotations during class for smaller examples, when it came to the project they had difficulties executing. The students with grades less than 12 had difficulties in writing loop annotations specially with in finding an invariant. Students with grades between 13 and 15 had a good understanding of the level of specification needed but failed to find exactly the key annotations to guide the solvers. Finally, some students have shown quite the potential, they were able in a short amount of time to well execute the knowledge acquired in the class.

At NAU, there is a procedure for class evaluation by students: 7 questions with 4 possible responses ranging from strongly disagree (1) to strongly agree (4), and 3 open questions: What suggestions do you have to improve this course? The assignment that most contributed to my learning is. What did you like best about this course? The average score to the 7 questions was 3.5 which denotes a good level of satisfaction. There was not any heavy trend in the answers to open questions, but for the assignment that helped the most: the homework assignments. This is not surprising as these assignments are focused on a few concepts. In-class group exercises were also appreciated.

Suggestions for improvements were often contradictory, for example one student would have liked even more examples while another one would have prefered a focus on concepts. Some comments focused on the last assignment but made it a general comment on the course: in the last phase of the project, the students had to experiment with writing assertions in a function body to guide the SMT solvers. Thwas is not an aspect we exercised a lot in class. For all other concepts and ACSL features, several examples and exercises were presented. One comment was representative of the challenges faces by some students: “have an assignment that explicitly outlines/teaches mathematical logic such as disjunction, conjunction, proof by induction, and the like.”

There were many aspects the students liked best about this course. The only answer with several (similar) occurrences was: “thinking about the code in a different way”.