Taypsi: Static Enforcement of Privacy Policies for Policy-Agnostic Oblivious Computation
summary
A new MPC language called Taypsi compiles ordinary functional programs with recursive ADTs into policy-respecting oblivious implementations using a lifting algorithm that generates constraints solved by CVC3; the compiler and typechecker are implemented and artifacts are available. The system encodes policies as oblivious algebraic data types (public views like maximum length), pads representations to hide shape, proves type soundness and obliviousness, and reports exponential speedups over prior dynamic enforcement—several workloads that previously timed out now complete in seconds.
AI-written summary · about
chapters (13)
- 0:00Taypsi and APC language
- 1:25Secure app implementation challenges
- 3:55Policy-agnostic privacy goal
- 5:40Taypsi language design
- 6:22Taypsi in action example
- 8:47Oblivious algebra data types
- 10:11Side types for translation
- 11:36Private filter function
- 12:41Lifting algorithm and constraints
- 13:43Compilation overhead results
- 14:47Formal security guarantees
- 15:53Taypsi features summary
- 16:38Q&A on timing channels
related talks
27mOblivious Privacy in a Statically Typed World
56mFormal Methods and Proofs of Privacy Properties, Part II
28mType-directed Program Transformation for Constant-Time Enforcement
18mSpace-Efficient Polymorphic Gradual Typing, Mostly Parametric
16mBalancing Privacy: Leveraging Privacy Budgets for Privacy-Enhancing Technologies
21mPrivacy and Compliance - A pragmatic approach
22mPrivacy-preserving Computation in Plain Sight
18mDeveloping a Dependently Typed Language with Runtime Proof Search