NetList is a library written in Haskell that allows easy generation of circuit descriptions. It is not meant to be used for hardware circuits, but for static-valued circuits instead, where each wire has a constant value. It includes efficient constructions for various simple data structures that are commonly useful in implementing circuits. Currently it can produce circuit descriptions in two different formats:
GCParser's input format for executing secure computation
DIMACS format that should work on any of off-the-shelf SAT solvers popular today. We tested it with Lingeling.
In this library, we have efficient implementations of the same data structures we describe in our paper below. We might add more if requested by others. If you want to generate circuit descriptions in other formats (e.g. the SMTLIB format), it should not be hard to add another backend to the system. While we do not have any developer's documentation for this yet, please let us know if you want to know more about how to do this.
This software package is made freely available under the Apache License, Version 2.0.
Abstract Several techniques in computer security, including generic protocols for secure computation and symbolic execution, depend on implementing algorithms in static circuits. Despite substantial improvements in recent years, tools built using these techniques remain too slow for most practical uses. They require transforming arbitrary programs into either Boolean logic circuits, constraint sets on Boolean variables, or other equivalent representations, and the costs of using these tools scale directly with the size of the input circuit. Hence, techniques for more efficient circuit constructions have benefits across these tools. We show efficient circuit constructions for various simple but commonly used data structures including stacks, queues, and associative maps. While current practice requires effectively copying the entire structure for each operation, our techniques take advantage of locality and batching to provide amortized costs that scale polylogarithmically in the size of the structure. We demonstrate how many common array usage patterns can be significantly improved with the help of these circuit structures. We report on experiments using our circuit structures for both generic secure computation using garbled circuits and automated test input generation using symbolic execution, and demonstrate order of magnitude improvements for both applications