Abstract:

What does software verifiability have to do with an 18th-century Swiss mathematician? Come to hear the story that starts with Leonhard Euler, progresses to a patent worth hundreds of millions of dollars, and ends with software verifiability for safety and security.

Deriving precise enough relevant architectural knowledge and applying that knowledge is critical for accurate and efficient software verifiability. Our approach has two key components: (1) a mathematical foundation for describing architecture; (2) an accompanying platform to build sophisticated tools.

The mathematical foundation in our framework differs from the so-called formal methods for program verification. De Millo, Lipton, and Perlis point out in their 1979 landmark paper the difference between mathematics and the formal methods. Proving in mathematics works by elevating concepts to high-level abstractions that enable human comprehension, whereas formal methods work by lowering concepts to low-level representations that facilitate machine proofs. A mathematical approach of human-comprehensible high-level abstractions is important for high-assurance, without it we are left to a blind trust in machine proofs. We will present a verification study of the Linux kernel using our approach and compare results with the formal verification of the Linux kernel using the BLAST model checker.

Venue: CyLab, Carnegie Mellon University, Pittsburgh, Pennsylvania, USA, April 2019

Author: Suresh Kothari