BattleZips
  • Awesome Circom
  • 🔬Theory
    • Prerequisite Knowledge
    • Resources
      • White Papers & PDF's
      • Blogs and Writeups
      • Videos
      • Important Entities
      • Communities
    • Proving Schemes
    • Primitives
      • Hash Functions
      • Public Key Cryptosystems
        • Note on L1 key registry → L2 hot key + callback to circuit-optimized hash functions
        • ECDSA & secp256k1
        • EdDSA
      • Merkle Trees
        • What is a Merkle Tree?
        • What is a merkle proof of inclusion?
        • zk-kit
        • Incremental Merkle Trees
        • Sparse Merkle Trees
        • Tree Arity (Binary, Quinary)
      • Semaphore
      • Arithmetic Circuits
  • 🏗️Development
    • Circom Language
      • Installation
      • IDE
      • Signals and Variables
      • Signal Assignment and Constraint Generation
      • Conditional Statements
      • Components and Templates
      • Circuit Compilation
      • Syntax
    • SnarkJS
      • Proving Schemes
      • Powers of Tau
      • ZK Keys
      • Zero Knowledge Proofs
      • On-Chain ZKP
      • Page 2
    • circomlib
      • Basic Math Constraints
      • Multiplexing
      • Hashing
      • EdDSA
      • circomlibjs
    • circom-tester
    • hardhat-circom
    • SHIELD
    • Circomspect
  • 🌆Ecosystem
    • Circom vs Other Solutions
      • Domain-Specific Languages
      • ZK Virtual Machines
      • ZK Ethereum Virtual Machines
    • Communities to Join
    • Recorded Content
    • Projects
  • 🛳️Examples
    • BattleZips V1
      • On the BattleZips Project
      • Docs holder
        • Join Game UML Sequence Diagram
        • Play Game UML Sequence Diagram
        • End Game UML Sequence Diagram
      • ZK Privacy Stack
      • Deploying Artifacts to Prod
      • Browser Client
    • RollupNC
      • Smart Contracts
      • Account/ State Tree
      • Transaction Tree
      • Layer 1 Deposits to Layer 2
      • Layer 2 Transacting
      • Layer 2 Withdrawals to Layer 1
Powered by GitBook
On this page
  • Intro
  • Static Analysis Capabilities
  • Links
  1. Development

Circomspect

Static analyzer for Circom syntax and safety

PreviousSHIELDNextCircom vs Other Solutions

Last updated 2 years ago

Intro

"In October 2019, a security researcher found a devastating vulnerability in Tornado.cash, a decentralized, non-custodial mixer on the Ethereum network... because of an issue in one of the ZKPs, anyone could forge a proof of deposit and withdraw funds from the system... This bug would have been caught using Circomspect, a new static analyzer for ZKPs."

This excerpt is taken from by the tool's creators. Read more about the bug and how Circomspect addresses it in the blog post.

Static Analysis Capabilities

This information is lifted word-for-word from the . As time progresses, Trail of Bits (Circomspect creator) plans to add more checks to the static analysis.

Warning Messages

Side-effect free assignments

An assigned value which does not contribute either directly or indirectly to a constraint, or a function return value, typically indicates a mistake in the implementation of the circuit. For example, consider the following BinSum template from circomlib where we've changed the final constraint to introduce a bug.

  template BinSum(n, ops) {
      var nout = nbits((2 ** n - 1) * ops);
      var lin = 0;
      var lout = 0;

      signal input in[ops][n];
      signal output out[nout];

      var e2 = 1;
      for (var k = 0; k < n; k++) {
          for (var j = 0; j < ops; j++) {
              lin += in[j][k] * e2;
          }
          e2 = e2 + e2;
      }

      e2 = 1;
      for (var k = 0; k < nout; k++) {
          out[k] <-- (lin >> k) & 1;
          out[k] * (out[k] - 1) === 0;

          lout += out[k] * e2;  // The value assigned here is not used.
          e2 = e2 + e2;
      }

      lin === nout;  // Should use `lout`, but uses `nout` by mistake.
  }

Here, lout no longer influences the generated circuit, which is detected by Circomspect.

Shadowing variable declarations

A shadowing variable declaration is a declaration of a variable with the same name as a previously declared variable. This does not have to be a problem, but if a variable declared in an outer scope is shadowed by mistake, this could change the semantics of the program which would be an issue.

For example, consider this function which is supposed to compute the number of bits needed to represent a.

  function numberOfBits(a) {
      var n = 1;
      var r = 0;  // Shadowed variable is declared here.
      while (n - 1 < a) {
          var r = r + 1;  // Shadowing declaration here.
          n *= 2;
      }
      return r;
  }

Since a new variable r is declared in the while-statement body, the outer variable is never updated and the return value is always 0.

Signal assignments using the signal assignment operator

Signals should typically be assigned using the constraint assignment operator <==. This ensures that the circuit and witness generation stay in sync. If <-- is used it is up to the developer to ensure that the signal is properly constrained. Circomspect will try to detect if the right-hand side of the assignment is a quadratic expression. If it is, the signal assignment can be rewritten using the constraint assignment operator <==.

However, sometimes it is not possible to express the assignment using a quadratic expression. In this case Circomspect will try to list all constraints containing the assigned signal to make it easier for the developer (or reviewer) to ensure that the variable is properly constrained.

The Tornado Cash codebase was originally affected by an issue of this type. For details see the Tornado Cash disclosure .

Branching statement conditions that evaluate to a constant value

If a branching statement condition always evaluates to either true or false, this means that the branch is either always taken, or never taken. This typically indicates a mistake in the code which should be fixed.

Use of the non-strict versions of Num2Bits and Bits2Num from Circomlib

For example, Suppose that we create a component n2b given by Num2Bits(254) and set the input to 1. Now, both the binary representation of 1 and the representation of p + 1 will satisfy the circuit over BN128, since both are 254-bit numbers. If you cannot restrict the input size below the prime size you should use the strict versions Num2Bits_strict and Bits2Num_strict to convert to and from binary representation. Circomspect will generate a warning if it cannot prove (using constant propagation) that the input size passed to Num2Bits or Bits2Num is less than the size of the prime in bits.

Overly complex functions or templates

As functions and templates grow in complexity they become more difficult to review and maintain. This typically indicates that the code should be refactored into smaller, more easily understandable, components. Circomspect uses cyclomatic complexity to estimate the complexity of each function and template, and will generate a warning if the code is considered too complex. Circomspect will also generate a warning if a function or template takes too many arguments, as this also impacts the readability of the code.

Informational Messages

Bitwise complement of field elements

Circom supports taking the 256-bit complement ~x of a field element x. Since the result is reduced modulo p, it will typically not satisfy the expected relations (~x)ᵢ == ~(xᵢ) for each bit i, which could lead to surprising results.

Field element arithmetic

Circom supports a large number of arithmetic expressions. Since arithmetic expressions can overflow or underflow in Circom it is worth paying extra attention to field arithmetic to ensure that elements are constrained to the correct range.

Field element comparisons

Field elements are normalized to the interval (-p/2, p/2] before they are compared, by first reducing them modulo p and then mapping them to the correct interval by subtracting p from the value x, if x is greater than p/2. In particular, this means that p/2 + 1 < 0 < p/2 - 1. This can be surprising if you are used to thinking of elements in GF(p) as unsigned integers.

Links

Using Num2Bits and Bits2Num from to convert a field element to and from binary form is only safe if the input size is smaller than the size of the prime. If not, there may be multiple correct representations of the input which could cause issues, since we typically expect the circuit output to be uniquely determined by the input.

🏗️
It Pays to be Circomspect
Circomspect rust crate
here
Circomlib
Introductory Blog Post by Trail of Bits
Source on GitHub
Rust Crate