origolab/origo-compiler-build repository overview

⁠Origo Compiler

⁠Introduction

Origo-Compiler is the project to create a compiler toolchain for compiling programs to circuits for verifiable or secure computation purpose, with support for any possible frontend language for LLVM, like C, C++, rust and so on, even solidity and python.

⁠Background

As the fundamental computation model of theoretical computer science, arithmetic circuit (AC) also plays an important role in cryptography. Secure computation was first formally studied by Andrew Yao in the early 1980s [1]. His introductory paper demonstrated protocols for a few examples, but did not prove every function was securely computable. That didn’t happen until 1986, with the construction of Yao’s garbled circuits [2]. In this work and followed efforts, it is proved that every circuit is securely computable and every function can be converted to an equivalent circuit. Even recent breakthrough results on fully homomorphic encryption (e.g. [3][4]) provide an alternative method for constant-round secure computation that has better asymptotic communication complexity. But it is still quite inefficient for practical usage. So most secure computation protocols are studied based on (boolean or arithmetic) circuits as an abstraction of computation.

However, there is a huge representation gap: secure computation protocols rely on circuits, but programmers in reality write programs. So secure computation compiler which is in charge of compiling programs to circuits becomes important topic for practical secure computation applications. There are already lots of works done in the field. For verifiable computation, researcher have developed tool for converting a subset of C language (or LLVM [16] IR for C) to quadratic arithmetic program (QAP) [10, 11], which is another representation of certain types of computation (Its relation to AC, you can find it here.); or tools for converting C programs to certain DLS programs then to circuits [12, 13]. For secure multi-party computation, there are tools for converting a subset of specific high level languages, like ANSI C [5] [6] or comprising their own DSL, such as TASTYL [7], Wysteria [8], ObliVM-lang [9] and so on. Zokrates [14] is the project to create offchain programs with its own language and link them to the Ethereum blockchain to make them verifiable with zkSNARKs [15].

The tools described above all suffer certain drawbacks which make them not easy to use for general purposes in verifiable or secure computation, especially for the programmers who do not have cryptography background; some of them only support C programs, or their own DSLs; some convert programs to certain type of computation representations directly instead of the circuits, which limit their backend cryptography protocols to only specific ones; some of them need a preset repetition count upper bound for the loops of the programs, and so on.

⁠Design

Origo-Compiler defines its own Circuit Intermediate Representation (CIR) of the circuit. It generates the CIR by consuming LLVM IR. The the CIR can be used as input to different optimizers to generate optimized circuits for different purposes, like circuits for zero knowledge proof (ZKP) or MPC, even for different protocols, like Pinocchio [12], Geppetto [13] or Bulletproof [17]). The CIR leverages some concise representation advantages, for example the loop instruction of the programs can be represented by the special type of circuit -- the head-tail connection circuit:

⁠Components of CIR

CIR mains three major components, CircuitBoard, BoardContext, Connector and ConnectorType.

⁠CircuitBoard

CircuitBoard represents a circuit combination, which is a systemically organized circuit stacks. This is the top level container of all program-converted circuits, it is the top level container for CIR.

⁠BoardContext

BoardContext owns and manages the CircuitBoard’s “global” data, including type and constant unique tables. It helps to maintain and create ConnectorTypes for one CircuitBoard.

⁠Connector

Connector is the base type for all the computation elements in the circuit, for example, wires and gates are all subclasses of Connector class. Each connector instance has a correponding ConnectorType, which describes the basic properties of that connector. Connector could be a container for multiple sub-connectors and works as a combination of organized and wired connectors.

⁠ConnectorType

ConnetorType is the collection of the properties of the Connector, it describes the basic attributes of the corresponding connector, like the input wires, output wires and their value types.

⁠Build instructions

⁠Dependencies

The origo-compiler library relies on the following:

• C++ build environment
• CMake build infrastructure
• llvm
• boost
• Fetched and compiled via Git submodules: solidity⁠

⁠Building

Fetch dependencies from their GitHub repos:

$ git submodule init && git submodule update

Create the Makefile:

$ mkdir build && cd build $ cmake ..

Build the library:

$ make

⁠Reference

[1] Andrew C. Yao. Protocols for secure computations (extended abstract). FOCS ’82, pages 80–91.

[2] Andrew C. Yao. How to generate and exchange secrets (extended abstract). In 27th FOCS, pages 162–167.

[3] C. Gentry. Fully homomorphic encryption using ideal lattices. In STOC, pages 169–178, 2009.

[4] C. Gentry and S. Halevi. Fully homomorphic encryption without squashing using depth-3 arithmetic circuits. In FOCS, 2011

[5] A. Holzer, , M. Franz, S. Katzenbeisser, and H. Veith. Secure Two-Party Computations in ANSI C. In ACM Conference on CCS, 2012..

[6] Y. Zhang, A. Steele, and M. Blanton, “PICCO: a general-purpose compiler for private distributed computation,” In ACM Conference on CCS, 2013.

[7] W. Henecka, S. Kogl, A.-R. Sadeghi, T. Schneider, and I. Wehrenberg, ¨ “Tasty: tool for automating secure two-party computations,” in CCS, 2010.

[8] A. Rastogi, M. A. Hammer, and M. Hicks, “Wysteria: A Programming Language for Generic, Mixed-Mode Multiparty Computations,” in S & P, 2014.

[9] C. Liu, X. S. Wang, K. Nayak, Y. Huang, and E. Shi. ObliVM: A programming framework for secure computation. In S&P, 2015

[10] C. Costello, C. Fournet, J. Howell, M. Kohlweiss, B. Kreuter, M. Naehrig, B. Parno, S. Zahur. Geppetto: Versatile Verifiable Computation. In Proceedings of the IEEE Symposium on Security and Privacy, 2015

[11] https://github.com/amiller/geppetto⁠

[12] E. Ben-Sasson, A. Chiesa, D. Genkin, E. Tromer, and M. Virza. SNARKs for C: Verifying program executions succinctly and in zero knowledge. In CRYPTO, 2013.

[13] E. Ben-Sasson, A. Chiesa, E. Tromer, and M. Virza. Succinct noninteractive zero knowledge for a von neumann architecture. In Security, 2014.

[14] https://github.com/JacobEberhardt/ZoKrates⁠

[15] C. Reitwießner, zkSNARKs in a Nutshell, http://chriseth.github.io/notes/articles/zksnarks/zksnarks.pdf⁠

[16] https://llvm.org/⁠

[17] B. Bunz, J. Bootle, D. Boneh, A. Poelstra, P. Wuille, and G. Maxwell. Bulletproofs: Efficient range proofs for confidential transactions, 2017.