Modular Development of Certified System Software

Certified software consists of a machine executable program plus a rigorous formal proof (checkable by computer) that the software is free of bugs with respect to a particular 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 both foundational ideas and key insights that make the work on certified software differ from traditional style program verification. I will also describe several recent work on building certified thread implementation, interrupt handlers, stack-based control libraries, garbage collectors, and OS bootloaders.