Operating System (OS) kernels form the bedrock of all system software---they can have the greatest impact on the resilience, security, and extensibility of today's computing hosts (e.g., phones, workstations, clouds, self-driving cars, drones, IoTs) .  A single kernel bug can easily wreck the entire system's integrity and protection. It is thus highly desirable to build hacker-proof OS kernels that strictly adhere to their formal functional specification under all circumstances.

Building certifiably hacker-proof OS kernels is widely considered a grand challenge. Many people believe that the combination of concurrency and the OS kernels' functional complexity makes formal verification of functional correctness intractable, and even if it is possible, its cost would be prohibitive.

Under this research grant, PI Shao and his team at Yale University have successfully made multiple breakthroughs showing that building hacker-proof operating systems is not only feasible but also practical.

In their paper on Deep Specifications and Certified Abstraction Layers (appeared in the Proceedings of the 42nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015), they developed a novel language-based account of certified abstraction layers and advocated abstraction over a particularly rich class of specification which they call deep specifications. They then developed new methodologies and tools for formally specifying, programming, verifying, and composing abstraction layers. Using these new languages and tools, they have successfully developed multiple certified sequential OS kernels in the Coq proof assistant, the most realistic of which consists of 37 abstraction layers, took less than one person year to develop, and can boot a version of Linux as a guest.

In two other research papers (published in the Proceedings of 2016 ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2016), they showed that their layered compositional framework can be extended to support interruptible OS kernels and device drivers; they have also successfully developed a novel methodology for formally verifying end-to-end security of a software system that consists of both C and assembly programs.  Using these new methodologies, they have successfully constructed an end-to-end security proof of their CertiKOS kernel (running on an extended x86 assembly machine model).

In their latest paper (to be published in the Proceedings of 2016 USENIX Symposium on Operating Systems Design and Implementation, OSDI 2016), PI Shao and his team developed another highly novel compositional approach for building certified hacker-proof concurrent OS kernels. Concurrency allows interleaved execution of kernel/user modules across different layers of abstraction. Each such layer can have a different set of observable events. They insist on formally specifying these layers and their observable events, and then verifying each kernel module at its proper abstraction level. To support certified linking with other CPUs or threads, they prove a strong contextual refinement property for every kernel function, which states that the implementation of each such function will behave like its specification under any kernel/user context with any valid interleaving. They have successfully developed a practical concurrent OS kernel and verified its (contextual) functional correctness in Coq. Their certified kernel is written in 6500 lines of C and x86 assembly and runs on stock x86 multicore machines. This is the world's first proof of functional correctness of a complete, general-purpose concurrent OS kernel with fine-grained locking.

On the education side, PI Shao has developed a new course on operating system design and implementation at Yale. This is a hard core kernel programming course, known notoriously for its extremely heavy programming load---as a result, normally less than 15 students took this course at Yale each year. PI Shao redesigned this course and used the multi-layered CertiKOS OS kernel as the programming labs.  Because CertiKOS was constructed with an extremely clean specification and a set of well-organized abstraction layers; students get to focus on the OS related issues rather than be bogged down by low-level debugging. As a result, 44 students successfully finished the course in the fall term of 2015. The course received very good reviews. This project also helped train many research and teaching skills to a large number of post-doctoral research associates, graduate students, and undergraduate students at Yale.

Last Modified: 10/17/2016
Modified by: Zhong Shao