Security types and verification improve low-level multi-party protocols
SMT-Boosted Security Types and Correctness for Low-Level MPC
Cryptography and Security
Summary
Data privacy is crucial when multiple parties compute together without sharing secret information. The authors created a system that automatically checks both correctness and security of such protocols written in a specific programming framework. They use a mathematical tool called SMT verification to make this checking precise and fast. Their approach works in parts, scales well, and adapts to many types of secret sharing methods. This helps build safer protocols for distributed computing.
What this means in practice
- •For distributed system engineers: Verify and enforce security and correctness guarantees automatically when building low-level multi-party computation protocols.
- •For cryptography software developers: Build reliable cryptographic protocols that maintain privacy and correctness over various secret sharing schemes using automated SMT checks.
Authors
Christian Skalka, Steven Baldasty, Yeonhee Yeh, Felix Walberg, Joseph P. Near
Abstract
Secure Multi-Party Computation (MPC) is an important enabling technology for data privacy in modern distributed applications. We develop a new Hoare logic and type theory to automatically enforce correctness, confidentiality, and integrity properties of protocols written in the Prelude/Overture language framework. Both definition and automation of our analyses leverages SMT verification, supporting precision and efficiency. Our approach is compositional, scalable, and generalizes to arbitrary prime fields and secret sharing schemes.