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

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

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.

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.7.1
        with:
          path: src              # optional, defaults to the repo root
          lang: auto             # auto | o1js | noir
          # version: 0.7.1       # 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.7.1
  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 suite with:

pip install -e ".[dev]"
pytest

License

Apache-2.0. See LICENSE.