Title: DeepSpec: Modular Certified Programming with Deep Specifications
Advisor: Zhong Shao
Other committee members:
Bryan Ford (EPFL, Switzerland)
Abstract:Building certifiably reliable and secure system software is one of the grand challenges facing today’s computing community. Despite the extensive progress in programming languages in the past few decades, today’s mainstream operating systems and hyper- visors are still written in C-like low-level languages. There seems to be an inherent clash between high-level formal reasoning and low-level system programming: the former relies on a rich equational theory at a much higher abstraction level while the latter must manipulate and manage low-level effects and hardware resources. The huge abstraction gap between these two tasks makes it difficult to provide direct lan- guage support for programming certified low-level code. Indeed, recent projects on OS kernel verification all required writing (manually) the actual kernel in a C-like lan- guage and a formal specification of the kernel in a proof assistant language; a large part of the verification effort was then spent on showing that the implementation indeed satisfied the specification.
In this work, we present the design and implementation of a new language (named DeepSpec) that can be used to directly program certified system software. To tackle the above-mentioned clash, DeepSpec provides native support for layered specifica- tion and abstraction refinement, full equational reasoning, and effect encapsulation and composition, so it can be used to directly support certified system programming at multiple abstraction levels. Using DeepSpec, a programmer needs only to write the formal specification of a desirable system; then the DeepSpec compiler will au- tomatically compile the DeepSpec program into a certified artifact consisting of a C program (which is then compiled into assembly by CompCert), a Coq specification, and a formal (Coq) proof that the C program satisfies the specification. We have successfully applied the DeepSpec tool chain to build a significant part of a certified OS kernel including the full physical memory and virtual memory managers, and a buffered disk and file manager. We believe that DeepSpec opens up a new space of programming language designs that can directly support the development of correct- by-construction system software.
Dissertation link: http://zoo.cs.yale.edu/~sw475/dissertation.pdf