计算机学院系列讲座菁英论坛28期——End-to-End Mechanized Proof of an eBPF Virtual Machine for Micro-controllers

报告题目(Title)：End-to-End Mechanized Proof of an eBPF Virtual Machine for Micro-controllers

时间(Date & Time)：2024.5.7；10:00-12:00

地点(Location)：智华楼 413

腾讯会议：137 984 465

主讲人(Speaker)：Jean-Pierre Talpin

邀请人(Host)：詹乃军

报告摘要(Abstract)：

RIOT is a micro-kernel dedicated to IoT applications that adopts 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. This paper shows 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.

DOI: https://dl.acm.org/doi/abs/10.1007/978-3-031-13188-2_15

主讲人简介(Bio)：

Jean-Pierre Talpin is a senior scientist  with INRIA. He received a Master degree in Theoretical Computer Science from University Paris VI and did his Ph.D. Thesis with Ecole des Mines de Paris under the supervision of Pierre Jouvelot. He joined INRIA in 1995, to lead project-teams ESPRESSO and TEA from 2000 to 2023.  Jean-Pierre Talpin received the 2004 ACM Award for the most influential POPL paper and the 2012 ACM/IEEE LICS Test of Time Award.

From his career-long studies in logic, type, concurrency theory and experiences in program analysis and verification, his research interests have focused on challenging topics such as the end-to-end mechanized program verification, the design of advanced process calculi  to model t cyber-physical system networks and of the compositional algebraic methods to verify them. 

欢迎关注计算机学院微信公众号，了解更多讲座信息！

北京大学计算机学院