Name
Abstract | ||
|---|---|---|
The practical application of Secure Two-Party Computation is hindered by the difficulty to implement secure computation protocols. While recent work has proposed very simple programming languages which can be used to specify secure computations, it is still difficult for practitioners to use them, and cumbersome to translate existing source code into this format. Similarly, the manual construction of two-party computation protocols, in particular ones based on the approach of garbled circuits, is labor intensive and error-prone. The central contribution of the current paper is a tool which achieves Secure Two-Party Computation for ANSI C. Our work is based on a combination of model checking techniques and two-party computation based on garbled circuits. Our key insight is a nonstandard use of the bit-precise model checker CBMC which enables us to translate C programs into equivalent Boolean circuits. To this end, we modify the standard CBMC translation from programs into Boolean formulas whose variables correspond to the memory bits manipulated by the program. As CBMC attempts to minimize the size of the formulas, the circuits obtained by our tool chain are also size efficient; to improve the efficiency of the garbled circuit evaluation, we perform optimizations on the circuits. Experimental results with the new tool CBMC-GC demonstrate the practical usefulness of our approach. |
Year | DOI | Venue |
|---|---|---|
2012 | 10.1145/2382196.2382278 | ACM Conference on Computer and Communications Security |
Keywords | Field | DocType |
standard cbmc translation,new tool,ansi c.,tool chain,bit-precise model checker cbmc,secure two-party computation,garbled circuit,two-party computation,secure computation,secure computation protocol,garbled circuit evaluation,privacy,model checking,compilers | Secure multi-party computation,Boolean circuit,Model checking,ANSI C,Computer science,Computer security,Source code,Compiler,Secure two-party computation,Computation | Conference |
Citations | PageRank | References |
58 | 1.48 | 26 |
Authors | ||
4 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Andreas Holzer | 1 | 197 | 13.62 |
| Martin Franz | 2 | 58 | 2.50 |
| Stefan Katzenbeisser | 3 | 1844 | 143.68 |
| Helmut Veith | 4 | 2476 | 140.58 |