Trust in a system can be compromised in many places. Extensive research has been conducted on the development of trustworthy requirements and policies, but those requirements and policies are effective only if they are carried out correctly. Ensuring the absence of implementation flaws by testing is inadequate; testing cannot be exhaustive and thus can miss critical vulnerabilities. Formal verification?proof that the system correctly implements its specification and enforces its policies?is an attractive alternative.
Standard approaches to formal verification are powerful, but experience has shown them to challenging to use. Specification languages fail to describe complete systems, tools with limited capabilities cannot be integrated, verification techniques are difficult and time consuming to apply, and verification requires high levels of expertise. Current approaches also impose limitations on developers that make it difficult to fit formal verification into the development cycle.
Our approach, Echo, is a new approach to formal software verification that makes such verification readily available, applicable, cost effective, and useful to the community that needs it. The basis of our approach, in stark contrast to traditional methods, is to transform the program, extract a high-level specification from a low-level one, and prove that it implies the original specification. The required analysis is split between a powerful general-purpose theorem-proving system and a low-level verification system.
Echo will improve security and other facets of dependability in important computer applications thereby reducing losses resulting from security attacks and other failures.
