April 23, 2021
Oblivious computation is computation on private data while keeping that data secure. It finds application in many privacy-sensitive domains. While the computation is usually encoded as some circuits for the cryptographic protocols, many programming languages are proposed to provide a high-level interface to the programmers. However, these languages assume the structure of the private data is always public, if they allow structured data at all. So, if the programmers want to hide the private structured data completely, they have to manually “pad” the data and protect themselves against, say, timing channel. In this talk, I will introduce our ongoing work on a programming system with algebraic data types (ADT), where the computation is also oblivious of the structure of the data. We propose a core calculus for doing such oblivious computation, dubbed λOADT, where oblivious ADTs are expressed as indexed types a la large elimination. We also propose another higher-level language, dubbed λPADT, where oblivious ADTs are expressed as indexed types a la subset types, which makes it better suited for programming and reasoning about. A translation process is needed to connect them. To this end, we design an algorithm to derive primitive oblivious operations for ADTs that is correct-by-construction and oblivious-by-fusion.