On compiling Boolean circuits optimized for secure multi-party computation

Secure multi-party computation (MPC) allows two or more distrusting parties to jointly evaluate a function over private inputs. For a long time considered to be a purely theoretical concept, MPC transitioned into a practical and powerful tool to build privacy-enhancing technologies. However, the practicality of MPC is hindered by the difficulty to implement applications on top of the underlying cryptographic protocols. This is because the manual construction of efficient applications, which need to be represented as Boolean or arithmetic circuits, is a complex, error-prone, and time-consuming task. To facilitate the development of further privacy-enhancing technology, multiple compilers have been proposed that create circuits for MPC. Yet, almost all presented compilers only support domain specific languages or provide very limited optimization methods. In this work (this is an extended and revised version of the paper ‘Secure Two-party Computations in ANSI C’ (Holzer et al., in: ACM CCS, 2012) that reflects the progress in secure computation and describes the current optimization tool chain of CBMC-GC) we describe our compiler CBMC-GC that implements a complete tool chain from ANSI C to circuit. Moreover, we give a comprehensive overview of circuit minimization techniques, which we have identified and adapted for the creation of efficient circuits for MPC. With the help of these techniques, our compilation approach allows for a high level of abstraction from the cryptographic primitives used in MPC protocols, as well as the complex design of digital circuits. By using the model checker CBMC as a compiler frontend, we illustrate the link between MPC, formal methods, and digital logic design. Our experimental results illustrate the effectiveness of the implemented optimizations techniques for various example applications. In particular, compared with other state-of-the-art compilers, we show that CBMC-GC compiles circuits from the same source code that are up to four times smaller.