diff --git a/_posts/2022-06-17-metadata-secure-messaging.md b/_posts/2022-06-17-metadata-secure-messaging.md index 43aed78..cf03aab 100644 --- a/_posts/2022-06-17-metadata-secure-messaging.md +++ b/_posts/2022-06-17-metadata-secure-messaging.md @@ -1,19 +1,34 @@ --- -title: "COMING SOON: Metadata-privacy preserving Instant Messaging" +title: "Metadata-privacy preserving Instant Messaging" date: 2022-06-17 12:00:00 description: "What existing tools for private massaging exist (or could exist) beyond end-to-end encryption?" --- +{% include section.html c="Update Oct 2022" %} + +It had previously been proposed that [Fuzzy Message Detection](https://eprint.iacr.org/2021/089) +could be extended to give more formal guarantees of privacy in a central-server-based messaging system. +[More recent work](https://arxiv.org/abs/2109.06576) clarified the guarantees provided by the original FMD definition, +and showed that for practical purposes it provides very little privacy. + +A few of us are still investigating this line of research. +In particular, + +- How do the guarantees of FMD change or improve if a false-negative rate is introduced to the scheme? + Can any such advantages be preserved while also taking steps to mitigate the usability problems of false-negatives? +- How can FMD be combined with other systems to given better practical performance and privacy? + ([Open Privacy Research Society](https://openprivacy.ca/) has already done some work here, + _e.g._ [niwl](https://git.openprivacy.ca/openprivacy/niwl).) {% include section.html c="TLDR: Use Signal" %} While there are a lot of really cool projects out there that I want to write about here, -[Signal](https://signal.org/) is _ok_, and you can install it and start using it _today_. +[Signal](https://signal.org/) is _ok_, and you can install it and start using it _right now_. I look forward to a day when I can update this tldr! {% include section.html c="Metadata privacy in Instant Messaging" %} -One of my current research interests is advanced privacy-preserving IM tools. +One of my current research interests is advanced privacy-preserving IM tools. E2EE, done correctly (_a la_ Signal) prevents any third parties from reading your messages, but leaves a great deal of useful information unprotected, such as diff --git a/_posts/2022-06-17-pl-theory-for-smpc.md b/_posts/2022-06-17-pl-theory-for-smpc.md index 2204dbc..eec48a0 100644 --- a/_posts/2022-06-17-pl-theory-for-smpc.md +++ b/_posts/2022-06-17-pl-theory-for-smpc.md @@ -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.