Keel: A Verified In-Kernel Proof Checker for Proof Carrying BPF

Yalu Cai, Tung-Che Chang, Santosh Nagarakatte

Recent systems such as the eBPF Certificate Framework (BCF) and Proof-Carrying BPF address the imprecision in the Linux eBPF verifier with proof-carrying code. When the verifier's abstract domains cannot prove a safety condition, an in-kernel proof checker checks an untrusted user-space refutation proof. A single bug in this checker can compromise the security of the entire kernel. While formalizing BCF's in-kernel checker, we discovered 13 bugs such as unsound rewrite rules, silently unchecked proof steps, and memory safety errors. We demonstrate that forged certificates can trick the kernel to accept arbitrary unsafe eBPF programs. To address this problem, we propose Keel, a formally verified in-kernel proof checker for the Linux eBPF verifier. First, we specify the checker as a pure functional program in Lean and prove its soundness against bit-vector semantics. We decouple the steps of the proof certificate checker from the mathematical rewrite rules, which enables us to extend the rewrite rules without the need to change the checker. Second, we implement the checker in EmbC, a deeply embedded C fragment, and prove that our C implementation refines the functional…