Automated security audit

Three checks run against every pull request and again nightly, wired up in .github/workflows/security-audit.yml. They cover three different kinds of claim, and it is worth being precise about which is which, because the three are not interchangeable.

Surface	Tool	Claim	Strength
Decoders	cargo-fuzz / libFuzzer	no panic, no over-allocation, canonical encodings	evidence, not proof
Ledger arithmetic	Kani	u64 credits, debits and nonce bumps cannot wrap	proof (see caveat)
Unsafe code	cargo-geiger + scripts/check-unsafe.sh	first-party unsafe is justified; dependency unsafe is visible	survey plus a gate

---

1. Fuzzing the decoders

Everything under fuzz/fuzz_targets/ drives one entry point that reads bytes the node did not produce.

Target	Entry point
tx_decode	Transaction::from_bytes
header_decode	BlockHeader::from_bytes
block_decode	Block::from_bytes
payload_decode	TxKind::decode
account_decode	Account::decode
sv2_frame_decode	maya_stratum_v2::frame
car_decode	maya_archive::read_car

Each asserts two properties. The first is the obvious one: a malformed frame must surface as NodeError::Decode and never as a panic — ByteReader range-checks every access precisely so a hostile peer cannot turn a bad frame into an aborted node.

The second is canonicality, and it is the one worth spelling out. ByteReader::finish rejects trailing bytes, and every field in the wire format is either fixed-width or length-prefixed. Together those mean each accepted frame must re-encode to itself. If two distinct byte strings decoded to one transaction, that transaction would have two txids — and a transaction with two identities is a double-spend the nonce check cannot see. The targets assert the round-trip rather than trusting the argument.

What the targets deliberately never call

Transaction::verify, BlockHeader::pow_hash and BlockHeader::pow_hash_at. Hybrid signature verification is ~105 ms and ArgonBlake is a 32 MiB Argon2id pass measured in seconds. The DAG rule that replaces ArgonBlake above the fork is cheaper — ~2.0 ms per verification, measured — but its first call for an epoch generates a 64 MiB cache, which a fuzzer would pay for repeatedly. Any of them would cap the fuzzer somewhere around ten executions per second, which does not find bugs — it just makes the job look like it ran. None is a decode concern; all are covered by crates/node/tests/hybrid_tests.rs, crates/node/tests/malleability_tests.rs, crates/node/tests/consensus_tests.rs and crates/node/tests/dag_tests.rs.

The consensus vectors job

crates/node/tests/fixtures/dag_vectors.json pins the bytes of the DAG proof of work, and the consensus-vectors job checks both implementations of it — the node’s and the GPU miner’s — against that file on every push. It is in this workflow rather than a general test run because what it defends against is the same class of thing the rest of this file is about: a change that compiles, passes its own tests, and silently forks the chain.

Budget

A pull request gets 60 seconds per target against the committed corpus: enough to catch a regression on a path the corpus already reaches. The nightly scheduled run gets 900 seconds per target, which is where genuinely new inputs come from.

Corpus

Seeds are generated by the real encoders, never hand-written:

cargo run --example gen_fuzz_corpus

A hand-rolled seed is a second, undocumented copy of the wire format; when a field moves it stops decoding, and the fuzzer keeps running against a corpus that silently no longer reaches the code it was written for. Generating them means a format change either updates the corpus or fails to compile.

Seeds sit near the boundaries on purpose — u64::MAX output amounts, a joinsplit one mutation away from wrapping public_out + fee, a SettleBatch at the CLOSURE_SIZE accounting edge.

Windows: cargo fuzz does not support x86_64-pc-windows-msvc. Run the targets under WSL or leave them to CI; corpus generation works everywhere. See fuzz/README.md.

---

2. Proving the ledger arithmetic

crates/ledger-math/ holds every u64 credit, debit and nonce bump the chain performs, and crates/ledger-math/src/proofs.rs model-checks them with Kani.

cargo kani -p maya-ledger-math

Kani runs on Linux and macOS only — it needs CBMC, which has no Windows build. Together with cargo fuzz’s lack of MSVC support, that means neither the proofs nor the fuzzing can run on a Windows workstation: CI is where both execute, and a Windows developer’s local loop is cargo test and cargo clippy. The unit tests in crates/ledger-math/src/lib.rs cover the same functions by example and do run everywhere, which is what keeps a Windows developer from being blind to a break between pushes.

Why it is a separate crate

Kani compiles a crate together with its entire dependency graph into a CBMC goto-binary. custom-l1-node depends on rocksdb — which is C++ through librocksdb-sys — plus libp2p, fips204, and the ark-* SNARK stack. Kani has no semantics for the C++. cargo kani -p custom-l1-node is not slow; it is not possible.

A dependency-free leaf crate is. StateDB::stage_transaction, ShieldedPool::settle, Settlement::credit and ChannelClosure::total all call into maya-ledger-math rather than inlining their own checked_add, so what the proofs establish is a property of the code that runs when a block is applied — not of a restatement of it that could drift.

Its [dependencies] table is empty and must stay that way. A dependency added there is a dependency added to every proof.

What is proved

Most harnesses check the operation against a wider-type oracle: the same arithmetic in u128, where no u64 ledger quantity can overflow. That pins down what the answer must be, not merely what it must not be — a checked_add silently replaced by a saturating_add still never wraps, and fails the oracle immediately.

Harness	Establishes
credit_agrees_with_wide_addition	exact sum, or None precisely at the ceiling
debit_agrees_with_wide_subtraction	exact difference; a debit never leaves the account richer
debit_then_credit_is_the_identity	the two directions agree
debit_is_strict_unless_zero	a non-zero debit strictly reduces
advance_nonce_steps_by_one	steps by one, stops only at u64::MAX
combined_balance_agrees_with_wide_addition	a channel closure’s claimed total cannot wrap past the capacity check
total_outputs_agrees_with_wide_summation	the fold matches exact u128 summation
total_outputs_of_nothing_is_zero	the empty transaction moves nothing
a_two_output_transfer_conserves_value	debit + two credits conserve total held
settle_pool_agrees_with_wide_arithmetic	all three shielded-pool outcomes are exact
settle_pool_moves_value_in_the_stated_direction	deposits never shrink the pool, withdrawals never grow it

The caveat, stated plainly

Every scalar harness is unbounded: it quantifies over all u64 inputs, with no loop and no unwind bound. There is no input those functions have not been checked on.

total_outputs_agrees_with_wide_summation is bounded. It folds over a sequence, so it carries #[kani::unwind(5)] and is proved for up to four outputs — while ByteReader::read_collection_len will accept 65,536. The gap is real. What justifies it is that the fold is uniform: each step is one checked_add on the running total, proved for all u64, and the induction from step n to step n + 1 introduces no new case. The honest summary is that the step is proved and the fold is proved to depth four.

a_two_output_transfer_conserves_value is likewise a two-output model with three distinct accounts. A self-transfer reads through the block overlay and so sees its own debit — a claim about the overlay rather than about arithmetic, and covered by crates/node/tests/state_tests.rs.

---

3. Unsafe accounting

Two things run here, and they do different jobs.

cargo-geiger — a survey, reported not gated

cargo geiger --workspace --all-features counts unsafe expressions across the whole dependency graph and writes the result into the job summary.

It is not a gate, on purpose. We do not control what the RocksDB bindings, libp2p, or the arkworks stack do, so any threshold over that number would be chosen to make the build pass rather than to mean something. What the survey is good for is showing a reviewer what a version bump changed.

cargo-geiger is also lightly maintained and has a history of breaking on new cargo metadata formats, so its step is continue-on-error. That covers the tool, not the finding: when geiger falls over, the job says so and the gate below still runs.

scripts/check-unsafe.sh — the gate

Fails the build if any unsafe block or unsafe impl in first-party code lacks a // SAFETY: comment in the five lines above it. No dependencies beyond grep and awk, so it cannot break for tooling reasons.

A comment rather than a baseline count, because a count rots: it drifts whenever an unrelated line moves, and it says nothing about whether the unsafe that exists is justified. The SAFETY rule is the one CLAUDE.md already states, and it stays true as the code changes.

unsafe fn, unsafe extern and #[unsafe(...)] are not gated. They declare a proof obligation rather than discharge one — the caller is who has to justify anything — so demanding a note on the declaration would only train people to write one that says nothing.

contracts/ is not scanned. Those build for wasm32 against a host ABI, outside this workspace and on their own toolchain, and their unsafe is host-import plumbing with a different review story. The script counts and prints them so the omission is visible rather than silent.

cargo-deny

deny.toml checks advisories, bans and sources. Licence checking is off: it is a compliance question, and enabling it would let a licence reclassification turn the security audit red.

There is no ignore list under [advisories], and the empty list is the point — an advisory that has to be accepted should be accepted in a commit that says why.

cargo-audit disagrees, and that is expected

cargo audit reads Cargo.lock, so it reports advisories for packages the build never compiles — today, hickory-proto and lru, which libp2p declares under a dns feature this workspace does not enable. cargo deny resolves the graph and reports advisories ok.

Neither is silenced. deny.toml keeps ignore = [] on purpose, and no .cargo/audit.toml exists either: the discrepancy is written down instead, with the empirical check behind it, in launch-checklist.md. The upstream fix is hickory >= 0.26.1, which needs libp2p 0.57 — a bump across the transport and the ML-KEM wrapper, and so a deliberate change rather than an audit side effect.

---

Running it all locally

cargo test --workspace                       # the existing suite
cargo clippy --workspace --all-targets       # lints
cargo kani -p maya-ledger-math               # proofs
cargo run --example gen_fuzz_corpus          # regenerate seeds
./scripts/check-unsafe.sh                    # the unsafe gate
(cd fuzz && cargo fuzz run tx_decode)        # fuzzing — Linux/macOS only

When a fuzz target crashes

1. Minimize: cargo fuzz tmin <target> fuzz/artifacts/<target>/<crash>.
2. Fix the decoder.
3. Add the minimized input as a regression case in the matching crates/node/tests/*_tests.rs.
4. Commit the minimized input to fuzz/corpus/<target>/ so the path stays warm.

The regression test lands with the fix, in one commit. Committing a reproducer ahead of the fix puts a failing test on the branch.