You think your software works? Prove it!
Formal methods have been quietly moving from the research lab into mainstream software development, especially in high-assurance systems. With modern programming languages and proof technology, developers can make use of formal methods at various levels, ranging from enforcement of safe language features to proof of compliance with formally specified requirements. Understanding the benefits and costs associated with each level can help developers decide whether and how to adopt and employ formal methods. And it’s not an “all or nothing” choice: formal methods can be mixed with traditional verification techniques (i.e., testing), introduced incrementally into an existing project, and combined with code written in languages such as C or C++.
Program verification has traditionally relied on testing, but as the late computer scientist Edsger Dijkstra once remarked, “program testing can be used to show the presence of bugs but never to show their absence”. This drawback has been known since the dawn of programming, and one of the earliest research areas in the software field was formal verification: statically analyzing the source code for a program and proving specified dynamic properties with mathematics-based rigor. For various reasons, however, this methodology did not make it into widespread practice. The language subsets were overly restrictive, machines were slow, proof techniques were impractical for large programs, goals were overly ambitious (proof of functional correctness), the false alarm rate was too high, and formal verification didn’t integrate well with traditional development methods.
Well, that was then, and this is now. Recent years have seen marked progress in proof technology, exponentially faster hardware, multicore for parallelism, better and more expressive programming languages, and approaches that can combine proof with testing. And, not insignificantly, the increased attention being paid to software reliability, safety and security has led to the realization that confidence backed by mathematical reasoning is required for critical program properties.
The SPARK programming language and analysis / proof toolset illustrates this trend, and experience with its usage has led to the formulation of practical implementation guidance: how to introduce formal methods into an enterprise based on the relevant assurance goals, and how to combine proof with testing.
What Is SPARK?
The SPARK language is a subset of Ada 2012 designed for modular static verification (thus omitting features that are difficult to verify or whose semantics is not well defined), augmented with aspects that facilitate analysis. It includes Ada’s features for program structure (packages, subprograms, generics), most data types, object-oriented programming, and, most importantly, the contract-based features added in Ada 2012 (e.g., subprogram pre- and post-conditions). It also includes a deterministic set of Ada tasking (concurrency) features known as the Ravenscar profile. The most notable omissions are access types (pointers), side effects in functions, aliasing of names (e.g., referring to the same object through a global variable and a subprogram parameter), the goto statement, and exception handling.
Figure 1 shows an example of a fragment of a SPARK program. (Source: AdaCore)
The Increment procedure reads the global variable N and adds its value to the formal parameter X. The names Global, Depends, Pre, and Post are known as “aspects” and represent various properties (contracts) of the procedure Increment. The Global aspect shows that the procedure uses N as an input, the Depends aspect shows that the final value of X depends on its starting value as well as the value of N, the Pre aspect reflects the subprogram’s precondition (needed to ensure absence of arithmetic overflow), and the Post aspect reflects the functionality of the procedure (the final value of X is the sum of the starting value of X and the value of N). The SPARK tools can statically verify the Global, Depends and Post contracts. In the case of Post, the proof tool will show that, if the precondition is met and the procedure terminates, then the postcondition will be met. The precondition is checked at each point where the procedure is called.
Since SPARK is a subset of Ada, the dynamic contracts such as Pre and Post can be treated with Ada semantics and checked at run time. That allows a smooth transitioning from test-based verification to static (formal) verification, and also the ability to mix and match within the same program. Some parts of the program can be indicated as being in SPARK mode (and subject to analysis and proof) while others are not in SPARK mode. As a specific example, a subprogram specification may be in SPARK mode while its body is not. This allows hybrid verification where, for example, calls of the subprogram are verified formally to make sure that the precondition is met, while the implementation of the subprogram body is verified via testing, for example because it uses features outside the SPARK subset. Indeed, combining SPARK not just with full Ada but with code written in languages such as C or C++ can be handled in an analogous fashion. Formally verified SPARK code can call, or be called from, code written in these other languages.
Levels of Assurance
One of the impediments to the use of formal methods in the past was the perception that it was “all or nothing”: it was difficult to introduce into an existing project, and seemed to require a whole new mindset and approach for its application. To address this issue, AdaCore worked with one of its customers to see how to introduce formal methods, and SPARK in particular, in the context of ongoing Ada software development. The result of this collaboration was a methodology expressed as guidance that describes five levels of software assurance; for each level the guidance presents the approach, its benefits and costs, and the impact on the software development and verification processes.
At this basic level, the approach is to implement as much code as possible in the SPARK subset but without necessarily trying to perform the associated data and flow analysis or proof. The main benefit is that the code will be more portable and easier to maintain. The cost is the effort involved in inspecting non-compliant code and then either adapting it so that it is legal SPARK, or else marking the code as in non-SPARK mode so that it is not subject to formal analysis. An example is the usage of pointers. If pointers are not heavily used then revising the code to use array indices or the formal containers library may be practical. Otherwise pointers could be defined through encapsulated types in Ada, with their representation as pointers supplied in non-SPARK sections. Once the initial code base has been converted, the incremental effort in development and verification is similar to full Ada.