CSE Colloquium: Ronghui Gu

Ronghui Gu, Research Associate, Yale University

Monday, February 27, 2017

11:30-12:30pm

HBL Class of 1947 Conference room

(located behind Bookworms in the Library)

Title: Building Fully Certified OS Kernels

Operating System (OS) kernels have a significant impact on the reliability and security of today’s software system. Hence it is highly desirable to formally verify the OS kernels. Recent efforts have demonstrated the feasibility of building large scale formal proofs for the functional correctness of simple kernels, but the cost of such verification is still prohibitive, and it is unclear how to extend their verified kernels to support concurrency. In this talk, we present CertiKOS, an extensible architecture for building certified sequential and concurrent OS kernels with certified abstraction layers. We show how to specify, program, and compose layers formally and how to support different kinds of concurrency within the kernel. We also discuss how to verify a practical concurrent OS kernel with fine-grained locking using our CertiKOS framework.

Bio:

Ronghui Gu obtained his Ph.D. degree from Yale University under the supervision of Prof. Zhong Shao. His research interests are programming languages and operating systems, with a focus on certified system software, concurrency reasoning,  and language-based support for safety and security. His primary research work is the design and implementation of the CertiKOS framework. Ronghui obtained his B.S. degree from Tsinghua University, and his honored undergraduate thesis is about verifying the preemptive scheduler of uC/OS-II.