<html><head><meta http-equiv="Content-Type" content="text/html charset=us-ascii"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;">Hi guys,<div><br></div><div>Go to this talk if you are interested. Zhong Shao is a well known researcher in PL.</div><div><br></div><div>Kenny</div><div><br><div><br><div>Begin forwarded message:</div><br class="Apple-interchange-newline"><blockquote type="cite"><div style="margin-top: 0px; margin-right: 0px; margin-bottom: 0px; margin-left: 0px;"><span style="font-family:'Helvetica'; color:rgba(0, 0, 0, 1.0);"><b>From: </b></span><span style="font-family:'Helvetica';">Yijia Chen <<a href="mailto:yijia.chen@cs.sjtu.edu.cn">yijia.chen@cs.sjtu.edu.cn</a>><br></span></div><div style="margin-top: 0px; margin-right: 0px; margin-bottom: 0px; margin-left: 0px;"><span style="font-family:'Helvetica'; color:rgba(0, 0, 0, 1.0);"><b>Subject: </b></span><span style="font-family:'Helvetica';"><b>Fwd: Talk by Prof. Zhong Shao from Yale University</b><br></span></div><div style="margin-top: 0px; margin-right: 0px; margin-bottom: 0px; margin-left: 0px;"><span style="font-family:'Helvetica'; color:rgba(0, 0, 0, 1.0);"><b>Date: </b></span><span style="font-family:'Helvetica';">June 5, 2014 at 5:14:56 PM GMT+8<br></span></div><div style="margin-top: 0px; margin-right: 0px; margin-bottom: 0px; margin-left: 0px;"><span style="font-family:'Helvetica'; color:rgba(0, 0, 0, 1.0);"><b>To: </b></span><span style="font-family:'Helvetica';"><<a href="mailto:kzhu@cs.sjtu.edu.cn">kzhu@cs.sjtu.edu.cn</a>><br></span></div><br><div>Hi Kenny,<br><br>Tomorrow we will have a talk which might interest you<br>and your group as well.<br><br>Best,<br><br>Yijia<br><br><br>-------- Original Message --------<br>Subject: Talk by Prof. Zhong Shao from Yale University<br>Date: Wed, 4 Jun 2014 15:38:32 +0800<br>From: Yijia Chen <<a href="mailto:c.yijia.chen@googlemail.com">c.yijia.chen@googlemail.com</a>><br>To: <a href="mailto:tcs-at-shanghai@googlegroups.com">tcs-at-shanghai@googlegroups.com</a>, <a href="mailto:zhong.shao@yale.edu">zhong.shao@yale.edu</a><br>Reply-To: <a href="mailto:tcs-at-shanghai@googlegroups.com">tcs-at-shanghai@googlegroups.com</a><br><br>Zhong Shao (Yale University, USA)<br><br>Time: 14:00-15:00, June 6, 2014<br>Venue: Room 318, SEIEE-3<br><br>Title: CertiKOS: Compositional Layered Specification and Verification<br>of a Hypervisor OS Kernel<br><br>Abstract:<br>Operating System (OS) kernels and hypervisors form the backbone of all<br>system software. They can have the greatest impact on the resilience,<br>extensibility, and security of today's computing hosts. Recent effort<br>on seL4 has demonstrated the feasibility of building large scale formal<br>proofs of functional correctness for a general-purpose microkernel,<br>but the cost of such verification is still prohibitive, and it is<br>unclear how to use such a verified kernel to reason about user-level<br>programs and other kernel extensions.<br><br>In this talk, I will present a novel compositional approach for formally<br>specifying and verifying OS kernels. Because the very purpose of an OS<br>kernel is to build layers of abstractions over hardware resources, we<br>insist on uncovering and specifying these layers formally and then<br>performing the verification of each kernel function at its proper<br>abstraction layer. To support linking with other kernel extensions and<br>user-level programs, we prove a stronger contextual refinement<br>property for every kernel function, which states that the<br>implementation of each such function will behave like its functional<br>specification under any kernel/user or host/guest context. Our abstraction<br>layers are defined as assembly-level machines extended with abstract<br>kernel primitives, but almost all of our kernel programs are written in a<br>variant of CompCert Clight language, verified at the source level, and<br>compiled and linked together using a modified version of the CompCert<br>compiler. To demonstrate the effectiveness of our new methodology, we<br>have successfully implemented and specified a realistic hypervisor OS<br>kernel and verified its (contextual) functional correctness property<br>in the Coq proof assistant. Our hypervisor kernel is written in 3000<br>lines of C and x86 assembly, and can successfully boot a version of<br>Linux as a guest. The entire specification and proof effort took less<br>than one person year.<br><br><br>Short Bio:  Zhong Shao is Professor of Computer Science at Yale University.<br>He received his PhD degree in Computer Science from Princeton University<br>in 1994.  His research interests include certified code, programming<br>languages and compilers, program verification, formal  methods, and<br>operating systems.  He was a key developer of the Standard ML of<br>New Jersey system and the architect of the FLINT certifying compiler<br>infrastructure. He currently leads the Yale FLINT group to build a practical<br>infrastructure for constructing large-scale certified system software.<br><br>-- <br>You received this message because you are subscribed to the Google Groups "TCS at Shanghai" group.<br>To unsubscribe from this group and stop receiving emails from it, send an email to <a href="mailto:tcs-at-shanghai+unsubscribe@googlegroups.com">tcs-at-shanghai+unsubscribe@googlegroups.com</a>.<br>For more options, visit <a href="https://groups.google.com/d/optout">https://groups.google.com/d/optout</a>.<br><br></div></blockquote></div><br></div></body></html>