Validating the eBPF Verifier via State Embedding
Talkat 18th USENIX Symposium on Operating Systems Design and Implementation (OSDI '24) · 2024-07-10..07-12·
summary
State embedding validates the eBPF verifier by taking concrete runtime states from profiling and folding, encoding them into an eBPF program so the verifier must prove those concrete states lie inside its abstract approximation; if the transformed program P' is accepted then the verifier is unsound. The implemented tool folds many traces into a single register (e.g. R9) and embeds conditional checks, and within one month finds 15 logic bugs—10 fixed and 2 exploitable for local privilege escalation.
AI-written summary · about
chapters (5)
- 0:00The verification challenge
- 4:20Overview of eBPF verifier
- 6:56State embedding technique
- 11:33Results and bug analysis
- 14:25Conclusion and summary
related talks
26mVerifying the Verifier eBPF Range Analysis Verification
17mVEP: A Two-stage Verification Toolchain for Full eBPF Programmability
42mA Deep Dive Into eBPF Program Loader
43meBPF Superpowers for SRE
01h 03mBPF and Spectre: Mitigating transient execution attacks
14mA Flow-Sensitive Refinement Type System for Verifying eBPF Programs
38mAlice in Kernel Land: Lessons Learned From the eBPF Rabbit Hole
31meBPF 101