基于 SMT 的底层 MPC 安全类型与正确性验证

研究者提出一套新的 Hoare 逻辑与类型理论，用于自动验证 Prelude/Overture 语言框架所写协议的正确性、机密性与完整性。该分析的定义与自动化均借助 SMT 验证，兼顾精度与效率，方法具备可组合性与可扩展性，并可推广至任意素数域与秘密共享方案。