You think your software works? Prove it!
The Bronze level consists of the Stone level plus performing flow analysis to verify intended data usage (global variables, formal parameters, local variables). This analysis will detect variables that might not be initialized, as well as instances of variable aliasing. The benefits include guarantees for a number or program properties (no reads of uninitialized variables, no interference between parameters and global objects, no race conditions on access to shared data) as well as improved readability from the contracts (Global and Depends) that show the programmer’s intent. The analysis will also uncover suspect code that could be an error (for example an unused assignment or a statement that has no effect). The main cost is in the initial pass, which involves inspecting the check messages and either rewriting the code or explaining the false alarms.
The Silver level consists of the Bronze level plus ensuring the absence of run-time errors. This involves running the proof tool, inspecting each failure (i.e., each place where the prover could not guarantee the absence of an exception) and then either correcting the code, explaining why it is a false alarm, or adding appropriate contracts to facilitate proof. Subprogram pre- and post-conditions and loop invariants may be needed. The benefits at the Silver level are substantial and include the assurance that run-time errors will not occur (thus no buffer overflow) and the ability to compile the final executable without exception checks. The cost is the effort required in the initial pass, and the added effort in inspecting and resolving the check failures. Ongoing maintenance is similar to the Bronze level.
The Gold level consists of the Silver level plus proving key integrity properties such as data invariants or safe transitions between program states. The approach is similar to the Silver level, and features such as subprogram pre- and postconditions and type predicates are especially useful. Figure 2 illustrates a type predicate, which is an invariant that in this example ensures that arrays are always sorted.
Figure 2 shows an example of a type predicate in SPARK. (Source: AdaCore)
The predicate is enforced on assignments to objects of type Sorted_Array. The costs and benefits at the Gold level are similar to the Silver level. The verification effort depends on the complexity of the properties to be proved, and developing the contracts and interacting with the tool may require practice. For large programs, tool execution may take several hours.
The Platinum level consists of the Gold level plus proof of full functional correctness (ie, compliance with formally specified requirements). This may be appropriate for small, critical components that demand the highest degree of confidence and whose developers have experience with the proof technology.
AdaCore worked with one of its customers, Thales (France), in introducing SPARK into several pilot projects, to investigate the costs and benefits of formal methods at several assurance levels. Thales is a global company in the Aerospace, Ground Transportation, Defense and Security domains.
Port to a new platform
The context was a radar system comprising around 300 K Lines of Code (KLOC). The target was Stone level. The effort entailed refactoring the code to comply with the SPARK subset, for example to deal with the usage of pointers. A large part of the effort was successfully performed in a few days, and the remainder is scheduled for completion.
Demonstrate compliance with low-level requirements
The context was a small numerical function, and the target was the Gold level to prove a specific property. This project showed the challenges of achieving the Gold level on numeric computation: the contracts ended up being as long and complex as the code that they were designed to prove. The property was not proved automatically, and the “lesson learned” was that for these kinds of programs a lower level of assurance is more realistic and traditional verification methods (testing) is more practical.
Identify and fix weakness
The context was a code generator, and the target was the Gold level to prove a property related to memory bounds. Two senior developers, assisted by a SPARK expert, took a half day to reach the Silver level and two days to reach Gold.
Guarantee safety properties
The context was a command and control component (7 KLOC) and the target was the Gold level to prove a property expressed as an automaton. Two senior developers, assisted by a SPARK expert, took one day to reach Silver and four days to reach Gold.
Based on experience from both the pilot projects noted above and other successful applications of formal methods in real-world applications, it’s safe to say that this technology is ready for prime time. Formal verification through SPARK allows the flexibility to fine-tune its gradual insertion into existing processes while mitigating its associated risks and costs. Developers with no previous experience in SPARK or formal methods can quickly become proficient in the technology.
Here are some recommendations concerning the various levels:
Use the Stone level as an intermediate stage during adoption
Aim for the Bronze level for as large a part of the code as possible, since the flow analysis will detect potential problems with initialization and aliasing and identify other suspicious constructs
Choose the Silver level as the default for critical software (subject to costs and limitations)
Go for the Gold level only for a subset of the code that is subject to key integrity (safety / security) properties
These recommendations are based on experience with the SPARK language and toolset; the same principles could be applied using other formal method technologies (such as Frama-C) although the specific costs and benefits will be different.
References / Resources
Textbook for students and software professionals: McCormick and P. Chapin, Building High Integrity Applications with SPARK; Cambridge University Press; 2015
SPARK blog and resources (User’s Guide)
Dr. Benjamin Brosgol is a member of the senior technical staff of AdaCore. He has been involved with programming language design and implementation thoughout his career, concentrating on languages and technologies for high-assurance software. Dr. Brosgol was a member of the design team for Ada 95, and he has also served in the Expert Groups for several Java Specification Requests. He has presented papers and tutorials on safety and security certification on numerous occasions including ESC (Embedded Systems Conference), ICSE (IEEE/ACM International Conference on Software Engineering), STC (Software Technology Conference), ACM SIGAda, and Ada-Europe. Dr. Brosgol holds a BA in Mathematics from Amherst College, and MS and PhD degrees in Applied Mathematics from Harvard University.