Last week, a few of us at AdaCore attended a one-day workshop organized at Thales Research and Technologies, around the topic of "Verified, trustworthy code - formal verification of software". Attendees from many different branches of Thales (avionics, railway, security, networks) were given an overview of the state-of-the-practice in formal verification of software, focused on two technologies: the SPARK technology that we have been developing at AdaCore, in conjunction with our partner Altran, for programs in Ada; and the Frama-C technology developed at CEA research labs for programs in C.

The two technologies are quite close in terms of methodology and scientific background. My colleague Johannes Kanig recently published a document comparing SPARK with MISRA C and Frama-C, which gives a very good overview of both the similarities and the differences. The Frama-C open source technology is also at the core of the analysis technology developed by TrustInSoft.

The most interesting part of the day was the feedback given by three operational teams who have experimented for a few months with either SPARK (two teams) or Frama-C (one team). The lessons learned by first-time adopters of such technologies are quite valuable:

1. The fact that the specification language is the same as the programming language (SPARK) or very close to it (Frama-C) makes it easy for developers to write specifications in a few days.
2. The first application of such technologies in a team should be targeting a not-too-hard objective (for example absence of run-time errors rather than full functional correctness) on a small part of a codebase (for example a few units/files comprosing a few thousand lines of code rather than a complete codebase with hundreds of thousands of lines of code).
3. Expertise is key to getting started. In particular, there should be an easy way to interact with the tool development/support team. This is all the more important for the first uses, before a process and internal expertise are in place.
4. While specifying properties is easy, proving them automatically may be hard. It is important here to be able to get feedback from the tool (like counterexamples) when the proof fails, and to have a process in place to investigate proof failures.
5. Last but not least, a detailed process needs to be described, so that future applications of formal verification (in the same team, or other teams in the same organization) can reliably get the expected results within the expected budget (effort, schedule).

The last point is particularly important to justify the use of new technology in a project. As part of the two experiments with SPARK at Thales, we defined guidelines for the adoption of SPARK in Ada projects, which follow a scale of four levels:

1. Stone level - valid SPARK - The goal of reaching this level is to identify as much code as possible as belonging to the SPARK subset. The stricter SPARK rules are enforced on a possibly large part of the program, which leads to better quality and maintainability.

2. Bronze level - initialization and correct data flow - The goal of reaching this level is to make sure no uninitialized data can ever be read and, optionally, to prevent unintended access to global variables. The SPARK code is guaranteed to be free from a number of defects: no reads of uninitialized variables, no possible interference between parameters and global variables, no unintended access to global variables.

3. Silver level - absence of run-time errors (AoRTE) - The goal of this level is to ensure that the program does not raise an exception at run time. This ensures in particular that the control flow of the program cannot be circumvented by exploiting a buffer overflow, possibly as a consequence of an integer overflow. This also ensures that the program cannot crash or behave erratically when compiled without support for run-time exceptions (compiler switch -gnatp), after an operation that would have triggered a run-time exception.

4. Gold level - proof of key integrity properties - The goal of the gold level is to ensure key integrity properties such as maintaining critical data invariants throughout execution, and ensuring that transitions between states follow a specified safety automaton. Together with the silver level, these goals ensure program integrity, that is, the program keeps running within safe boundaries: the control flow of the program is correctly programmed and cannot be circumvented through run-time errors, and data cannot be corrupted.

During the two experiments, we managed to reach bronze, silver and gold levels on various parts of the projects, which allowed both detecting some errors and proving properties about program behavior. A really nice outcome for a few weeks of work.