beat365系列講座菁英論壇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. 

歡迎關注beat365微信公衆号，了解更多講座信息！

beat365官方网站