Formal Verification of eBPF interpreter and Just-In-Time compiler

时间：2024-11-20 分类：学术活动

Title:	Formal Verification of eBPF interpreter and Just-In-Time compiler
Speaker:	Shenghao Yuan (袁胜浩), Zhejiang University, China
Time:	2024年11月29日（周五）, 10:00AM
Venue:	中国科学院软件研究所 5号楼3层 337会议室
Abstract:	Modern operating systems have adopted Berkeley Packet Filters (BPF) as a mechanism to extend kernel functionalities dynamically, e.g., Linux’s eBPF or RIOT’s rBPF. The just-in-time (JIT) compilation of eBPF introduced in Linux eBPF for performance has however led to numerous critical issues. Instead, RIOT’s rBPF uses a slower but memory-isolating interpreter (a virtual machine) which implements a defensive semantics of BPF; and therefore trades performance for security. This presentation shows our effort on verified RIOT rBPF interpreter and JIT compiler. The related technique details can be found in CAV22 and CAV24, and the artifacts are available at [1][2]. This talk will also report our recent progress in eBPF and JIT. [1] https://gitlab.inria.fr/x-SYuan/rbpf-dx [2] https://gitlab.inria.fr/x-SYuan/certrbpf-jit
Bio:	Shenghao Yuan is a researcher interested in theorem proving (Coq and Isabelle/HOL), programming language semantics (e.g. Rust and binary), and compiler/OS formal verification. Especially, Linux eBPF-related verification. He received his PhD degree at INRIA and Université de Rennes in December 2023, under the supervision of Jean-Pierre Talpin and Frédéric Besson. He joined Zhejiang University in May 2024.