SMT-Boosted Security Types for Low-Level MPC
Journal:
arXiv
Published Date:
Jan 29, 2025
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.
