Enter SPARK 2014, an open-source subset of Ada 2012 specifically designed to achieve this goal. It includes a complete contract facility, enabling the programmer to prove that all contracts both the implicit ones (like no integer overflow) and the explicit ones written into the program are guaranteed to be obeyed under all conditions. In fact, with SPARK, we won't even need the runtime checks because we will know in advance, with the security of a mathematical proof, that such checks could not fail in any case.
People have been talking about the idea of proving programs correct for many decades. One perspective is that you write a giant formal specification of your program, and then you prove your program correct in the sense that it is guaranteed to meet this specification. However, there are several weaknesses in this approach. First, producing such a formal specification is a huge amount of work. Second, carrying out the necessary verification on that scale is a very tough proposition. But most importantly, this won't guarantee the absence of errors, since the specification itself may be wrong. In fact, it most likely will be wrong, since a formal specification for a realistic system is essentially an enormous program in its own right.
SPARK 2014 takes a more conservative approach; it tries to prove only the contracts that are included in the program. Basically, programmers can decide which requirements are important enough to capture as contracts. Even if none are explicitly included, a lot can still be achieved by proving that the implicit contracts inherent in the language semantics are satisfied; for example, it can be proved that buffer overruns (out-of-range array indexes) cannot happen. If OpenSSL had been written in SPARK 2014, then the bug simply could not have survived the compilation/proof processes.
SPARK in Practice
All this is easy to say, but is it really practical? The answer is yes, with some impressive large scale examples from earlier versions of SPARK. For instance, the latest set of software tools supporting air traffic control in the U.K., iFACTS, is a very large and complex program; most of it is written in SPARK, and has been proved to be free of all runtime errors.
How was this goal achieved? First of all, designers had to worry about those features that make trouble for a proof-based approach. One issue, noted earlier, is undefined behavior. This can arise in most languages through a reference to an uninitialized variable, as an example. SPARK 2014 avoids all undefined behavior; all variables in SPARK must be initialized before they are referenced. In addition, features that make life entirely too difficult for automated proofs are omitted. In particular, pointers are excluded since they are a huge menace. If a C program contains something like:
int *a; … *a = 3;
then the assignment could clobber any
int variable anywhere. Because a proof depends on carefully tracing possible values, that introduces a significant complication. Things are somewhat better in Ada, since only those variables explicitly marked as aliased are susceptible to modification through such indirect assignments. Nevertheless, the ability to modify variables indirectly makes the proof of program properties more difficult because of the additional complexity of the data flow analysis, so SPARK 2014 bans pointers completely. That requires the programmer to use an alternative style, perhaps less convenient than pointers; but this is a worthwhile tradeoff to obtain a guarantee of no runtime errors in the program. Similarly, the SPARK language eliminates exceptions (we don't really need them if we prove they can't happen anyway). Even after removing these troublesome features, SPARK 2014 is an expressive language, significantly larger than previous versions in the SPARK language series, supporting the development of high-integrity systems of significant size and complexity.
Suppose we write a large program in SPARK 2014, and click the Prove button; and the output shows that most but not all the contracts have been proved. What now?
There are several reasons why we might fail to prove something:
- The error can't occur, but the prover cannot see that this is the case. In this situation, we can add additional assertions to help. In really difficult cases, we might have to provide a manual proof.
- The error can't occur, but that's because there are assumptions that we know about that are unknown to the prover. For example, perhaps an error can occur only if the outside air temperature is greater than 1000 degrees. In this case, we can add an assumption stating that the outside temperature is in some known safe range. An assumption differs from an assertion in that the prover will believe it and not try to prove it. We have to be very careful with such assumptions to make sure they are legitimate.
- The error can occur. This is a real bug in the program, and it is no surprise that the prover fails to prove that the error cannot occur. In this case, the bug, which may either be in the contract itself or in the code, must be fixed.
A major goal of the SPARK 2014 design is to minimize the number of cases in the first category. One advantage programmers today have over those trying to do proofs thirty years ago is that we have much faster machines and greatly superior proof technologies. Our experience so far with SPARK 2014 indicates that its proof technology is practical for the programmers who typically develop critical software and who tend to be domain specialists rather than experts in mathematical logic. There is a bit more effort up front, but it's worth it to avoid more Heartbleeds and to ensure that the software in critical systems (such as automotive control) is safe and secure enough for us to trust our lives to it.
A final point is that it's hardly practical to expect projects to start from scratch using SPARK 2014. Although this may be possible in some limited cases, real-world systems are generally a mixture of legacy code and new code. A very important part of the SPARK 2014 approach is to accommodate programs written in multiple languages (SPARK 2014 mixed with C and full Ada, for example). In these cases, we can combine traditional testing approaches for the non-SPARK parts of the program with proof of contracts applying to the SPARK sections. This involves some subtle language design to get things to mesh reliably. SPARK 2014 has a comprehensive solution for this kind of mixing of approaches, and thus, it is potentially applicable to a far wider class of problems than previous SPARK versions.
The SPARK 2014 technology is available as GPL-licensed software. At this writing, the 2014 version is a near-final technology preview, while earlier versions are fully validated releases.
Dr. Robert Dewar is cofounder and President of AdaCore and Emeritus Professor of Computer Science at New York University. He has been a major contributor to Ada throughout its evolution and is a principal architect of AdaCore's GNAT Ada technology. Dr. Rod Chapman is a Principal Engineer with Altran, specializing in the design and implementation of safety and security-critical systems. He currently leads the development of the SPARK language and its associated analysis tools.