README.md

mkit Kani harnesses

Bounded model checking of mkit's untrusted-input decoders with Kani (pin: Kani 0.68.0, CBMC 6.11.0). The harnesses live next to the code they check, in #[cfg(kani)] mod kani_proofs blocks:

Every result below is bounded: a harness checks every input up to the stated size (every byte symbolic unless said otherwise), not every input. Nothing here is a proof for unbounded inputs; the fuzz targets (docs/FUZZ.md) and proptests cover larger inputs by sampling.

Running

cargo install --locked kani-verifier --version 0.68.0 && cargo kani setup
cd rust

# mkit-core: always --no-default-features (with the default `pack-zstd`
# feature the C zstd dependency is linked in and CBMC ran out of memory on
# most harnesses). -Z stubbing is needed by every harness that uses
# #[kani::stub] (harmless for the others).
cargo kani -p mkit-core --no-default-features -Z stubbing --harness delta_decode_no_panic

# merkle_verify_*, merkle_roundtrip_*, merkle_canary_*, pack_*: add the
# 32-byte digest/trailer comparison bound
cargo kani -p mkit-core --no-default-features -Z stubbing \
  --harness pack_entries_one_frame \
  -Z unstable-options --cbmc-args --unwindset memcmp.0:33

cargo kani -p mkit-keystore -Z stubbing --harness software_key_record_roundtrip
cargo kani -p mkit-rpc --harness rpc_read_frame_no_panic

Run one harness at a time (--harness is a substring match; every name below is unique as a substring except where noted). Peak CBMC memory was ~5.4 GB (pack_window_cursor_decode); most harnesses stay under 2 GB.

Expected-outcome convention (same as the Quint check.sh scripts): a *_canary_* harness is #[kani::should_panic] and must report VERIFICATION:- SUCCESSFUL (encountered one or more panics as expected): the checker has falsified a deliberately wrong statement, which shows the property it mirrors is checkable at that bound. Every other harness must report VERIFICATION:- SUCCESSFUL. The two harnesses marked FINDING below failed until the production code was fixed (MKIT-56, MKIT-59, 2026-09-27); both now pass. kani::cover! sites must be satisfied (Kani prints N of N cover properties satisfied); they show the asserted Ok paths are reachable.

Results (2026-09-26, macOS arm64, 15 cores, shared with other jobs)

Time is wall-clock per cargo kani invocation including the (cached) build. Cap: 15 min per harness.

mkit-core: delta (--no-default-features -Z stubbing)

mkit-core: serialize

mkit-core: merkle (BLAKE3 stubbed by a deterministic mixer)

mkit-core: pack (BLAKE3 → toy_hash, zstd decompression stubbed)

mkit-keystore (-Z stubbing; format! and from_utf8 stubbed)

mkit-rpc

Findings

1. SPEC-MERKLE-OBJECTS §5.4 builder rule vs BmtTree::range_proof. The spec now says a builder asked for position 0 of an empty Tree, "including the range 0..=0, MUST refuse rather than return the all-default proof". merkle.rs BmtTree::range_proof still has if self.empty { if start == 0 && end == 0 { return Ok(Proof::default()); } ... }, so build_tree_entries_range_proof(&Tree { entries: vec![] }, 0, 0) returns Ok(Proof { leaf_count: 0, siblings: [] }). merkle_builder_empty_tree_refuses reports this counterexample (start = 0, end = 0; the single-leaf and multi-leaf builders refuse correctly). Fixed (MKIT-56): range_proof now returns PositionOutOfRange(start) for every range of the empty tree, an intentional divergence from upstream commonware_storage::bmt (commented in the code; the commonware cross-check draws n >= 1 only). Regression test merkle::tests::empty_tree_builders_refuse_position_zero; the harness passes (2026-09-27: 0 of 4628 failed, 1/1 cover, 7.5 s).
2. SPEC-KEYSTORE §6.1.1 algorithm id 0x04 under bls-threshold. The spec says a MKITKSV1 decoder MUST reject id 0x04. algorithm_from_id maps 4 => Algorithm::Bls12381Threshold when the bls-threshold feature is on, so EncryptedKeyRecord::decode accepts such a record; rejection only happens later, in decrypt's plaintext length check. software_key_record_rejects_algorithm_4 held in the default build and failed with --features bls-threshold. Fixed (MKIT-59): §6.1.1 and §6.1.2 are explicit that shares use the separate MKITKSB1 record, so algorithm_from_id now rejects 4 in every build (no spec change). Regression test encrypted_record::tests::encrypted_record_decode_rejects_reserved_algorithm_4 (failed under bls-threshold before the fix); the harness passes in both configurations (2026-09-27: 0 of 771 failed each).

Dropped or narrowed (did not finish within 15 min)

• WindowCursor decoding with every body byte symbolic (125 B): symbolic option tags or tree depths make CBMC explore every layout after them. The harnesses fix the layout (tag and depth bytes) and keep every value symbolic. Invalid-tag and invalid-depth rejection is not covered here.
• A second layout (pack-id-bound cursor with a first-non-raw index), and the canonical re-encoding check (to_bytes(from_bytes(b)) == b): both timed out (900 s). Each from_bytes call costs ~7 min of symbolic execution (~6.8M steps), and a harness with two calls did not finish.
• PackReader::read (needs an on-disk ObjectStore), builder-side build_chunk_proof / compute_chunked_id, buffa message decoding in read_frame, non-empty keystore round-trip fields, and multi-entry trees: see the doc comments on each module. They are left to the fuzz targets and proptests.
• The §3.3 writer rule added on this branch ("a writer MUST NOT emit a 0x03/0x04 entry whose uncompressed_len would exceed MAX_RAW_OBJECT_SIZE") is enforced in maybe_compress_capped, behind the pack-zstd C compressor that Kani cannot model. It is not model-checked. append_raw_frame itself does not re-check the claim against the cap; it relies on maybe_compress.

Harness fixes in this pass

• Every stub-using harness needs -Z stubbing under Kani 0.68 (the earlier runs did not document it). Without it compilation fails with "Using the stub attribute requires activating the unstable stubbing feature".
• encrypted_record.rs: #[allow(invalid_from_utf8)] on the from_utf8 stub, which builds its error value from a known-invalid literal.