SMT-Boosted Security Types for Low-Level MPC
Christian Skalka, Joseph P. Near
TL;DR
This work addresses automated verification of correctness and security for low-level MPC protocols by marrying SMT-based constraint solving over finite fields with a robust type-theoretic framework. It introduces confidentiality and integrity type systems, augmented by a dependent Hoare-logic layer in Prelude/Overture, to enable compositional and scalable verification across arbitrary prime fields $\mathbb{F}_p$. The approach provides soundness guarantees for both passive and malicious security (with hyperproperties such as noninterference modulo output and integrity under adversarial behavior) and supports constraint-based reasoning via Satisfiability Modulo Finite Fields (SMFF). Extended examples (GMW, BD OZ, YGC) demonstrate practical applicability, and performance results show SMT-based verification remains efficient (e.g., milliseconds for 3-party addition in large fields on typical hardware). Overall, the framework offers automated, scalable, field-general verification for low-level MPC protocols, enabling safer composition and deployment of privacy-preserving computations.
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.