-
Notifications
You must be signed in to change notification settings - Fork 0
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
1 parent
098eff7
commit 07c87c2
Showing
2 changed files
with
34 additions
and
7 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,12 +1,24 @@ | ||
--- | ||
title: "COMING SOON: PL Theory for SMPC Implementations" | ||
title: "PL Theory for SMPC Implementations" | ||
date: 2022-06-17 13:00:00 | ||
description: "Programming Language(s) for automatic verification of Secure Multi-Party Computation implementations" | ||
--- | ||
|
||
My primary reseach 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 primative, | ||
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. | ||
|
||
TODO: Write about the work I'm building on top of and some of the key ideas so far. | ||
[Earlier work](https://arxiv.org/abs/1806.07197) 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](https://arxiv.org/abs/1711.09305). | ||
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](https://link.springer.com/chapter/10.1007/3-540-36377-7_13) | ||
and [causal-graphical-model analysis](https://arxiv.org/abs/1301.3847) to bridge the remaining gap. | ||
We expect to start presenting a solution based on [Sum-Product-Networks](https://arxiv.org/abs/1202.3732) this Fall. | ||
|