Overview

Circuitous is a set of tools and libraries used in Trail of Bits' work on the DARPA SIEVE program to generate circuits used in zero-knowledge proofs of exploit. It is unique in that the circuits it produces are tailored to a specific binary. Circuitous accomplishes this by lifting binaries to LLVM and recovering instruction decoding via fuzzing. It lowers to a custom CircIR, further optimizing using an equality saturation-based framework. CircIR can be targeted to output circuits in a variety of formats: we use Verilog on SIEVE.

Using a binary-specific circuit has many benefits: principally, it reduces circuit area by only modeling instructions actually used in the binary (as opposed to the entirety of an instruction set supported by a processor)- no need to pay for what you don't use. Since circuits are generated rather than handwritten, they are super easy to extend (just run the tooling again if your binary changes). The framework can also be used to experiment with different approaches to circuit design (e.g., different gate cost models).

While we do provide core parts of the project as a libary, there are also some drivers ready to be used. circuitous-seed can provide a list of instructions to lift from a given binary. (This list can subsequently be modified to exclude instructions.) circuitous-lift then takes this input and emits a circuit, generally in Verilog. We will eventually provide a full step-by step example, but for now, you can invoke --help on the respective tools, check out the Usage section and tests, or open an issue or discussion topic!

Since this project is in active development, there are some caveats:

• We currently support only a subset of x86 (both 32-bit and 64-bit - see Tiny86 for more details) and the API is not super stable yet.
• Due to how the internals of Circuitous work, it is hard to produce a circuit with all forms of given instruction (e.g., all variants of add) - since it ingests the instruction encoding as input.
• Reducing circuit size is a really hard task, and we are still trying to improve effectiveness of some of our optimizations.

Build

Build of circuitous follows the traditional, modern cmake build process. The simplest way to build and install the project is to use premade presets that take care of downloading all dependencies. Dependencies of circuitous are managed by vcpkg manifest file. Before building one need to specify environment variables CXX_COMMON_ROOT and VCPKG_ROOT that point to folders of pre-downloaded vcpkg and cxx-common or run scripts/build/setup.sh to download and setup these dependencies automatically. We also suggest setting CC and CXX to clang when also building dependancies, as some require this.

Depending on your system, use linux or osx preset. To make debug build use deb presets:

# configure project
cmake --preset ninja-cxx-common-x64-osx-rel

# build project
cmake --build --preset ninja-cxx-common-osx-rel

# install project
cmake --build --preset ninja-cxx-common-osx-rel --target install

Development build

If you want to use your own prebuilt dependencies, project presets allow you to configure the build. For example, if you have prebuilt llvm, can be from cxx-common package, you can specify CMAKE_PREFIX_PATH to point to LLVMConfig.cmake folder. For example:

CMAKE_PREFIX_PATH=${CXX_COMMON_ROOT}/installed/x64-linux-rel/share/:${CMAKE_PREFIX_PATH}

Then use presets with prefix ninja-cxx-common-system-llvm and your desired triplet. Similarly, to build with system remill use presets prefixed ninja-system-remill.

Testing

ctest --preset ninja-cxx-common-osx-deb-test

Dependencies

Name	Version
Git	Latest
CMake	3.23+
Clang	12+
ccache	Latest
cxx-common	0.2.6
llvm	14+
remill	Latest
gap	Latest
doctest	2.4.8+
spdlog	1.10.0

For python dependencies see requirements.txt and for c++ vcpkg.json.

Usage

circuitous-lift

The main binary that produces the circuits. It has several options, which falls into few categories.

• --arch and --os are defaulted to mac and current machine (these are needed to initialise libraries circuitous uses under the hood)
• Some form of input

• --bytes-in raw bytes in human readable form (for example 1468 for some version of ADC). More encodings should be just concatenated together.
• --ciff-in a config file provided by circuitous-seed. You can find some example in scripts/seed_sets/*.ciff

• Run information

• --lift-with to specify the lifter to use (currently only v2 is supported with v1 being deprecated and v3 in active development. As you probably guessed these are placeholder names.

• Outputs

• --verilog-out outputs the circuit in verilog

• Random

• --quiet to silence debug/log outputs

So an example invocation may look like

circuitous-lift --arch amd64 --os macos \
                --lift-with v2 \
                --bytes-in 1468 \
                --verilog-output out.v \
                --quiet

Tests

See test/README.md

Dev Container for Actions

Run manually Build Dev Container action or execute:

docker build .devcontainer --no-cache \
    -t ghcr.io/trailofbits/circuitous-ubuntu-22.04-dev:latest

docker push ghcr.io/trailofbits/circuitous-ubuntu-22.04-dev:latest

This requires to have CLI access to github resources.

Benchmarks

See scripts/bench/README.md.

Distribution and Licensing

This research was developed with funding from the Defense Advanced Research Projects Agency (DARPA) under Agreement No. HR001120C0084.

The views, opinions, and/or findings expressed are those of the author(s) and should not be interpreted as representing the official views or policies of the Department of Defense or the U.S. Government.

DISTRIBUTION STATEMENT A: Approved for public release, distribution unlimited.

circuitous is licensed under the GNU AGPLv3 License. A copy of the terms can be found in the LICENSE file.