Language-Based Security for Low-Level MPC

TL;DR

This paper introduces a new programming language framework for defining and verifying low-level probabilistic MPC protocols, aiming to improve security assurance and reduce manual proof effort.

Contribution

It develops a staged programming language for low-level MPC, formalizes confidentiality and integrity hyperproperties, and provides automated verification tactics.

Findings

Formalizes hyperproperties like noninterference and declassification for MPC

Relates language hyperproperties to passive and malicious security models

Provides automated tactics for security verification in separation logic

Abstract

Secure Multi-Party Computation (MPC) is an important enabling technology for data privacy in modern distributed applications. Currently, proof methods for low-level MPC protocols are primarily manual and thus tedious and error-prone, and are also non-standardized and unfamiliar to most PL theorists. As a step towards better language support and language-based enforcement, we develop a new staged PL for defining a variety of low-level probabilistic MPC protocols. We also formulate a collection of confidentiality and integrity hyperproperties for our language model that are familiar from information flow, including conditional noninterference, gradual release, and robust declassification. We demonstrate their relation to standard MPC threat models of passive and malicious security, and how they can be leveraged in security verification of protocols. To prove these properties we develop automated tactics in $\mathbb{F}_2$ that can be integrated with separation logic-style reasoning.