unconstrained-witness-to-state

Specimen 65 of 96 · Other active opt-ins / Privacy and cryptographic derivations

Severity: medium
Confidence: varies
Maturity: experimental
Selection: Opt-in
Policy intent: not required
Release: v0.1.1
Engine facts used: successful-predicates private-provenance state-writes completed-entries

Selection and scope#

Not selected by default. Select it with --detectors or the detectors list in nightshade.json. Either one replaces profile selection, so list every rule you want.

Shell

./.nightshade/node_modules/.bin/nightshade ./contracts --detectors unconstrained-witness-to-state
./.nightshade/node_modules/.bin/nightshade detector show unconstrained-witness-to-state

The first command runs only this rule; --detectors takes a comma-separated list. The second prints the rule's metadata from your installed version.

Severity is review priority. It does not express exploitability or impact. Confidence is detector metadata, not a probability. All built-in rules are experimental.

Compiler scope: the engine supports the pinned profiles 0.28.0, 0.29.0, 0.30.0, 0.31.1, 0.33.0-rc.2, 0.34.0, 0.35.0-rc.1 and 0.35.0, with ZKIR2 by default. Support for this rule can be narrower; the rule documentation below states any narrower scope.

Verified example#

Synthetic examplecompact-0.34.0-zkir2compiler-validated

A witness chooses the allocation written to the ledger without a preceding bound on that value. From the proof run of the released CLI; the examples page also has the lookalike and the files.

Compactvulnerable.compactline 7 flagged

// Owned synthetic witness-to-state regression.
import CompactStandardLibrary;

export ledger allocation: Uint<64>;
witness rewardAmount(): Uint<64>;
export circuit allocate(): [] {
  const value=rewardAmount();
  allocation=disclose(value);
}

output.txtexit 1

$ nightshade vulnerable.compact --config config.json --compiler /path/to/compactc

MEDIUM — Raw witness value reaches ledger state without a value-specific assertion [unconstrained-witness-to-state]
vulnerable.compact:7:15
  7 |   const value=rewardAmount();
    |               ^
allocate writes raw output of rewardAmount into allocation on a modeled successful history without an assertion depending on that witness leaf. Disclosure permits publication; it does not validate the value. An unrelated caller guard or a witness attestation about the value supplies no circuit validation. Public registration and prover-chosen metadata can be intentional; review the required application relation.
Source: vulnerable.compact:7:15
Call path: allocate
Remediation: If this field must represent an independently established fact, enforce the required relationship in the circuit using the exact supplied value. Document intentionally prover-chosen data. Review authorization and the adequacy of the check separately.

Semantic profile: compact-0.34.0-zkir2.
Baseline analysis: complete; selected rules: complete.
Rule coverage: 1 selected rule(s); 0 with incomplete entries.
1 finding(s), 0 suppressed, 0 baseline; 1/1 entrypoint(s) completed; analysis complete. Compiler validation passed.

Corrected: Assert a bound on the witness value before writing it. Changed lines are marked.

Compactcorrected.compactrule quiet

// Owned synthetic witness-to-state regression.
import CompactStandardLibrary;

export ledger allocation: Uint<64>;
witness rewardAmount(): Uint<64>;
export circuit allocate(): [] {
  const value=rewardAmount();
  assert(value<=100,"reward allocation");
  allocation=disclose(value);
}

corrected-output.txtexit 0

$ nightshade corrected.compact --config config.json --compiler /path/to/compactc

Semantic profile: compact-0.34.0-zkir2.
Baseline analysis: complete; selected rules: complete.
Rule coverage: 1 selected rule(s); 0 with incomplete entries.
0 finding(s), 0 suppressed, 0 baseline; 1/1 entrypoint(s) completed; analysis complete. Compiler validation passed.

The command line is shortened from the recorded run to what you would type; the output below it is verbatim, with absolute file paths shortened to the example folder. Long lines wrap. A quiet result shows that this rule stopped firing, not that the contract is secure.

Corpus checks#

Synthetic corpus checks for this rule in the 0.1.1 proof run. A check counts only with compiler acceptance and complete analysis.

Positive detected	Corrected quiet	Lookalike quiet	Other negative quiet	Incomplete
1/1	1/1	1/1	0/0	0

No deviations were recorded for this rule.

These are behavior checks on synthetic fixtures, not a precision or recall estimate. See evaluation.

Rule documentation#

From docs/detectors/unconstrained-witness-to-state.md at v0.1.1.

Availability: opt-in review, medium severity, low confidence for application risk.

Description, example and scenario#

Compact

const value = rewardAmount(); // witness
allocation = disclose(value);

A raw witness leaf reaches surviving ledger state on a modeled successful history without a circuit assertion using that exact leaf. Disclosure permits publication, it does not validate the value. If a reward allocation must match an independently established fact, this is a useful review point. The SDK seed removes an owned required reward assertion; it is not an upstream vulnerability.

Recommendation#

Assert the intended application relationship using the actual written witness value, and review the adequacy of that relationship independently. An unrelated caller guard, a check on another return leaf/call, and a witness Boolean attesting about the value do not validate that value in the circuit. Document deliberately prover-chosen metadata, registration and other public input policies.

Evidence, limitations and known false positives#

Exact instruction/reference histories and cached/uncached transfers preserve witness invocation/leaf identity. Required assertion dependencies are projected through Boolean alternatives; a branch choice alone is not an assertion. Self-comparisons/private echoes supply no check. Later atomic assertions count; later definite overwrites, constructors, rejected histories, parameter-only data, transformed/hash values and explicit casts are outside this narrow review. Wildcards cannot establish definite overwrites. Findings group a witness site within an entry and list affected writes and invocations.

An assertion dependency is not proof that a relation meaningfully restricts the value, that authentication is sound or that an invariant holds. Custom constraints, implicit conversions, control-only influence and transfer-only uses are outside scope. Public registration and prover-chosen application metadata are known intent-dependent shapes: the rule remains opt-in. Exhausted or missing exact observations/projections produce rule/entry-scoped incomplete diagnostics; baseline analysis and independent-entry findings remain available.

Suppress a match#

If a match is intentional, suppress it on the line before with the exact rule ID and a reason of at least eight characters: