← 研踪 PaperTrailarXiv:2611.11117 · v1
Keel: A Verified In-Kernel Proof Checker for Proof Carrying BPF
首次提交 2026-11-08 12:03
版本更新 2026-11-08 12:03
雷达观测 2026-11-10 12:16
摘要
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 specification without undefined behavior or memory leaks. Third, using an amortized potential argument, we prove linear time and memory bounds for the C checker. Keel is correct-by-construction while also being faster than the BCF checker inside the kernel, 1.3X in total and 2.0X on the slowest 1.4% of certificates.
作者备注：66 pages
观测到的版本
相邻记录可能跳过中间版本；首次发现 v2 及以上也会标为版本更新。
v1 · 2026-11-08 12:03 · 最新观测版本
Keel: A Verified In-Kernel Proof Checker for Proof Carrying BPF
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 specification without undefined behavior or memory leaks. Third, using an amortized potential argument, we prove linear time and memory bounds for the C checker. Keel is correct-by-construction while also being faster than the BCF checker inside the kernel, 1.3X in total and 2.0X on the slowest 1.4% of certificates.
查看此版本解读 →查看此版本原文 ↗