Building Certified System Software: Are We Close?

Title: Building Certified System Software: Are We Close?
Speaker: Zhong Shao, Yale University
Time:3:00pm, Thursday April 26
Venue:Lecture room, Lab for Computer Science, Level 3 Building #5, Institute of Software, CAS

Abstract:Certified software consists of a machine executable program plus a rigorous proof (checkable by computer) that the software is free of bugs with respect to a particular specification. Both the proof and the specification are written using a general-purpose mathematical logic, the same logic which all of us use (in reasoning) in our daily life. The logic is also a programming language: everything written in logic, including proofs and specifications, is developed using software known as a proof assistant; they can be mechanically checked for correctness by a small program known as a proof checker. As long as the logic we use is consistent, and the specification describes what the user wants, we can be sure that the underlying software is free of bugs with respect to the specification.

The conventional wisdom is that certified software will never be practical because any real software must also rely on the underlying operating system which is too low-level and complex to be verifiable.In recent years, however, there have been many advances in the theory and engineering of mechanized proof systems applied to verification of low-level code, including proof-carrying code, certified assembly programming, logic-based type system, and certified or certifying compilation. In this talk, I will give an overview of this exciting new area, focusing on key insights and high-level ideas that make the work on certified software differ from traditional style program verification. I will also describe several recent work—done by my group at Yale—on building certified garbage collectors, OS bootloader, thread implementation, and stack-based control libraries.