Making an eBPF Virtual Machine Faster on Microcontrollers: Verified Optimization and Proof Simplification

As a revolutionary kernel extension technology, Berkeley Packet Filters (BPF) has been applied for various operating systems from different domains, from servers (Linux’s extended BPF) to microcontrollers (RIOT-OS rBPF). Previous works have formally proved the memory isolation property for the non-optimized rBPF virtual machine in the Coq proof assistant. In this paper, we introduce a verified optimization for rBPF, and highlight a novel proof approach for optimization correctness: a simplification process is first used to transform monadic models with option state to simplified non-monadic models with inline arguments; then the optimization correctness theorem is split into i) proving simplification correct and ii) proving the optimization correctness on simplified models. Our proof approach enjoys a fruitful proof simplification. Preliminary experiments demonstrate satisfying performance.