Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Language-Based Security for Low-Level MPC

Christian Skalka, Joseph P. Near

TL;DR

This work presents a language-based framework for defining and verifying low-level probabilistic MPC protocols. It introduces the Overture protocol language and a Prelude metalanguage, formalizes confidentiality and integrity hyperproperties (conditional noninterference, gradual release, robust declassification) in a probabilistic setting, and develops automated verification tactics in $\mathbb{F}_2$. It demonstrates end-to-end verification on concrete MPC primitives and 2-party constructions like GMW and BDOZ, connecting low-level protocol design to standard security models (passive and malicious). The approach supports mechanized reasoning and automation, enabling scalable verification and providing a foundation for future extensions to concurrency, larger fields, and UC-style security.

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.

Language-Based Security for Low-Level MPC

TL;DR

This work presents a language-based framework for defining and verifying low-level probabilistic MPC protocols. It introduces the Overture protocol language and a Prelude metalanguage, formalizes confidentiality and integrity hyperproperties (conditional noninterference, gradual release, robust declassification) in a probabilistic setting, and develops automated verification tactics in . It demonstrates end-to-end verification on concrete MPC primitives and 2-party constructions like GMW and BDOZ, connecting low-level protocol design to standard security models (passive and malicious). The approach supports mechanized reasoning and automation, enabling scalable verification and providing a foundation for future extensions to concurrency, larger fields, and UC-style security.

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 that can be integrated with separation logic-style reasoning.
Paper Structure (33 sections, 11 theorems, 46 equations, 10 figures)

This paper contains 33 sections, 11 theorems, 46 equations, 10 figures.

Table of Contents

  1. Introduction
  2. Overview and Contributions
  3. Language design.
  4. Hyperproperty formulation.
  5. Fully and partially automated verification.
  6. Related Work
  7. The $\mathit{Overture}$ Protocol Language
  8. Syntax
  9. Semantics
  10. Example: Passive Secure Addition
  11. Security Model
  12. Probability Mass Functions
  13. Basic Distribution of a Protocol
  14. Honest and Corrupt Views
  15. Passive Correctness and Security
  16. ...and 18 more sections

Key Result

theorem 1

Assume given pre-imageable $\mathcal{F}$ and a protocol $\pi$ that correctly implements $\mathcal{F}$. If $\pi$ satisfies noninterference modulo output then $\pi$ is passive secure.

Figures (10)

  • Figure 1: Comparison of systems for verification of MPC security in PLs.
  • Figure 2: Top-to-bottom: Basic $\mathit{Overture}$ syntax, expression interpretation, and command evaluation.
  • Figure 3: Adversarial semantics, and semantics of $\texttt{assert}$.
  • Figure 4: Filtering solutions to expressions in $\mathbb{F}_2$.
  • Figure 5: $\mathit{Prelude}$ syntax (T), evaluation contexts (M), and operational semantics (B).
  • ...and 5 more figures

Theorems & Definitions (42)

  • definition 1
  • definition 2
  • definition 3
  • definition 4
  • definition 5
  • definition 6
  • definition 7
  • definition 8
  • definition 9: Corrupt and Honest Views
  • definition 10: Passive Correctness
  • ...and 32 more