Verifier

The verifier is the contract between userspace and the kernel: bytecode that cannot be proven safe is never executed. The current implementation performs control-flow analysis, abstract interpretation with tnum and range refinement, per-instruction liveness, and state pruning.

Pipeline

1. parse bytecode → instructions
2. build control-flow graph (CFG)
3. assert termination
     · every back-edge requires a bounded-iteration witness
4. abstract interpret
     · tnum (known-bits) tracking
     · signed/unsigned range tracking
     · range refinement after conditional branches
5. assert invariants
     · stack depth ≤ profile limit
     · memory accesses fall within registered regions
     · all paths terminate
6. emit Verified { bytecode, summary } | VerifyError

Skeleton

fn verify_program(bytecode: &[u8]) -> Result<Verified, VerifyError> {
    let cfg = build_cfg(bytecode)?;

    for node in cfg.nodes() {
        if has_backedge(node) && !has_bounded_iter(node) {
            return Err(VerifyError::UnboundedLoop);
        }
    }

    let abs = abstract_interpret(&cfg)?;
    abs.assert_stack_depth(STACK_LIMIT)?;
    abs.assert_memory_access(&cfg)?;

    Ok(Verified { bytecode, abs })
}

Profiles

The same verifier supports multiple physical-reality profiles. Embedded profile caps the stack at 8 KB and disables the JIT; cloud profile permits 512 KB and enables aarch64 JIT. Selection is at compile time via sealed traits.

#[cfg(feature = "embedded-profile")]
type BpfProfile = profile::EmbeddedProfile;

#[cfg(feature = "cloud-profile")]
type BpfProfile = profile::CloudProfile;

What the verifier guarantees

• Termination. No path runs forever.
• Bounded stack. Static bound on stack growth.
• Validated memory access. Every load and store hits a registered region with a verified size.
• Helper signature conformance. Helper calls take and return values within declared types.

What the verifier does not guarantee

• Functional correctness. A program may be safe yet useless.
• Wall-clock bounds. Termination ≠ promptness; profile-level instruction caps are used at execution.