o1js-scan

A fast, dependency-free static analyzer for zk circuit soundness bugs in:

• o1js / Mina zkApps (TypeScript .ts / .js) — Kimchi circuits from @method bodies
• Noir (.nr) — Aztec's Rust-like ZK DSL (including aztec-nr-shaped patterns)

The security-critical bugs usually aren't in the proving system — they're in the application's own constraints: witnesses the prover controls but the circuit never binds. o1js-scan is the under-constrained-signal scanner for Circom's cousins in the Mina and Noir ecosystems.

pip install o1js-scan
o1js-scan path/to/zkapp          # o1js + Noir (auto)
noir-scan path/to/circuits       # same binary — Noir-friendly alias
noir-scan . --lang noir --fail-on high --sarif noir.sarif

Example

Given a vault whose withdraw amount is a prover-controlled witness that is never bound to on-chain state:

$ o1js-scan examples/vulnerable_vault.ts
HIGH     O1JS_UNCONSTRAINED_WITNESS         vulnerable_vault.ts:23  fn=withdraw  Unconstrained witness `amount` flows to send_amount in `withdraw`
LOW      O1JS_UNCONSTRAINED_RECIPIENT       vulnerable_vault.ts:23  fn=withdraw  Recipient `to` is prover-chosen in `withdraw`
o1js-scan: 2 finding(s) [1 high, 1 low] in 1 file(s) — fails (--fail-on high)
$ echo $?
1

The HIGH finding is the drainable bug; the fixed contract (examples/safe_vault.ts) scans clean and exits 0. See examples/ for the o1js and Noir vulnerable/fixed pairs.

Contents

• Install
• Usage · Suppressing a finding
• GitHub Action
• What it detects — o1js · Noir
• Known limitations
• Compatibility · How it works
• Contributing

Install

pip install o1js-scan

Or from source:

git clone https://github.com/auditinfra-io/o1js-scan
cd o1js-scan
pip install -e .

No third-party dependencies. Python 3.8+. The noir-scan console script is installed alongside o1js-scan (same entry point).

Usage

# scan a directory (recursively; skips node_modules, target/, .git, …)
o1js-scan path/to/project

# Noir-only / o1js-only
noir-scan circuits --lang noir
o1js-scan src --lang o1js

# scan a single file
o1js-scan src/MyContract.ts
noir-scan src/main.nr

# machine-readable output for CI
o1js-scan src --json

# SARIF 2.1.0 for GitHub code scanning (writes o1js-scan.sarif by default)
o1js-scan src --sarif
noir-scan . --lang noir --sarif noir.sarif

# choose which severity fails CI (critical|high|medium|low|none; default high)
o1js-scan src --fail-on medium

# Noir test code is excluded by default; opt back in
noir-scan circuits --lang noir --include-tests

o1js-scan --version

Exit code is 1 when a finding at or above the --fail-on level (default high) is present and 0 otherwise — so you can drop it straight into CI. With the default, a low/medium finding (including the informational recipient rule below) does not fail the build; use --fail-on none to only report, or --fail-on medium to gate more strictly. A missing scan path exits 2 with an error on stderr, so a typo can't silently pass CI as a clean run. Every run prints a one-line summary (counts by severity and the gate verdict) to stderr.

Noir test code is excluded by default. Noir tests deliberately build invalid values inside unsafe blocks to prove the surrounding asserts reject them, so findings there are noise rather than circuit bugs. A file is treated as test code when its name is *_test.nr / test_*.nr, it sits under a test/ or tests/ directory, the function carries a #[test] / #[test(...)] attribute, or it is inside a mod test { … } / mod tests { … } block (block-scoped, so a test module at the bottom of a production file does not silence the rest of it). Pass --include-tests to report them.

Directories skipped when walking a tree: node_modules, target (nargo), .git, dist, build, __pycache__, .venv, venv.

Suppressing a reviewed finding

Silence a finding you've triaged without loosening the gate, with an inline comment on — or on the line above — the flagged line:

this.send({ to, amount });  // o1js-scan-disable-line O1JS_UNCONSTRAINED_WITNESS

// o1js-scan-disable-next-line
this.send({ to, amount });

let inv = unsafe { hint(x) };  // o1js-scan-disable-line NOIR_UNCONSTRAINED_WITNESS

List one or more rule ids to suppress only those; a bare directive (no ids) suppresses every rule on the target line.

As a library:

from o1js_scan import analyze_file, analyze_project

for path, finding in analyze_project("src", lang="auto"):
    print(path, finding.rule_id, finding.severity.value, finding.title)

GitHub Action

Add the scanner to CI in a few lines. Findings appear as annotations on the PR diff and as alerts in the repository's Security → Code scanning tab.

# .github/workflows/o1js-scan.yml
name: o1js-scan
on: [push, pull_request]

permissions:
  contents: read
  security-events: write   # required to upload SARIF to code scanning

jobs:
  scan:
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v4
      - uses: auditinfra-io/o1js-scan@v0.9.0
        with:
          path: src              # optional, defaults to the repo root
          lang: auto             # auto | o1js | noir
          # version: 0.9.0       # optional, pin the scanner version
          # fail-on-findings: true   # optional, fail the job on any high/critical

Noir-only CI recipe

- uses: auditinfra-io/o1js-scan@v0.9.0
  with:
    path: .
    lang: noir
    fail-on-findings: true

Or without the Action:

pip install o1js-scan
noir-scan . --lang noir --fail-on high --sarif noir.sarif

pre-commit (optional)

# .pre-commit-config.yaml
- repo: local
  hooks:
    - id: noir-scan
      name: noir-scan
      entry: noir-scan
      language: system
      pass_filenames: false
      args: [".", "--lang", "noir", "--fail-on", "high"]

Inputs: path (default .), lang (auto|o1js|noir, default auto), version (PyPI version to install, default latest), upload-sarif (default true), fail-on-findings (default false). SARIF upload needs security-events: write and code scanning enabled.

What it detects (o1js)

False-positive guards (o1js)

The analyzer is designed to stay quiet on correct code:

• Signature-gated methods are skipped. A @method that calls this.requireSignature() (or getAndRequireSignature, AccountUpdate.createSigned, Signature.verify) is owner/admin-gated — its arguments are chosen by the key holder, not an arbitrary prover — so its witnesses are not flagged. This is the o1js equivalent of onlyOwner.
• State-bound witnesses are skipped. An argument asserted equal to (or bounded by an ordering comparison against) a getAndRequireEquals()-derived value is sound and won't be reported. This covers both the direct form — amount.assertLessThanOrEqual(bal) — and the chained form amount.lessThanOrEqual(bal).assertTrue(). Binding that lives in an undecorated same-class helper (this.verifyX(arg)) is also recognized (depth 1 only).
• Verified proofs are skipped. A Proof / SelfProof / DynamicProof / *Proof-typed argument on which .verify() / .verifyIf() is called is constrained by the verified circuit — witness findings on it (and its publicOutput / publicInput) are suppressed. The same applies to the canonical OffchainState wrapper this.offchainState.settle(proof) (the framework verifies inside settle). A hand-rolled .settle(proof) is not assumed to verify. The inverse case (proof-typed arg never verified and not OffchainState-settled) is reported as O1JS_UNVERIFIED_PROOF.
• Asserted / used Bools are skipped. A predicate chained with .assertTrue() / .assertFalse(), nested in Provable.if(...), or assigned to a local that is later referenced, is not reported as O1JS_UNASSERTED_BOOL.
• Authenticated senders are skipped. this.sender.getUnconstrained() does not fire when the same @method also calls this.sender.getAndRequireSignature(), or when that witnessed value is passed to AccountUpdate.createSigned(...) / authenticated via .requireSignature() on an AccountUpdate built from it (argument identity required).
• Comments and string literals are stripped before analysis, so an assert inside a string can't create a false result.

What it detects (Noir)

The same soundness idea — under-constrained witnesses — applies to Noir (.nr) circuits. Point the scanner at .nr files (or use --lang noir) and it analyzes them with the Noir rule set. Same lexical, dependency-free approach. Calibrated against aztec-nr oracle / unsafe idioms — see docs/noir_calibration.md.

False-positive guards (Noir)

• Assert / let-hop / same-file confirm helpers bind unsafe hints.
• Call-site names constrain_* / confirm_* / verify_* / check_(non_)membership* / public_data_storage_read credit args (with unused-result detection for discarded checks).
• Documented intentional unconstrained (requires adjacent // Safety:): random(), avm::…, and kernel/rollup/discovery deferred wording.
• Tuple let + asserted flags bind merkle witnesses passed into membership checks.

Example:

noir-scan examples/noir_unconstrained.nr   # HIGH NOIR_UNCONSTRAINED_WITNESS
noir-scan examples/noir_constrained.nr     # clean

Known limitations

The analyzer is a lexical, name-matching pass, not a dataflow engine. Keep these blind spots in mind when triaging — they are known and intentional for this dependency-free design, not bugs:

• Aliasing defeats the taint. Witness tracking matches argument names, so copying a witness through a local hides it:

  const q = qty; this.send({ to: dest, amount: q });   // qty is not flagged
  const slot = this.root; slot.get();                  // missing precondition missed
  

• Cross-method binding is depth-1 only. An undecorated same-class helper called as this.verifyX(arg) can state-bind a caller's argument (one level). Deeper chains (@method → helper A → helper B) and free/imported functions are not followed. Local-variable aliasing of the helper argument also stays a documented limitation.

• Unasserted-Bool detection is statement-shaped. Tier A only flags bare expression statements whose outermost call is a Bool predicate with nothing chained after it. Predicates nested inside Provable.if(...), or assigned and later used, are not flagged. Complex control-flow uses of a Bool local may still be missed if the name is never referenced (failure mode: miss, not a false positive).

• Signature-gating is method-level and substring-based. _method_is_signature_gated treats a whole @method as owner-gated if it contains a signature idiom, and it recognizes a verifier only when the receiver name literally contains signature — so sig.verify(admin, msg) is not recognized as gating, while an unrelated signature check elsewhere in a large method can over-suppress. It is all-or-nothing per method.

• Sender authentication is name-based and same-method only. O1JS_UNCONSTRAINED_SENDER suppresses when this.sender.getAndRequireSignature() or AccountUpdate.createSigned(<that sender>) appears in the same @method body. A signature requirement that lives only in a helper (this.requireSenderSig() → getAndRequireSignature inside) is not followed — failure mode is a false positive on correct code that wraps the idiom, not a missed real bug.

• Noir cross-crate helpers are recognized by name convention only (no Nargo.toml / import resolution). Prefer miss over false positive.

These are the reason findings are a starting point for human review, not proofs. A dataflow-aware rewrite is deliberately out of scope for the lexical analyzer.

Compatibility

Works on o1js 1.x and 2.x. o1js-scan analyzes TypeScript source as text and has no runtime dependency on o1js — nothing is version-pinned. It keys on the modern require* precondition API (getAndRequireEquals, requireEquals, requireSignature, getAndRequireSignature), the @method / @method.returns(...) decorators, @state, this.send({...}), and Permissions.*, all of which are unchanged across the 1.x → 2.x boundary. The 2.x owner-auth idiom this.sender.getAndRequireSignature() is recognized as signature-gating. (Legacy assertEquals preconditions are still accepted, so older code isn't broken either.)

Noir analysis targets Noir syntax used by Aztec / nargo projects (.nr); it does not invoke nargo or compile circuits.

How it works

It's a lexical analyzer, not a full TypeScript or Noir parser — o1js and Noir sources are brace-delimited and regex-tractable, and the output is meant to be triaged by a human. That keeps it dependency-free and instant to run in CI. Findings are a starting point for review, not proofs.

Roadmap / contributing

Contributions welcome — new rule families, more FP guards, and real-world calibration archetypes are all valuable. See CONTRIBUTING.md. Run the tests and linter with:

pip install -e ".[dev]"
pytest          # 154 tests
ruff check .    # lint

License

Apache-2.0. See LICENSE.