CircGen - Circuit Description Generation tool
This is a prototype of the CircGen tool. It is based on CompCert - a certified compiler for C (http://compcert.inria.fr). Please consult the original CompCert's README and its manual for addition information on CompCert on its copyright/usage instructions.
The current prototype translates source C programs into a representation of combinatory boolean circuits in a format accepted by most secure computation engines (the Bristrol SMC circuit syntax). The tool is fully functional but is still under active development. It still lacks support for specific features (such as division and moduli operations, floating-point types, etc.). Please refer to the paper A Fast and Verified Software Stack for Secure Function Evaluation for further details.
Instalation
This repository includes, as a submodule, the original CompCert distribution (v2.5).
Dependencies
In order to compiler to prototype, the following dependencies are needed:
- Python3
- Ocaml functional language (version 4.00 or higher)
- Coq proof assistant (version 8.4.6)
- Menhir parser generator
- SsReflect Ssreflect/MathComp (version 1.6.1)
All the above packages are available through the OPAM (Ocaml Package Manager).
opam install coq-8.4.6
...
opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq-mathcomp-algebra.1.6.1
Clone the repository
The circgen
tool reposity includes the CompCert repository as a submodule.
In order to clone it (including CompCert's repo) please perform:
$ git clone --recursive https://github.com/haslab/CircGen.git
$ cd circgen
build
directory
Preparing the The tool is compiled in a dedicated build
directory that only has
links to both CompCert's and CircGen's source files. The toplevel Makefile
includes a target to setup the build
directory.
$ make clean_setup_build_dir
$ cd build
Compilation
To compile the tool, please execute ($OS is either macosx
or linux
):
$ ./configure bool-circ-$OS
$ make depend
$ make
Examples
Directory ./tests/bcircuits
includes several examples on the usage of
the tool. These examples include standard SMC test circuits, such as
the AES symmetric cipher or the SHA-256 compression function.