PhD Proposal: Semantics Preserving Compilation of Mixed-Mode Computations

Talk
Aseem Rastogi
Time: 
01.23.2015 14:00 to 15:30
Location: 

AVW 3460

In a Secure multi-party computation (SMC), mutually distrusting parties use cryptographic techniques to cooperatively compute over their private data; in the process each party only learns the explicitly revealed outputs, while cryptography hides other computation details. Some applications of SMCs include auctions (where bids are the private data), elections (where votes are the private data), and statistical computations.
SMC also finds applications in military where multiple coalitions want to compute over their private resources without sharing details with each other. Despite their usefulness, SMCs have remained largely intractable to the programmers, and unusable for real-world applications. The cryptographic techniques (e.g. garbled circuits) used to implement SMCs can be prohibitively expensive for large applications. More importantly, existing languages for programming SMCs are either too low-level (e.g. at the level of boolean circuits) or lack abstractions required to program real applications (e.g. no support for integrating local computations with secure computations).
Our previous work has focused on making SMCs more practical by applying ideas from programming languages. We have developed program analyses to perform knowledge inference, that can further be used to optimize SMC programs (Rastogi et. al. PLAS''13). Our algorithms, given an SMC program, output which intermediate variables are known to which parties. We have also designed and implemented a high-level functional language, called Wysteria, for writing SMC programs (Rastogi et. al. IEEE S&P''14). Wysteria supports writing mixed-mode programs, programs that combine local computations and secure computations. These mixed-mode computations can be viewed as having a single thread of control, providing a conceptual single-threaded semantics that makes programs far easier to write and reason about. We have implemented a game of mental-poker in Wysteria where card dealing is done using secure computation.
In this thesis proposal, we propose extending Wysteria to provide more robust guarantees from the Wysteria programs that the programmer writes. In particular, we plan to formally verify that the Wysteria compiler, when it compiles a single threaded program to the actual multi-threaded protocol, preserves the semantics of the program. Furthermore, we plan to take advantage of Wysteria''s single-threaded program view, and enable programmers to verify functional correctness of the programs they write (e.g. a sorting SMC program does indeed sort the inputs); a single program is arguably easier to verify than n concurrent programs. Such guarantees would be suitable for highly sensitive settings such as military. We plan to achieve these by embedding Wysteria in F*, - a dependently-typed functional language designed for program verification. Going forward, we would also look at implementing our PLAS''13 analysis in a relational version of F*. To build more trust in the tool chain, we would also verify the GMW protocol, crypto protocol that computes boolean circuits, in F*.
Eventually, we hope that our work would result in a general framework for developing more analyses for SMCs and would contribute to actually realizing the promise that SMCs have shown since decades.
Examining Committee:
Committee Chair: - Dr. Michael Hicks
Dept's Representative - Dr. Elaine Shi
Committee Member(s): - Dr. Jeffrey Foster
- Dr. Rance Cleaveland