[2022-04-06] Seminar on “End-to-end Mechanised Proof of an eBPF Virtual Machine for Microcontrollers”

Shenghao Yuan (PhD student) from Inria will give a presentation at our seminar next Wednesday afternoon (16:00, Apr. 6). The Zoom ID is 810 4464 5604

Title: End-to-end Mechanised Proof of an eBPF Virtual Machine for Microcontrollers

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 proposes a methodology to directly derive the verified C implementation of an eBPF virtual machine from a Gallina specification within the Coq proof assistant. Leveraging the formal semantics of the CompCertC compiler, we obtain an end-to-end theorem stating that the C code of our VM inherits safety and security properties of its Gallina specification. Our refinement methodology ensures that the isolation property of the specification holds in the verified C implementation. Preliminary experiments demonstrate satisfying performances.