o1js-scan

A fast, dependency-free static analyzer for o1js / Mina zkApp soundness bugs.

o1js zkApps compile TypeScript @method bodies into Kimchi circuits. Just like Circom circuits, the security-critical bugs usually aren't in the proving system (that's upstream o1Labs infrastructure) — they're in the application's own constraints: witnesses the prover controls but the contract never binds, state reads that never assert a precondition, and account permissions that let a signature bypass the proof logic entirely.

o1js-scan finds those. It's the o1js analog of under-constrained-signal scanning for Circom.

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+.

Usage

# scan a directory (recursively; skips node_modules)
o1js-scan path/to/zkapp/src

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

# 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
o1js-scan src --sarif report.sarif   # or a named file, or - for stdout

# 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.

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 });

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"):
    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.5.0
        with:
          path: src              # optional, defaults to the repo root
          # version: 0.5.0       # optional, pin the scanner version
          # fail-on-findings: true   # optional, fail the job on any high/critical

Inputs: path (default .), version (PyPI version to install, default latest), upload-sarif (default true), fail-on-findings (default false — by default the scan reports as alerts without failing the build). SARIF upload needs security-events: write and code scanning enabled (on by default for public repos; private repos need GitHub Advanced Security). To gate the build instead of (or in addition to) uploading alerts, set fail-on-findings: true.

What it detects

False-positive guards

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.

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.

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.)

How it works

It's a lexical analyzer, not a full TypeScript parser — o1js code is decorator + brace-delimited-method-body shaped 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. Please add a test to tests/ for any new rule or guard. Run the suite with:

pip install -e ".[dev]"
pytest

License

Apache-2.0. See LICENSE.