Repository navigation
Introduce Kani bounded verification over the pure security-load-bearing cores #1109
Description
Summary
Introduce Kani (a bit-precise bounded model checker for Rust) as a CI-grade verification tool over a handful of minimal's pure, security-load-bearing cores. Proof harnesses look like fuzz targets, run in CI, and prove properties like "never panics on hostile input", "never reads out of bounds", and small algebraic laws — over all inputs within a bound, not just sampled ones.
This is deliberately scoped as additive and non-breaking: no BuildSpec changes, no cache-key changes, no format changes. Harnesses live behind #[cfg(kani)], land independently, and need no maintainer decisions to start. It's the pragmatic floor of the verification story from the formal-methods audit — value today, and a concrete stepping stone toward the deeper Aeneas/Lean question without committing to that toolchain.
Why Kani, why here
The audit identified a set of pure "kernel" cores that parse or combine untrusted input — bytes from a bucket/CDN/mirror our own trust model explicitly treats as hostile, or path decisions where a reorder could be an escape. These are the textbook Kani sweet spot: small, pure, owned data in, bounded input space. AWS runs Kani in CI on Firecracker, s2n-quic, and the Rust std-lib verification campaign (16k+ harnesses/change), so the CI pattern is well-trodden.
Two of the targets below already ship defenses (a varint-overflow guard; a MAX_VARINT_LEN DoS cap). Kani's job there is to prove the defense holds for every input in-bound, turning "we added a check" into "the check is provably sufficient" — and to lock it against regression.
Proposed harnesses (ranked by input-hostility × harness-cheapness)
1. rcache::index_file — parsing untrusted cache-index bytes (do first)
IndexFile::from_reader (crates/rcache/src/index_file.rs:104) parses fixed 68-byte records (spec_hash(32) | flags(4) | sha256(32), WIRE_RECORD_LEN at :29) from storage the signed-index design (#86) exists because we don't trust. This same parser feeds build-servers' seal path, so one harness guards the hot format in both repos.
- Harnesses: arbitrary
&[u8]→from_readerreturnsOk/Err, never panics;merge(:146) on two small bounded indices returns the correct conflict count and preserves canonical (BTreeMap) order; round-tripfrom_reader(write_to(x)) == xon bounded indices. - Note: a fuzzer previously found a slice-math bug in this area — Kani proves the class the fuzzer sampled.
2. wire varint / LEB128 decode
decode_varint (crates/graph/src/wire.rs:146) consumes untrusted local-file-frame bytes; the four inline copies are also the audit's dedup target.
- Harnesses:
decode_varintnever panics on arbitrary bytes; the existingvarint overflowguard (:159) fires rather than wrapping (shift += 7at :156 never UB-overflows);decode_varint(encode_varint(n)) == nfor all boundedn; theMAX_VARINT_LENDoS cap (:41-54) is never exceeded. - Bonus: the dedup-into-one-function refactor this wants is the same change that makes it harnessable — one PR, both wins.
3. wire::fixup_spec / frame parse — untrusted arena reconstruction
fixup_spec (crates/graph/src/wire.rs:698) rebuilds arena indices from untrusted bytes and mutably rewrites references; the audit flagged its DanglingRef partiality (:75, :567, :685) as the most substantive in-kernel wire logic.
- Harness: arbitrary bounded frame →
from_bytesyieldsErr(DanglingRef)or a well-formed graph, never a panic and never a dangling index a later accessunwraps.
4. PathDecision::combine — the exhaustive freebie (security-relevant, no unwind bound)
combine (crates/sessions/src/core/policy.rs:739) folds per-path access decisions; its domain is a 4-variant Copy enum (Denied > Ignored > NeedsApproval > Allowed), so Kani checks the lattice laws exhaustively — no bound, no unwind caveat.
- Harnesses: commutative (
a.combine(b) == b.combine(a)), associative, idempotent, andDenied-absorbing (anyDeniedoperand ⇒Denied). Together these formally discharge the reorder-attack defense: no permutation of per-path decisions can downgrade a deny. - Strategic value: this is the exact "warm-up" target the Aeneas plan names. A Kani harness now is a zero-risk preview of the Lean proof later, with no toolchain-pinning commitment.
5. common::archive::normalize_within_root — sandbox-escape containment (highest security value)
normalize_within_root (crates/common/src/archive.rs:214) is lexical path containment.
- Harness: a bounded sequence of path components → output is
Noneor contains onlyNormalcomponents, never../root-escape, and stays lexically under root. This is the one whose failure is a real escape; worth a higher unwind bound and more care.
6. epoch-1 spec-hash codec — when it exists (forward-looking)
When the injective spec-hash redesign lands, it ships a Kani round-trip harness (decode(encode(spec)) == spec for bounded specs) from day one, and the known collision witnesses become kani::assert-refuted. Kani is the property bridge holding the injectivity claim between "shipped" and "Lean-proved". Tracked here for continuity; not part of the initial PR.
Practical setup
- Harnesses in the kernel crates behind
#[cfg(kani)];#[kani::proof]+kani::any()+#[kani::unwind(N)]where loops need bounding. - Stub
blake3— crypto in a model checker is solver death and irrelevant: every property above concerns the bytes before the digest. (-Z stubbing+#[kani::stub(...)].) - CI:
model-checking/kani-github-actionon the kernel crates only (rcache,graph,sessions,common), pinned Kani version (current is 0.67.0). Keep the harness job separate from the main test matrix so it can't block on Kani-version churn. - Bounds are documented per-harness; where a proof is bounded (not exhaustive), the bound is stated so "verified" never overclaims.
Scope of the first PR
Land the tooling + the two anchors that make the case concrete: #4 combine (exhaustive, ~20 lines, zero risk) and #1 index_file (highest value, hostile input) — plus the CI job. #2/#3/#5 follow as separate PRs; #6 rides the hash-epoch work.
Non-goals
Not a replacement for tests or fuzzing (complementary). Not applied to the effectful shell (orchestrator, sandbox2, minvmd, net, minimald) — Kani targets pure cores. Not a commitment to the Aeneas/Lean investment; this is the independently-valuable floor beneath that decision.
Activity
bryan-minimal commentedon Aug 3, 2026
Two additions surfaced by the gatehouse spec freeze (2026-08-03)
Mike published the Gatehouse auth spec + frozen known-answer vectors to
gominimal/arch(specs/authn-authz/). That makes this issue's tooling the foundation for the highest-stakes Kani application we have, and surfaces one concrete new harness target in our own tree.1. The marquee sibling application — gatehouse's parsing surface (different repo, same technique). JOSE alg-validation, SSH-cert parse, KRL parse — untrusted bytes, the CVE-density heart of any auth system (
none-alg, RS/HS confusion, jwk-smuggling). The frozen negativ 8 e v 10BC8 ectors name each failure's required error code, so they seed and cross-check Kani harnesses directly: every frozen negative becomes akani::asserton the error code, and Kani proves the class over all bounded inputs — closing the §9.1 coverage gaps (ES384, boundary encodings) the finite vector set leaves open. These harnesses live in the gatehouse impl repo and reuse this issue's exact setup (model-checking/kani-github-action,#[cfg(kani)], pinned version, stub-the-hash). Full plan ingatehouse-formal-verification.md→ Target D. Landing this issue's tooling once serves both.2. A concrete new harness target already in our code:
verify_webhook_signature(build-serverscrates/buildbot/src/github.rs:49). It parses an attacker-controlledsignature_header(sha256=<hex>from GitHub webhooks) via a hand-rolledhex_decodewhose own comment warns: "don't let a future call site turn a multi-byte char into a char-boundary panic." That is precisely a Kani property:&strsignature header →verify_webhook_signature/hex_decodenever panics (covers the char-boundary worry over all strings, not just today's ASCII caller) and the.expect("HMAC accepts any key size")never fires.index_file/ varint parsers already listed.minimal. Either fold a build-servers Kani job into this effort (the CI action is identical) or track it as a build-servers sibling issue reusing this tooling — but it's the same pattern and worth not losing.Neither changes this issue's first-PR scope (
combine+index_file+ tooling); both are the "where this goes next" once the foundation lands. The gatehouse Target-D pilot (one JOSE alg-confusion harness) is the highest-value next Kani harness in the org, and it's blocked only on this issue's tooling existing.test(kani): prove the index_file record codec and PathDecision lattice (
bryan-minimal commentedon Aug 14, 2026
PR-1 landed as #1217 (full green) — delivery vs this issue's scope
Harness set #4 (
combine): delivered beyond spec — the four laws plusAllowed-identity plus acombine == max-by-severitylemma, all exhaustive. One addition the mutation-testing review forced: the laws prove the algebra, not the wiring — deleting the symlink link-path arm of the dual check passed all proofs and the whole suite, so PR-1 also adds the missing live-fire unit test (symlink_link_denied_wins_over_allowed_target). Worth carrying that framing into the Aeneas/Lean discussion: proofs and tests cover orthogonal axes here.CI: delivered — Kani pinned exactly 0.67.0 (hard floor, not hygiene: older releases spuriously fail arrays >64 elements, and one record is 68 bytes), separate advisory lane
ci-kaniwith the house changes/aggregator pattern, promotable via ruleset edit. Direct-install-plus-cache substituted for kani-github-action (the action runs the same install uncached every time). Two integration walls solved inscripts/kani.sh: Kani's bundled toolchain is older than our MSRV floor (scratch-copy relax, documented, removable when Kani catches up), andcargo kaniexits 0 on a crate with zero harnesses — the script asserts exact harness counts so cfg-rot can't green the lane vacuously.Harness set #1 (
index_file): delivered one level below this issue's literal text, deliberately. Never-panics-at-any-truncation, the flags gate (proven to fire before consuming the sha256), and exact round-trip with pinned field offsets are all proven — at the record codec level (read_wire_kv/write_wire_kv), the layer that touches hostile bytes. The issue's literalfrom_reader/mergeharnesses are not under proof: symbolic 32-byte keys insideBTreeMapOOM CBMC (file-level first cut demonstrated this), and std's map isn't our proof obligation.from_readercomposition andmergesemantics remain covered by the existing unit tests + fuzz target; the division of labor is stated in the harness module docs. If file-level proofs are wanted later, the path is stubbing the map with a small model — its own PR."Stub blake3": turned out unnecessary — verified that no code path in the parse/merge/write layer ever invokes the compression function;
blake3::Hashis an inert 32-byte wrapper there. (One related lesson recorded in-harness: blake3's constant-timePartialEqis opaque to CBMC — compare bytes.)Remaining per this issue's sequencing: sets #2 (varint), #3 (
fixup_spec), #5 (normalize_within_root) as separate PRs; #6 rides the hash-epoch work. The unwind-bound playbook and MSRV dance carry over.test(kani): bounded verification for the index_file codec and PathDec…
fix(kani): unblock the proof build on Kani 0.68.0's std shim (#1434)
chore(kani): move to Kani 0.68.0, drop the MSRV relaxation, name comp…
docs(agents): list every workflow in the CI lane map (#1431)
norrietaylor commentedon Oct 17, 2026
Closing: done by #1217 on main.