Fuzzing the Verifier with a Test Oracle
summary
Proposal implements a test oracle that saves verifier expectations into a BPF map of verifier states and at runtime performs interpreter runtime checks of concrete register/scalar ranges and TM bits, issuing warnings when values deviate. RFC patchset targets registers only, checks scalar ranges, uses an LDM imm64 sentinel instruction today, and exposes states to userspace. Prototype reproduces a historical sign-loss bug (spill −44) but is not yet integrated with fuzzers or subprog-aware and needs refinement.
AI-written summary · about
chapters (7)
- 0:00Introduction to BPF verifier fuzzing
- 1:04False negatives in the verifier
- 2:24Academic approach to test oracle
- 5:58Simplified test oracle design
- 8:06Example of verifier bug detection
- 11:19Implementation challenges
- 14:54Conclusion and next steps
related talks
38mAlice in Kernel Land: Lessons Learned From the eBPF Rabbit Hole
01h 03mBPF and Spectre: Mitigating transient execution attacks
24mGenerating BPF Verifier Friendly Code with Clang
26mDifferential Testing with Foundry
50mWhat the Fuzz
29mVirtual Device Fuzzing Support in QEMU
50mTrust but Verify: Scaling Deductive Verification with Abstract Interpretation
24mVerification of Hardware and Software with Fuzzing and Proofs