Introduction

This project was published as

Fan, Yongming, Yuquan Xu, and Christina Garman. "SNARKProbe: An Automated Security Analysis Framework for zkSNARK Implementations." International Conference on Applied Cryptography and Network Security. Cham: Springer Nature Switzerland, 2024.

Abstract

With the recent growing interest in privacy-enhancing technologies, we are seeing a complementary growth in the desire to build and deploy complex cryptographic systems that involve techniques like zero-knowledge proofs. Of these, general purpose proof systems like zkSNARKs have seen the most interest, due to their small proof size, fast verification, and expressiveness. Unfortunately, as we have seen with many areas of cryptography, guaranteeing correct implementations can be tricky, as the protocols themselves are complicated and often require substantial low-level manual effort to achieve maximum performance. To help with this problem, and gain better assurances about the correctness and security of already implemented zkSNARK protocols and applications, we design and build SNARKProbe, an automated security analysis framework for zkSNARKs that can scan R1CS-based libraries and applications to detect various issues, such as edge case crashing, cryptographic operation errors, and/or inconsistencies with protocol descriptions. SNARKProbe leverages a variety of analysis techniques, including fuzzing and SMT solvers. We test the performance of SNARKProbe on a variety of different experimental parameters to demonstrate its practicality and reasonable runtime, and we also evaluate its ability to find potential inconsistencies and errors in implementations.

About The Tool

We provide two tools in this project, ConstraintChecker and SnarkFuzzer

1. ConstraintChecker

The primary goal of the ConstraintChecker is to help ensure that the realized proof is equivalent to a specified statement. This also allows the ConstraintChecker to find errors in flattening and/or gadget use. It achieves this by comparing the equivalence of a user-specified proof statement and the compiled R1CS gates to ensure that the proof generated by the library represents the developer's specified statement.

2. SnarkFuzzer

SnarkFuzzer is a smart fuzzing tool with the primary goal of finding potential logic or software errors in zkSNARK libraries. It produces zkSNARK programs with different proofs as input, to detect and catch these errors and provide full (important) code coverage.

Getting Started

Prerequisites

Before installation:

sudo apt-get update

General Dependencies

• python3 (3.7 or higher required, helpful link for installing python3.10: https://cloudbytes.dev/snippets/upgrade-python-to-latest-version-on-ubuntu-linux)
• git
• valgrind
• cargo (installation guide can be found here: https://itsfoss.com/install-rust-cargo-ubuntu-linux/)

sudo apt install python3 git valgrind

• pip

curl https://bootstrap.pypa.io/get-pip.py -o get-pip.py
python3 get-pip.py

Python Dependencies

• z3-solver
• numpy
• scipy
• atheris (Clang required, installation guide can be found here: https://clang.llvm.org/get_started.html)
• py_ecc

sudo python3 -m pip install z3-solver numpy scipy py_ecc

Dependencies for py_ecc (use pip3 install)

• mypy-extensions
• eth_typing
• eth_utils (Cython required)

sudo python3 -m pip install mypy-extensions eth_typing Cython eth_utils

Dependencies for libsnark

• build-essential
• cmake (3.13.4 or higher)
• libgmp3-dev
• libprocps-dev
• python3-markdown
• libboost-program-options-dev
• libssl-dev
• pkg-config

sudo apt install build-essential cmake git libgmp3-dev libprocps-dev python3-markdown libboost-program-options-dev libssl-dev pkg-config

Installation

1. Clone the repo

   git clone https://github.com/fanym919/snarktool.git

2. Install Libsnark example program

   cd model/depends/
   python3 install.py

3. Install Bellman example program

   cd model/depends/
   git clone https://github.com/arcalinea/bellman-examples.git
   cd bellman-examples
   cargo build

4. Modify config.txt based on target library
5. Navigate to model/, run

   python3 main.py

Usage

To run these tools, read their documentation at

ConstraintChecker: here

SnarkFuzzer: here

We also provde several demonstration programs for each tool