[Adapt] Fwd: Talk by Prof. Zhong Shao from Yale University

[Kenny Zhu]

Hi guys,

Go to this talk if you are interested. Zhong Shao is a well known researcher in PL.

Kenny


Begin forwarded message:

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

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://cs.sjtu.edu.cn/pipermail/adapt/attachments/20140605/292ae7e9/attachment.html>