March 24, 2023
Secure multiparty computation (MPC) allows for joint computation over private data from multiple entities, usually backed by powerful cryptographic techniques that protect sensitive data. Several high-level programming languages have been proposed to make writing MPC applications accessible to non-experts. These languages typically require developers to enforce security policies within the logic of the secure application itself, making it difficult to update security requirements, or to experiment with different policies. This paper presents the design and implementation of Taype, a language that permits security concerns to be decoupled from the program logic. To do so, Taype provides the first implementation of oblivious algebraic data types and tape semantics, two language features recently proposed by a core calculus for oblivious computation, lambda OADT+. We evaluate our implementation of Taype on a range of benchmarks, demonstrating its ability to encode a range of security polices for a rich class of data types.
About Qianchuan
Qianchuan Ye is a PhD student at Purdue advised by Benjamin Delaware. He likes proofs.