Description

Create a toy BPF verifier in Lean 4 that models the Linux kernel's BPF verifier behavior. This implementation provides a formally verifiable foundation for understanding verifier correctness—crucial for security-critical BPF programs in production environments.

The reference monitor enforces runtime safety properties (register initialization, type safety) while the verifier performs static analysis to prove programs satisfy these properties before execution. This separation enables formal reasoning about verifier soundness: if the verifier accepts a program, the reference monitor will never reject it.

Code: https://github.com/shunghsiyu/toy-verifier

Goals

• ✓ BPF virtual machine interpreter (MOV, ADD, SUB)
• ✓ Reference monitor with register initialization checks
• Verbose error reporting with detailed diagnostics
• Verifier abstraction layer for static analysis
• Prove basic soundness property: "verifier acceptance → reference monitor never fails"
• Support forward jumps (enabling control flow)
• Additional ALU operations (MUL, DIV, shifts)
• Stack-based memory instructions (LD/ST)
• BPF maps (array map as initial target)
• Helper call modeling (tail calls)

Resources

• Lean 4 Documentation
• Proof-Carrying Code (Necula & Lee, 1996)
• Linux BPF Verifier Source
• Intro to the Lean Theorem Prover | Jakob von Raumer (Lindy Labs) - DSS 101 2024
• Last year's Hack Week: Model checking the BPF verifier