Monday, December 10, 2018
12:00 PM
Wegmans Hall 1400
Professor Zhong Shao
Yale University
CertiKOS: From Hacker-Resistant OS to Certified Heterogeneous Systems
Computer science is being transformed by new exciting "vertical" research themes such as IoTs, self-driving cars, blockchains, and robotics. These new themes often require complex computing platforms involving not only heterogeneous hardware and software components but also physical, human, and social entities. The successful deployment of these technologies would critically depend on our ability to establish strong properties such as safety, security, resilience, resource efficiency, fairness, and privacy. In this talk, I present a novel compositional approach for building certified heterogeneous systems that aim to provide many such trustworthiness guarantees. We advocate abstraction over a particularly rich class of specification and present new methodologies and tools for formally specifying, programming, verifying, and composing abstraction layers. Using these new technologies, we have successfully developed the CertiKOS certified OS kernel and verified its contextual functional correctness in the Coq proof assistant. This is the world's first proof of functional correctness of a complete, general-purpose concurrent OS kernel with fine-grained locking. We show how to extend our base kernel with new features such as virtualization, interrupts and device drivers, and end-to-end information flow security, and how to quickly adapt existing verified layers to build new certified kernels for modern heterogeneous platforms.