Model checking and static analysis techniques have been successfully applied to some problems, and some of these techniques scale well. However, their analysis targets only certain properties. For critical applications, complete formal verification of functionality is highly desirable.
The Echo approach is intended for routine use alongside existing software development techniques and does not require programmers to be skilled in mathematical logic or formal verification techniques. To ease the burden of creating proofs of correctness, the Echo process splits these into two separate proofs.
A software developer using the Echo process first produces both a formal specification and an annotated SPARK Ada program using familiar, traditional software engineering techniques. Using the SPARK tools, the developer establishes an implementation proof showing that the SPARK Ada source code complies with its annotations. Echo’s unique reverse synthesis process then produces a high-level abstract extracted specification. Finally, the developer establishes an implication proof showing that the extracted specification implies the given formal specification. Taken together, the implementation and implication proofs form a complete proof of correctness.
The keys to the practicality of the Echo process are the use of verification refactoring and the availability of a practical implementation proof process. In verification refactoring, the SPARK program is subjected to user-selected machine transformations. Software must run adequately fast, but this speed often comes at the cost of increased complexity. By transforming the source code into a lessc omplicated form with the same functional semantics, verification refactoring reduces the complexity of the extracted specification. Re-rolling loops, splitting procedures into simpler sub-procedures, reversing function inlining, and adding or removing intermediate computations or storage will not change the program behavior, but can dramatically ease the creation of the required proofs.
The effect of verification refactoring can be dramatic. In one study, Knight and Yin formally verified a SPARK implementation of the Advanced Encryption Standard (AES). By adjusting data structures and reversing table lookups, the efficient implementation to be verified was transformed to one more amenable to formal verification.
While the Echo approach could, in theory, be applied to programs written in any language, SPARK offers a number of advantages, specifically:
- The use of SPARK provides a powerful programming language with associated mechanism for low-level specification.
- SPARK precludes the use of language features that would have made the proofs — both the implementation proof and the implication proof — either extraordinarily difficult or more likely impossible.
- The SPARK tools are robust and mature, and they immediately support the implementation proof that is a fundamental part of the Echo approach.
- Production-quality compilers, such as AdaCore’s GNAT-Pro High-Integrity Edition, are available for many platforms.
The LifeFlow LVAD software project has implemented a control system for the active magnetic bearings that the LVAD uses. A complete verification proof demonstrates that the SPARK implementation refines the high-level PVS specification. The implementation targets a high performance embedded microprocessor. Since no operating system is used, almost all the software that executes has been the subject of formal verification. The only unproven software items are the assembly-language loader, implementations of two low-level C functions called by compiler-generated object code, and the machine configuration parameters.
This article was written by John Knight, PhD, Professor of Computer Science, University of Virginia in Charlottesville, VA; Xiang Yin, Senior Software Design Engineer, MicroStrategy, Inc., Tysons Corner, VA; and Patrick John Graydon, Research Associate, University of York, York, UK.