Verifier

Relevant source files

The verifier is the only producer of VerifiedProgram values. Verifier::verify_with_stats(prog_type, insns, config) returns a BpfProgram plus VerifyStats (states_explored, wcet_cycles, and the proven-constant referenced_map_handles). The kernel manager calls it on every legacy load and again at every attach.

This branch adds two entries that share the same core (verify_inner):

verify_with_stats_bounded(prog_type, insns, config, budget) runs verification under a caller-owned VerificationBudget so every verifier buffer is fallibly allocated and byte-charged (below).
verify_managed_with_stats_bounded(insns, contract, budget) (in verifier/managed.rs) verifies a managed controller against an exact ManagedContract and returns a ManagedProgram, a type that ordinary hooks and the JIT cannot accept.

The legacy sys_bpf load and attach paths still call the unbounded verify_with_stats; only the managed preparation worker uses the bounded entries.

Phases

The managed fragment is loop-free in every profile, including cloud host builds. The ordering is deliberate: profile structural constraints (loop-freedom, forbidden helpers, the WCET budget) run before path-sensitive exploration, so an over-budget or looping embedded program is rejected without paying exploration cost, and the WCET check cannot be masked by the explorer’s state cap.

Control-flow graph

ControlFlowGraph::build computes basic-block leaders, edges, back edges, exit points, and a compressed-sparse-row successor table so successors(i) is proportional to out-degree. This keeps liveness, reachability and WCET passes linear. Any instruction that is not reachable (other than wide-instruction continuations) is UnreachableInstruction.

Abstract state

Each register carries a type from the RegType lattice (NotInit, Scalar, PtrToStack, PtrToMapValue, PtrToMapKey, PtrToCtx, PtrToPacket*, ConstPtrToMap, PtrToFp, NullPtr) and, for scalars, a ScalarValue that combines a known-bits TnumValue with an unsigned interval. Pointers returned by map lookup and ring buffer reserve are maybe-null until a null check clears the flag on the taken branch. Stack state is sparse (StackState), so only touched slots cost memory.

Module	Role
`alu.rs`	Constant folding and tnum propagation through ALU ops, with 32-bit width semantics
`refine.rs`	Tightens scalar ranges on each arm of a conditional branch
`pruner.rs`	State subsumption: skip a path if an earlier state at the same pc covers it
`liveness.rs`	Backward dataflow so differences in dead registers do not block pruning
`map_policy.rs`	Map value sizes, generation-checked handles, and read/write permission checks

The pruner retains at most 8192 states in total (DEFAULT_MAX_STATES) and 64 per program counter (DEFAULT_MAX_STATES_PER_PC). Exceeding the total yields StateLimitExceeded. Exploration uses an explicit worklist rather than recursion, so verification does not grow the kernel stack with branch nesting.

Stack depth across branch joins

Commit c977440 fixed an under-report of the program’s stack size. main recorded one state per program counter and took the maximum depth over that table after exploration, so a later shallow path reaching a join point could overwrite the state of an earlier deeper path. The branch keeps a running max_stack_depth that is updated for every explored state before pruning. The regression program needs 64 bytes where the previous implementation reported 16. Because the interpreter zeroes only the verified stack suffix, this value matters at run time.

Context payload provenance

Commit ed46a6b splits the context pointer type. PtrToCtx now means only the BpfContext wrapper at entry; a pointer obtained from its data field is PtrToCtxData, a read-only view of payload bytes whose loaded fields are plain scalars. A scalar loaded from the payload therefore cannot be dereferenced as if it were the wrapper’s data pointer, while payload pointers can still be copied, offset and passed to helpers that accept context memory.

What is checked

Structure: empty program, no exit, instruction count over MAX_INSN_COUNT, invalid opcodes, registers above 10, invalid jump targets.
Registers: use of uninitialized registers, writes to r10 (the frame pointer), division by a provably zero divisor (including after 32-bit truncation).
Memory: stack, context and map-value accesses are bounds-checked against sizes supplied in VerifyConfig; dereferencing a maybe-null pointer is rejected (MisalignedAccess exists as an error variant; its exact trigger conditions were not traced for this page). With the zero-config verify() entry, context and map-value accesses are rejected because no region size is known.
Context size: R1 is bounded to size_of::<BpfContext>() for every hook; the per-hook payload reached through BpfContext::data is bounded by ctx_data_size (see Hooks).
Helpers: ID must be known and available in the active profile, argument count and register types must match the signature, and the caller must satisfy the helper’s tier (below).
Maps: constant map handles must resolve in the generation-checked table; a lookup yields exactly that map’s value size; a dynamic handle is bounded to the smallest map and is rejected if any map is unavailable or write-only. Mutating helpers (map_update_elem, map_delete_elem, ringbuf_output, timeseries_push) require a provably writable map handle; stores through a read-only lookup are rejected.
Implicit map helper inputs (new, commit c0c0d01): map helpers read fixed-size key and value buffers whose lengths are not in their bytecode signatures. VerifyConfig now carries per-map key sizes as well as value sizes, and the verifier checks that each key or value pointer is readable for the target map’s full extent and that stack-backed bytes are initialized. A known handle uses that map’s exact size; a dynamic handle must satisfy the largest reachable map. A lookup value pointer used as an update or timeseries_push source must be at least the destination value size, counting any nonzero offset. Empty size tables keep the standalone verifier’s earlier type-only behaviour.
Stack: computed maximum depth must fit the profile (StackExceeded).

Caller tiers and helper policy

VerifyConfig carries caller (Unprivileged, Privileged, Trusted), allow_actuation, and forbid_logging_helpers. A helper signature can set a minimum tier, require actuation authority, or be marked as possibly logging. verify_call raises HelperRequiresPrivilege, ActuationCapabilityRequired or LoggingHelperForbidden accordingly. The helper table is on Maps and Helpers.

Bounded verifier storage

Commit 1f334bd (with allocator rounding added in 984f98f) introduces verifier/budget.rs. A VerificationBudget is a caller-owned byte allowance shared by one verification. All preparation-path growth goes through BudgetVec: the CFG, liveness tables, the pruner’s per-pc state lists, sparse stack storage, the WCET dynamic-programming table, referenced-handle lists and the output code copy. Growth counts both the old and the replacement buffer while they overlap, and any exhaustion returns VerifyError::ResourceExhausted instead of panicking or aborting.

Scratch buffers refund automatically on every exit.
Successful output buffers (code and handle vectors) stay charged until their owner calls release_output or transfers the charge.
VerificationBudget::with_allocator_policy(limit, minimum, quantum) raises each nonempty request to the allocator’s minimum and rounds to its quantum. The preparation worker uses 16 bytes and 8 bytes to match the pinned linked_list_allocator.
Test builds can inject a failure at any reservation. The plan records failure injection across every reservation of a representative branching, stack and map program.

The cumulative state cap (DEFAULT_MAX_STATES) still bounds exploration work separately from the byte allowance.

Managed verification

verifier/managed.rs holds the managed contract. ManagedContract::new(manifest, signer_effects, slot_effects) rejects effect bits other than EFFECT_MOTOR_PAIR and invalid private-array declarations (UnsupportedManagedContract), and keeps the intersection of the signed, signer-policy and slot effect ceilings. Verification then enforces, in addition to the ordinary checks:

Only map lookup, private-array update and bpf_managed_motor_pair_v1 (1009) are callable; other helpers fail with HelperModeMismatch, and 1009 is likewise refused to ordinary programs.
Map handles must be proven constants 0 (read-only envelope, if declared) or 1 (private array, if declared) with local generation zero; both use four-byte keys.
The motor helper requires the motor effect in the intersected ceiling (ManagedEffectRequired).
Normalized code only: no pseudo calls or bindings, no malformed wide immediates, no loops. Pointer spills and pointer-to-scalar conversion are rejected.

BehaviorArtifact::prepare decodes the authenticated bundle into a budgeted buffer, runs this verification, and keeps the identity, contract, code, wcet_cycles and the exact output charge. See Managed Bundles.

WCET bound and admission

cost.rs assigns a static cost in relative cycle units to each instruction and computes the program’s WCET as a fixed invocation base (95 units) plus the longest path through the loop-free CFG, using a single reverse dynamic-programming pass.

Instruction class	Cost
Default (cheap ALU, jump, mov, exit)	1
Memory load/store	2
Division and modulo	2
Helper: counter reads (ktime, cpu id, prandom, pid, uid, latency, boot time, heap, image, sensor timestamp)	4
Helper: copies and device access (probe_read, comm, GPIO, PWM, motor pair, managed motor pair, IIO, CAN)	10
Helper: ring buffer (output, reserve, submit, discard)	12
Helper: map operations (lookup, update, delete, timeseries push)	16
Helper: trace_printk	20
Unknown helper ID	8

On main the cost constants were described as conservative bounds calibrated against a 2026-06-11 Raspberry Pi 5 JIT run. On this branch the same weights are kept but the source calls them retained model values that “do not qualify the shipped interpreter”; the managed capture helper is placed in the copy class as uncalibrated bookkeeping. The source also notes that trace_printk’s real cost is serial-I/O-bound and is not modeled by its weight, so it is banned by policy instead.

Two enforcement points use the result on the embedded profile:

Per-program budget (verifier). wcet_cycles above WCET_CYCLE_BUDGET (RT_PERIOD_NS / CYCLE_UNIT_NS, now 10,000,000 / 6, about 1,666,666 units; it was 1,000,000 / 6 on main) is rejected with WcetExceeded. Any back edge is rejected with UnboundedLoop, and bpf_trace_printk with HelperForbiddenOnRtFragment. On the cloud profile the budget is u64::MAX and back edges are not rejected by this check; non-terminating exploration is bounded by MAX_INSN_COUNT per path (InfiniteLoop) and the state budget.
Utilization admission (kernel, at attach). AdmissionLedger::admit adds wcet_cycles * CYCLE_UNIT_NS * freq_hz nanoseconds of CPU per second for the attachment, and refuses (AdmissionRejected) if the total would exceed UTILIZATION_BUDGET_NS_PER_S (500,000,000 on embedded, i.e. half a core). Detach releases exactly what attach committed. BpfManager::hook_frequency_hz assumes every hook fires at the control-loop rate (now 100 Hz on embedded); per-hook frequencies are noted in source as future work. On cloud the frequency is 0 and the budget unbounded, so admission never rejects.
Managed reservation (new). The ledger gains one fixed managed contribution at 100 Hz. prepare_managed reserves the larger of the active and replacement costs (never their sum, because the two controllers never run together) without allocating; legacy attachments see that reservation and cannot take it. finish_managed settles the charge from the worker after the slot outcome is known, so the timer’s publication path never mutates the ledger. Cancellation and failure keep the old charge.

This is a load-time utilization ledger, not an EDF scheduler. On this branch CYCLE_UNIT_NS = 6 is explicitly labeled an unqualified model value; v0.5 requires a retained Pi 5 interpreter corpus (the verifier-cost shapes) before the budgets become a timing claim. Treat them as policy constants, not proven timing guarantees.

Limits summary

Limit	Cloud	Embedded	Source
Instructions	1,000,000	100,000	`PhysicalProfile::MAX_INSN_COUNT`
Stack	512 KiB	8 KiB	`MAX_STACK_SIZE`
WCET per program	unbounded	about 1,666,666 units	`WCET_CYCLE_BUDGET`
Managed verifier and artifact-wrapper workspace	512 KiB	512 KiB	reserved at upload finalize (`managed-runtime`)
Verifier recorded states	8192 total, 64 per pc	same	`StatePruner`
Subprogram call depth	8	8	loader `normalize`
Raw `BPF_PROG_LOAD` instruction count	4096	4096	`sys_bpf`
ELF payload	1 MiB	1 MiB	`BpfLimits::max_elf_bytes`

Selected `VerifyError` variants

InvalidOpcode, InvalidRegister, UninitializedRegister, OutOfBoundsAccess, InvalidMemoryAccess, UnreachableInstruction, InfiniteLoop, StateLimitExceeded, InvalidJump, NoExit, EmptyProgram, InvalidHelper, HelperRequiresPrivilege, ActuationCapabilityRequired, LoggingHelperForbidden, PointerLeakUnprivileged, HelperNotAvailable, InvalidMapId, WriteToReadOnlyMap, WriteMapNotProvablyWritable, HelperArgCount, HelperArgType, DivisionByZero, StackExceeded, InsnCountExceeded, WriteToReadOnly, MisalignedAccess, WcetExceeded, InterruptUnsafe, DynamicAllocationAttempted, UnboundedLoop, HelperForbiddenOnRtFragment, and new on this branch ResourceExhausted, UnsupportedManagedContract, HelperModeMismatch and ManagedEffectRequired. UnboundedLoop is no longer embedded-only because the managed fragment uses it on every profile. Every variant carries the failing instruction index where one applies.

Assurance

The fuzz targets verify_only (termination and no panics) and verify_then_exec (a verified program must execute without panicking in the interpreter) exercise this code; the fuzz README states the PR smoke job runs verify_only for 60 seconds and a weekly job runs longer campaigns. Building the kernel with the verifier-cost feature emits per-load cost markers on the UART.