feat(detector): flag verification consuming public inputs without a field-element range check - #946
Conversation
…ield-element range check Adds `public_input_range` (SANCT_PUBLIC_INPUT_UNVALIDATED), which flags `#[contractimpl]` entrypoints that feed caller-supplied public inputs into a verification call without first checking that each one is a canonical field element strictly less than the scalar field modulus r. This is a different axis from the existing proof_length_check. That detector asks whether the right number of bytes arrived; this one asks whether those bytes denote a legal field element. A buffer can be exactly the expected length and still carry a value the verifier's soundness argument does not cover. Why it is worth an Error rather than a Warning: - Aliasing. Field arithmetic is modular, so x and x + r are the same element. When the contract's own logic reads a public input as an ordinary integer — an amount, an account id, a nullifier — while the pairing check sees it reduced mod r, the two disagree about what was proven. The proof verifies honestly for x mod r and the contract acts on x. Neither the verifier nor the circuit is broken; the gap is entirely in the unvalidated boundary between them. - Implementation-defined reduction. What a backend does with an out-of-range limb is not part of any proof system's security argument, and differs between arkworks, bellman and hand-rolled assembly. A verifier that behaves correctly today because of which crate it links is relying on undefined behaviour, and a dependency bump changes the answer. Detection, and the false-positive story: Public-input parameters are matched by name (public_input(s), pub_input(s), public_signal(s), pub_signals, inputs, instance(s)) — deliberately not bare `proof`, since a proof is not a public input and flagging it here would duplicate proof_length_check on a different axis. A finding is raised only when such a parameter reaches a call containing verify, pairing or check_proof. Three validation forms silence it, each because it actually establishes the property: a comparison against a modulus-like constant in either direction (matched by rendering the expression and scanning for modulus / field_order / scalar_field / group_order / fr_modulus / bls12_381_r and friends, so MODULUS, crate::consts::FR_MODULUS and Fr::MODULUS all work); a checked deserializer that returns Option/Result on a non-canonical encoding; or a dedicated validation helper. `*_unchecked` constructors are explicitly not treated as validation even when the name contains "canonical" — from_canonical_bytes_unchecked is still flagged, since that naming is exactly where this bug hides. There is a test pinning that. Entrypoints that take public inputs but never verify are not flagged: a setter makes no soundness claim. Neither are `#[cfg(test)]` modules, and inline `sanctifier:ignore[SANCT_PUBLIC_INPUT_UNVALIDATED]` is honoured, matching the conventions of the surrounding rules. Documentation: docs/detectors/public_input_range.md covers the aliasing mechanism, the vulnerable shape, all three accepted fixes, and references to the 0xPARC ZK Bug Tracker, ZKSecurity's common-vulnerabilities writeup, Trail of Bits, and arkworks' from_bigint contract. Rows added to the detector catalog and the finding-code table; the docs-coverage test enforces both. Tests: 8 unit tests covering the flagged shape, each accepted validation form, the unchecked-constructor case, the no-verify and no-public-input cases, and suppression. Note for reviewers: two pre-existing failures in `memory::tests` reproduce on an unmodified checkout of main on macOS (memory sampling) and are unrelated to this change.
c3a85ca to
cac7fcc
Compare
|
Force-pushed a fix for the failing CI.
"public_input_range": "SANCT_PUBLIC_INPUT_UNVALIDATED",
"SANCT_PUBLIC_INPUT_UNVALIDATED": "SANCT_PUBLIC_INPUT_UNVALIDATED"All 13 test targets pass locally now, including The corpus entry is anchored next to The workflow runs on the new commits are sitting at |
Closes #628
Summary
Adds
public_input_range(SANCT_PUBLIC_INPUT_UNVALIDATED): flags#[contractimpl]entrypoints that feed caller-supplied public inputs into a verification call without first checking that each one is a canonical field element strictly less than the scalar field modulusr.This is a different axis from the existing
proof_length_check. That detector asks whether the right number of bytes arrived; this one asks whether those bytes denote a legal field element. A buffer can be exactly the expected length and still carry a value the verifier's soundness argument does not cover.Why this is an Error, not a Warning
Aliasing. Field arithmetic is modular, so
xandx + rare the same element. When the contract's own logic reads a public input as an ordinary integer — an amount, an account id, a nullifier — while the pairing check sees it reduced modr, the two disagree about what was proven. The proof verifies honestly forx mod r; the contract acts onx. Neither the verifier nor the circuit is broken. The gap is entirely in the unvalidated boundary between them, which is why this survives an audit of either component alone.Implementation-defined reduction. What a backend does with an out-of-range limb is not part of any proof system's security argument, and differs between arkworks, bellman and hand-rolled assembly. A verifier that behaves correctly today because of which crate it happens to link is relying on undefined behaviour, and a dependency bump changes the answer.
Non-canonical encodings are the same problem in encoding space: two byte strings decoding to one element let an attacker produce a second, distinct-looking submission for a nullifier meant to be spent once.
Detection, and the false-positive story
Public-input parameters are matched by name (
public_input(s),pub_input(s),public_signal(s),pub_signals,inputs,instance(s)) — deliberately not bareproof, since a proof is not a public input and flagging it here would duplicateproof_length_check. A finding is raised only when such a parameter reaches a call containingverify,pairingorcheck_proof.Three validation forms silence it, each because it genuinely establishes the property:
modulus/field_order/scalar_field/group_order/fr_modulus/bls12_381_retc., soMODULUS,crate::consts::FR_MODULUSandFr::MODULUSall work without pattern-matching every shape a constant reference can takefrom_canonical_bytes,from_repr,deserialize_compressed, … — the ones that returnOption/Resulton a non-canonical encodingvalidate_public_inputs,is_in_field, anything matching*canonical*or*range*check**_uncheckedconstructors are explicitly not treated as validation even when the name contains "canonical" —from_canonical_bytes_uncheckedis still flagged, because that naming is exactly where this bug hides. There is a test pinning that behaviour.Not flagged: entrypoints that take public inputs but never verify (a setter makes no soundness claim); verification with no public-input parameter;
#[cfg(test)]modules; lines carrying// sanctifier:ignore[SANCT_PUBLIC_INPUT_UNVALIDATED]. All conventions match the surrounding rules.Documentation
docs/detectors/public_input_range.mdcovers the aliasing mechanism, the vulnerable shape, all three accepted fixes, and references to the 0xPARC ZK Bug Tracker, ZKSecurity's common-vulnerabilities writeup, Trail of Bits, and arkworks'from_bigintcontract. Rows added to the detector catalog and the finding-code table —tests/detector_docs_coverage.rsenforces both.Acceptance criteria
Tests
8 unit tests.
cargo fmt --all -- --checkclean,cargo clippy -p sanctifier-core --all-targetsclean,cargo test -p sanctifier-corepassing.Pre-existing failures, unrelated to this PR:
memory::tests::memory_guard_rejects_above_zero_limitandmemory::tests::memory_tracker_samples_increase_peakfail on an unmodified checkout ofmainon macOS (memory sampling). Verified by stashing this change and re-running — same two failures. Worth a separate issue if they are not already known.Local runs used
--no-default-featuresbecause the defaultsmtfeature needsz3.hpresent; that is a local toolchain gap, not a change here.Conflicts
This and #629's PR share four files by necessity — the detector registry (
rules/mod.rs),finding_codes.rs, and the two docs tables. Rather than both appending to the same place, each PR's insertions are anchored far apart in every shared file: this one registers aftervk_provenanceand inserts nearPROOF_LENGTH_UNVALIDATED; the other registers afteredge_amountand inserts nearBALANCE_EQUALITY, tens of lines away in each case, so no two hunks share context.Both merge orders were tested locally against
main— clean either way, with fmt, clippy, the docs-coverage test and 294 passing tests on the combined result.