Formal verification

Formal verification has long been recognized as a gold standard for software quality – but carries a high cost. Writing secure software typically requires both automated reviews and peer reviews, to insure that security bugs have been eliminated in the design and implementation. Design bugs can allow an attacker to work around good software, and vice versa. While many helpful tools exist today, for example automated software testing tools and sophisticated automated model checking tools, pioneering computer scientists such as Edsger Dijkstra and Sir C. A. R. Hoare suggested that a powerful way to eliminate bugs is to create a model and a mathematically rigorous proof showing that the software cannot err. These models and their proofs are called formal methods, and their results are called verification.

Recent successes by NSA-teaming researchers demonstrate that for the simple and powerful Separation Theorem, formal verification is not beyond reach. For example, researchers at Motorola and Rockwell-Collins have created high assurance hardware implementations derived from the Separation Theorem. Similarly, RedPhone Security has developed a formal security policy model based on the Separation Theorem introduced by John Rushby.

More information: