联系我们


学院办公室:89534639

学生工作办公室:89534640

89534638

重点实验室:89534290

实验室办公室:89534104

协同创新中心:80570780

11月22日 15:00 Jean-Pierre Talpin:eBPF虚拟机的端到端形式化验证

2023-11-22  点击:

讲座时间:20231122(周三)下午15:00

讲座地点:2024欧洲杯买球网站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.




关闭