SMT-Boosted Security Types for Low-Level MPC

TL;DR

This paper introduces a new type theory for secure multi-party computation that leverages SMT verification to automatically ensure correctness, confidentiality, and integrity in distributed protocols, enhancing automation and scalability.

Contribution

It presents a novel type theory integrated with SMT verification for automatically enforcing security properties in MPC protocols within the Prelude/Overture framework.

Findings

Automated enforcement of security properties in MPC protocols.

Scalable analysis for arbitrary prime fields.

Generalization to various data and key sizes.

Abstract

Secure Multi-Party Computation (MPC) is an important enabling technology for data privacy in modern distributed applications. We develop a new type theory to automatically enforce correctness,confidentiality, and integrity properties of protocols written in the \emph{Prelude/Overture} language framework. Judgements in the type theory are predicated on SMT verifications in a theory of finite fields, which supports precise and efficient analysis. Our approach is automated, compositional, scalable, and generalizes to arbitrary prime fields for data and key sizes.