Verifier Model
This document describes how Solnix programs are checked against Linux eBPF verifier rules, what guarantees the language provides, and which properties are deferred to the kernel verifier.
1. Background: The Linux eBPF Verifier
- Purpose of the verifier (safety, termination, memory bounds)
- Register state tracking and type system
- Pointer, stack, and map safety rules
- Bounded loops and control-flow constraints
- Helper call validation
2. Solnix Verification Philosophy
- Compile-time enforcement vs kernel-time enforcement
- What Solnix proves statically
- What is left to the kernel verifier
- Design goal: reduce verifier rejections, not replace the verifier
3. Static Checks Performed by Solnix
3.1 Control Flow
- Bounded loops
- No unstructured jumps
- Finite state transitions
3.2 Memory Safety
- Stack bounds
- Map value bounds
- Packet data access ranges
3.3 Type and Pointer Rules
- Strong typing of registers and map values
- Restricted pointer arithmetic
- Context pointer lifetime
3.4 Helper Function Usage
- Argument type checking
- Context-sensitive helper availability
- Return value handling
4. Interaction with the Kernel Verifier
- How Solnix-generated C maps to verifier states
- BTF and CO-RE implications
- Common verifier error classes and how Solnix avoids them
5. Limitations
- No symbolic execution
- No full path-sensitive analysis
- No proof of absence of all verifier failures
- Dependence on kernel version
6. Debugging Verifier Failures
- Using
clang -O2 -target bpf - Inspecting generated C and LLVM IR (optional)
- Using
bpftool prog load --log-level - Mapping kernel verifier errors back to Solnix source
7. Future Work
- Range analysis
- Loop bound inference
- Map value lifetime tracking
- Formal verifier model alignment