Echo: A New Approach to Formal Verification Based on Ada
The Technology & Experience in Security and Medical Devices

John Knight

Abstract

Echo is a novel yet practical approach to the formal verification of large software systems. The Echo approach splits verification into two major parts. In the first part, the SPARK tools are used to verify an implementation written in SPARK Ada against a low-level specification written using the SPARK sourcecode annotations. In the second part, a high-level specification is extracted automatically from the annotated implementation, and a proof constructed using the PVS theorem proving system that the extracted specification implies the original specification.

Part of what makes Echo practical is a technique called verification refactoring. The program to be verified is mechanically refactored specifically to facilitate verification. In both parts of the proof process, semantics-preserving refactorings are applied to the implementation to reduce the complexity of the software and thereby to reduce the difficulty of verification proof.

Much of the Echo approach is automated. The verification burden is reduced by distributing the burden over separate tools and techniques.

In this presentation, the Echo verification technology will be described. The technology will be illustrated using the verification of two security applications and a novel medical device.