<html><head><meta http-equiv="Content-Type" content="text/html charset=utf-8"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;" class=""><div class=""><div class=""><span class="" style="font-size: 14px;"><b class="" style="font-family: LucidaGrande; background-color: rgba(255, 255, 255, 0);"><u class="">Department of Computer Science </u></b><b class="" style="background-color: rgba(255, 255, 255, 0); font-family: LucidaGrande;"><u class="">Seminar</u></b></span></div></div><div class="" style="font-family: LucidaGrande;"><span class="" style="background-color: rgba(255, 255, 255, 0);"><br class=""></span></div><div class=""><div class="" style="font-family: LucidaGrande;"><span class="" style="font-size: 14px;">Monday, April 10, 2017</span></div><div class="" style="font-family: LucidaGrande;"><span class="" style="font-size: 14px;">2:30 pm</span></div><div class="" style="font-family: LucidaGrande;"><span class="" style="font-size: 14px;">Ryerson 251 </span></div><div class="" style="font-family: LucidaGrande;"><br class=""></div><div class="" style="font-family: LucidaGrande;"><span class="" style="font-size: 14px;">Ronghui Gu</span></div><div class="" style="font-family: LucidaGrande;"><span class="" style="font-size: 14px;">(Yale University)</span></div><div class="" style="font-family: LucidaGrande;"><br class=""></div><div class=""><span class="" style="font-size: 14px;"><span class="" style="font-family: LucidaGrande;">Title: </span><span class="" style="font-family: LucidaGrande;">Building Fully Trustworthy OS Kernels through Formal Verification</span><br class="gmail-m_4827095062818533991gmail_msg"><br class="gmail-m_4827095062818533991gmail_msg"><span class="" style="font-family: LucidaGrande;">Abstract: </span></span></div><div class=""><font face="LucidaGrande" class=""><span class=""><span class=""><span style="font-size: 14px;" class="">Operating System (OS) kernels have a significant impact on the reliability and security of today’s software system. Hence it is highly desirable to verify the OS kernels formally. Recent efforts have demonstrated the feasibility of building large scale formal proofs for the functional correctness of complex systems, 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 based on certified abstraction layers. We show how to specify, program, and compose layers formally and how to support different kinds of concurrency within the kernel. As a case study, we discuss how to verify a practical concurrent OS kernel with fine-grained locking using our CertiKOS framework.<br class=""><br class=""></span><br class=""></span></span></font><span class="" style="font-size: 14px; font-family: LucidaGrande;">-----</span></div><div class=""><font face="LucidaGrande" class=""><span class=""><span class="" style="font-size: 14px;"> </span><span class="" style="font-size: 14px;"><br class=""></span></span></font><span class="" style="font-size: 14px;"><span class="" style="font-family: 'Lucida Grande';">Bio: </span></span></div><div class=""><div class=""><div class=""><font face="LucidaGrande" class=""><span style="font-size: 14px;" class="">Ronghui Gu obtained his Ph.D. degree from Yale University in 2016 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 in 2011, and his honored undergraduate thesis is about verifying the preemptive scheduler of uC/OS-II.</span></font></div></div><div class="" style="font-family: LucidaGrande;"><span class="" style="font-size: 14px;"><br class=""></span></div><div class="" style="font-family: LucidaGrande;"><span class="" style="font-size: 14px;"><br class=""></span></div><div class="" style="font-family: LucidaGrande;"><span class="" style="font-size: 14px;">Host: John Reppy</span></div><div class="" style="font-family: LucidaGrande;"><span class="" style="font-size: 14px;"><br class=""></span></div><div class="" style="font-family: LucidaGrande;"><font size="2" class="">Refreshments in Ry. 255 after the talk</font></div></div></div>
<br class=""></body></html>