Taypsi: Static Enforcement of Privacy Policies for Policy-Agnostic Oblivious Computation

TL;DR

The paper addresses the scalability bottleneck of policy-agnostic MPC by replacing dynamic policy enforcement with a static, translation-based approach. It introduces Taypsi, a language that extends Taype with $\Uppsi$-types to enable modular, policy-driven translations of non-secure programs into secure, oblivious counterparts, particularly for structured data. The authors formalize the core calculus $\lambda_{OADT\Uppsi}$, prove security guarantees (obliviousness) and correctness of the translation, and present a complete lifting pipeline with constraint solving that yields multiple private versions of functions while preserving semantics. Empirical results show exponential performance improvements over the prior dynamic approach on complex benchmarks, with additional optimizations and a scalable compilation process. Overall, Taypsi cleanly separates privacy policy specification from program logic and provides a principled, verifiable path to efficient policy-accurate MPC for structured data.

Abstract

Secure multiparty computation (MPC) techniques enable multiple parties to compute joint functions over their private data without sharing that data with other parties, typically by employing powerful cryptographic protocols to protect individual's data. One challenge when writing such functions is that most MPC languages force users to intermix programmatic and privacy concerns in a single application, making it difficult to change or audit a program's underlying privacy policy. Prior policy-agnostic MPC languages relied on dynamic enforcement to decouple privacy requirements from program logic. Unfortunately, the resulting overhead makes it difficult to scale MPC applications that manipulate structured data. This work proposes to eliminate this overhead by instead transforming programs into semantically equivalent versions that statically enforce user-provided privacy policies. We have implemented this approach in a new MPC language, called Taypsi; our experimental evaluation demonstrates that the resulting system features considerable performance improvements on a variety of MPC applications involving structured data and complex privacy policies.

Figures (5)

• Figure 1: Filtering a list
• Figure 2: Oblivious lists with maximum and exact length public views
• Figure 3: Public and oblivious types
• Figure 4: $\Uppsi$-structures of
• Figure 5: $\lambda_{\mathtt{OADT}\Uppsi}$ syntax with extensions to $\lambda_{\mathtt{OADT}}$ highlighted