SMT-Boosted Security Types and Correctness for Low-Level MPC
The research introduces a new framework using Hoare logic and type theory to automatically verify correctness, confidentiality, and integrity in low-level Multi-Party Computation (MPC) protocols written in Prelude/Overture. By combining these formal methods with SMT solvers, the system enables compositional verification that enforces passive security (noninterference modulo output) and malicious security (integrity), offering a scalable way to ensure protocol properties.