Compiler Verification and Beyond: Verified Tools for High-Assurance Software

Presented as part of the 2011 HCSS conference.

Abstract

The formal verification of software has progressed tremendously in the last decade. Principled but once academic approaches such as Hoare logic and abstract interpretation finally gave birth to quality verification tools, operating over source code (and not just idealized models thereof) and able to verify complex real-world applications.

The effectiveness of source-level verification is, however, limited by the confidence we can have in the verification tools themselves (are they sound? do they correctly predict all possible executions of the program?) and in the compilers and code generators used to produce the actual executable from a verified source program (couldn’t they miscompile the program and invalidate the guarantees obtained at the source level?).

In this talk, I will give an overview of the CompCert project, which aims at formally verifying a realistic C compiler for critical embedded software, therefore ruling out the possibility of miscompilation. I will then discuss the possibility of applying similar verification techniques to a generic static analyzer based on abstract interpretation, therefore ruling out the possibility of unsoundness in static analysis.

Biography

Xavier Leroy is a senior research scientist at INRIA near Paris, where he leads the Gallium research team. He received his Ph.D. from University of Paris 7 in 1992. His work focuses on programming languages and systems and their interface with the formal verification of software for safety and security. He is the architect and lead author of the Objective Caml functional programming language and of its implementation. He has published about 50 research papers, and received the 2007 Monpetit prize of the French Academy of sciences.