Description

Create a toy BPF verifier in Lean 4 (https://lean-lang.org/) 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.

Create a toy BPF verifier in Lean 4 that models the Linux kernel's BPF verifier behavior. This project builds the components of a formally verifiable system from the ground up to demonstrate verifier correctness—a crucial property for security-critical BPF programs.

The project is architected in several layers:

1. A Concrete Interpreter: First, a simple BPF virtual machine is implemented to define the operational semantics of the toy language.
2. A Secure Reference Monitor: This interpreter is then instrumented with runtime safety checks (e.g., for register initialization) to create a "ground truth" for safe execution. The monitor will halt a program if it attempts an unsafe operation.
3. A Static Verifier: The core of the project is a verifier that analyzes BPF code without running it. Using abstract interpretation, it predicts whether a program could ever fail the runtime safety checks.
4. A Formal Proof of Soundness: Finally, the separation of these components allows for the ultimate goal: proving that the static verifier is sound. We use Lean's theorem-proving capabilities to formally guarantee that if the verifier accepts a program, the reference monitor will never halt it for a safety violation.

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

Goals

• ✓ BPF Virtual Machine Interpreter: Implemented a functional interpreter for a core BPF-like instruction set including MOVK, MOVX, ADDK, ADDX, SUBK, and SUBX.
• ✓ Reference Monitor: Built an instrumented runner (Secure.run) that checks for safety properties like register initialization before executing each instruction at runtime.
• ✓ Static Verifier: Designed and implemented an abstract interpreter (Verifier.check) that statically proves programs are free from initialization errors without actually running the code.
• ✓ Verbose Error Reporting: Defined a custom Error type to represent failures, enriched with contextual information like program counter and register ID.
• Formalize and Prove Soundness: Check that the verifier is correctly implemented by proving the basic soundness property: "verifier acceptance → reference monitor never fails".
  • ✓ The Bridge: Formally proved that the single-step logic of the verifier and the monitor are synchronized through key lemmas like instructionSafeconsistent and stepconsistent.
  • ✓ The Loop Lemma: Prove via induction that if each step preserves consistency, the entire program execution loop does as well.
  • The Main Theorem: Assemble the lemmas to prove the final soundness theorem, providing a top-to-bottom guarantee of verifier correctness.

Future Work

• Implement a macro for a more user-friendly BPF assembly syntax (e.g., mov r0, 7; or r0 = 7;).
• Enhance the verifier's abstract domain to track value ranges, not just initialization status.
• Add support for control flow via forward jumps (e.g., JEQ).
• Add support for control flow via backward jumps/loop.
• Expand the instruction set with more ALU operations (MUL, DIV, AND, OR, XOR, shifts).
• Add support for memory access (stack, BPF maps) with pointer tracking and bounds checking.
• Create a BPF-to-native-code JIT compiler.
• Prove the correctness of a BPF-to-native-code JIT compiler (a refinement proof).

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