Nullsec S1-ZK

Deterministic, graph-aware static analysis for zero-knowledge circuits.

Nullsec S1-ZK is an open-source security engine for zero-knowledge circuits.

It analyzes Circom and Halo2 circuits, builds constraint graphs, infers proof obligations, and generates exploit hypotheses for underconstraint risks.

S1-ZK is fully local and deterministic. It sends no code to external services. LLM-assisted reasoning is planned, but not required by the current engine.

Find underconstraints before they mint infinite money.

npx @trynullsec/s1-zk scan ./circuits

Why S1-ZK Exists

Catastrophic ZK bugs are often not ordinary application bugs. They are proof-system semantic failures: a witness can satisfy the constraint system while violating the protocol statement developers believe is being proven.

Nullsec S1-ZK is built around one question:

What does this circuit claim to prove, and what does it actually constrain?

The tool is designed for ZK auditors, protocol engineers, security researchers, and crypto developers who need fast, deterministic signal on underconstraints, unsafe witness assignments, missing public bindings, selector mistakes, incomplete EC relations, and other soundness risks.

Supported Frontends

Frontend	Status	Notes
Circom	Full	Tokenizer, parser, constraint graph, rule coverage
Halo2-style Rust	Heuristic	Pattern/dataflow based; no full Rust AST yet
Noir	Planned	Adapter stub only
gnark	Planned	Adapter stub only

Circom

The Circom frontend parses .circom files and builds a signal/constraint graph for high-signal soundness checks:

• Dangerous hint assignments with <--
• Assigned-but-unconstrained signals
• Unbound inputs
• Unconstrained outputs
• Missing booleanity checks
• Missing range checks
• Unsafe assertions
• Unsafe division or inverse patterns
• Alias and overflow risks
• Suspicious selectors

Halo2-Style Rust

The Halo2 frontend scans Rust source for Halo2 patterns and builds a best-effort constraint graph over gates, regions, selectors, equality edges, and public bindings:

• Assigned advice not constrained
• Instance value not bound
• Selector discipline risk
• Unsafe inverse/division
• Partial EC operation risk
• Missing enable_equality assumptions
• Gate extraction
• Assignment connectivity
• Equality/copy edges
• Public instance bindings

Deep Analysis Mode

--deep enables relationship-aware analysis beyond individual rule hits:

• Proof obligation extraction
• Relation checking
• Taint/witness flow analysis
• Exploit hypothesis generation

npx @trynullsec/s1-zk scan ./circuits --deep

Example deep-analysis output:

Proof obligations:
Total      68
Satisfied  59
Missing    9

Exploit hypothesis:
A malicious prover may choose EC point coordinates independently of the claimed scalar multiplication relation. If the verifier accepts those values as part of the EC output, the circuit may verify an invalid group operation.

Deep mode is still static analysis. It infers likely proof obligations from naming, graph relationships, and source structure, then checks whether parsed constraints appear to support those obligations.

Installation

Run without installing:

npx @trynullsec/s1-zk scan ./circuits

Install globally:

npm install -g @trynullsec/s1-zk

Usage

nullsec-zk scan ./circuits
nullsec-zk scan ./circuits --deep
nullsec-zk scan ./circuits --format json
nullsec-zk scan ./circuits --report markdown
nullsec-zk scan ./circuits --deep --no-banner
nullsec-zk rules
nullsec-zk explain NS-H2-005
nullsec-zk init

Use --no-banner for machine-readable logs or minimal terminal output:

nullsec-zk scan ./circuits --deep --no-banner

The same commands work through npx:

npx @trynullsec/s1-zk scan ./circuits --deep
npx @trynullsec/s1-zk rules
npx @trynullsec/s1-zk explain NS-H2-005

Example Output

Nullsec S1-ZK
AI-native auditing for zero-knowledge circuits

Target: ./examples
Frontend: Mixed
Files scanned: 24
Rules executed: 18
Issues found: 34

Severity summary:
CRITICAL  2
HIGH      20
MEDIUM    8
LOW       3
INFO      1

Proof obligations:
Total      68
Satisfied  59
Partial    0
Missing    9
Unknown    0

Rule Coverage

Rules are documented in RULES.md. The current rule families include:

• NS-ZK-* rules for Circom underconstraints, unsafe hints, missing booleanity/range checks, unsafe assertions, component-output binding, and selector risks.
• NS-H2-* rules for Halo2 advice connectivity, public instance binding, selector discipline, inverse safety, EC operation completeness, and equality assumptions.

List rules locally:

nullsec-zk rules

Explain a rule:

nullsec-zk explain NS-H2-005

Orchard-Class Demo

This repository includes a synthetic Halo2 benchmark inspired by the public Zcash Orchard vulnerability disclosure. The benchmark does not contain Zcash source code and does not claim to reproduce the original exploit. It models the same family of risk: an elliptic-curve multiplication relation where assigned EC values are not fully bound into the constraint system.

The demo lives under:

benchmarks/historical/orchard-inspired

Run:

npx @trynullsec/s1-zk scan ./benchmarks/historical/orchard-inspired --deep

Expected: S1-ZK flags the vulnerable synthetic gadget, identifies unconnected EC values, infers a partial EC multiplication proof obligation, and generates an exploit hypothesis.

Benchmark

Run the bundled regression corpus:

npm run benchmark

Current output:

vuln=14 safe=10 TP=13 FN=1 TN=10 FP=0
precision=100.00% recall=92.86% false_safe_rate=7.14% false_positive_rate=0.00%
MISSED: examples/halo2/vulnerable/missing-selector-booleanity.rs

Metric	Value
False-safe rate	7.14%
False-positive rate	0.00%
Precision	100.00%
Recall	92.86%

Bundled corpus size is small and intentionally synthetic. These numbers are regression signals for this repository, not a general claim about all ZK circuits.

Known miss: examples/halo2/vulnerable/missing-selector-booleanity.rs. Selector-booleanity detection for this fixture is not yet covered by NS-H2-003.

Reports

Nullsec S1-ZK supports:

• Terminal output
• JSON output
• Markdown reports
• SARIF for code-scanning workflows

Examples:

nullsec-zk scan ./circuits --format json
nullsec-zk scan ./circuits --report markdown
nullsec-zk scan ./circuits --format sarif --out nullsec-zk.sarif

Configuration

Create a config file:

nullsec-zk init

Example .nullsec-zk.json:

{
  "rules": {
    "NS-ZK-006": "off"
  },
  "ignore": ["node_modules", "target"],
  "failOn": "HIGH"
}

Limitations

Nullsec S1-ZK is a static analysis tool:

• Parsing is best-effort.
• It is not formal verification.
• It does not prove full circuit soundness.
• It does not replace expert ZK or cryptographic audits.
• Macro-heavy Rust/Halo2 code can be missed.
• Deep analysis infers likely proof obligations and can be wrong.

See LIMITATIONS.md for more detail.

Roadmap

• Real Rust AST parsing via syn
• Noir frontend
• gnark frontend
• Plonky2 frontend
• R1CS extraction
• Circuit graph visualization
• GitHub Action
• Hosted dashboard
• Witness counterexample generation
• Spec-to-circuit comparison
• Historical ZK bug benchmark suite

Security Philosophy

Nullsec S1-ZK treats ZK circuit bugs as proof semantics failures. It prioritizes cases where witness values, public claims, outputs, selectors, integer domains, and EC intermediates are not bound by constraints in the way the protocol likely intends.

The goal is not to replace human auditors. The goal is to give auditors sharper graph-aware evidence faster.

License

MIT