講座時間：2023年11月22（周三）下午15:00
講座地點：BETVLCTOR伟德官方网站216
講座主題：End-to-end Mechanized Proof of an eBPF Virtual Machine for Micro-controllers
主講嘉賓：Jean-Pierre Talpin
講座内容：
RIOT is a micro-kernel dedicated to IoT applications that adopt eBPF (extended Berkeley Packet Filters) to implement so-called femto-containers. As micro-controllers rarely feature hardware memory protection, the isolation of eBPF virtual machines (VM) is critical to ensure system integrity against potentially malicious programs. We show how to directly derive, within the Coq proof assistant, the verified C implementation of an eBPF virtual machine from a Gallina specification. Leveraging the formal semantics of the CompCert C compiler, we obtain an end-to-end theorem stating that the C code of our VM inherits the safety and security properties of the Gallina specification. Our refinement methodology ensures that the isolation property of the specification holds in the verified C implementation. Preliminary experiments demonstrate satisfying performance.
嘉賓簡介：
Jean-Pierre Talpin received the PhD degree from the Université Paris VI Pierre et Marie Curie, France, in 1993. He then was a research associate with the European Computer-Industry Research Centre in Munich before joining INRIA in 1995. He is a senior researcher with INRIA and leads the project-team which develops the open-source Polychrony environment. He has edited two books with Elsevier and Springer, guest-edited more than 10 special issues of ACM and IEEE scientific journals, and authored more than 20 journal articles and book chapters and 60 conference papers. He received the 2004 ACM Award for the most influential POPL paper for his second conference paper with Mads Tofte, and the 2012 LICS Test of Time Award for his first conference paper with Pierre Jouvelot.
