End-to-end Mechanized Proof of an eBPF Virtual Machine for Micro-controllers

Shenghao Yuan (1) , Frédéric Besson (2) , Jean-Pierre Talpin (1) , Samuel Hym (3) , Koen Zandberg (4) , Emmanuel Baccelli (4)

1 TEA - Tim, Events and Architectures
2 EPICURE - Analyse sémantique et compilation pour la sécurité des environnements d'exécution
3 CRIStAL - Centre de Recherche en Informatique, Signal et Automatique de Lille - UMR 9189
4 TRiBE - inTeRnet BEyond the usual

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.

Mots clés: mechanized proof virtual machines fault isolation; mechanized proof; virtual machines; fault isolation

Domaines: Informatique [cs]

Shenghao Yuan, Frédéric Besson, Jean-Pierre Talpin, Samuel Hym, Koen Zandberg, et al.. End-to-end Mechanized Proof of an eBPF Virtual Machine for Micro-controllers. CAV 2022 - 34th International Conference on Computer Aided Verification, Aug 2022, Haifa, Israel. pp.1-23. ⟨hal-03888082⟩