My primary research project this year is to build a language with type system enforcing MPC security. This is not a language that takes SMPC protocols as primitives; instead it takes communication between parties as its key primitive, and an SMPC scheme such as GMW can be build inside of it and type-checked. Once the language can be made sufficiently expressive, people will be able to express new or special-case protocols and use the type-checker instead of bespoke proofs of security.
Earlier work accomplished a similar goal, but restricted itself to situations where the “Ideal Functionality” was an (efficiently!) invertible function. Since existing general-purpose SMPC protocols can easily compute non-invertible functions, this is a serious limitation.
Our work began by building on top of Darais, Sweet, Liu, & Hicks’s language λ-obliv. Their type system supports a lemma guaranteeing uniformity and independence of random values that appear during program execution; this can be used to trivialize most of the work of a hypothetical simulator of the program in question. We’ve been investigating various techniques for program inversion and causal-graphical-model analysis to bridge the remaining gap. We expect to start presenting a solution based on Sum-Product-Networks this Fall.