Tags:Secure Multi-Party Computation, Security Policy, Security Verification and Synthesis
Abstract:
Secure multi-party computation (MPC) is a promising technique for privacy-persevering applications. A number of MPC frameworks have been proposed to reduce the burden of designing customized protocols, allowing non-experts to quickly develop and deploy MPC applications. To improve performance, recent MPC frameworks allow users to declare secret variables so that only these variables are to be protected. However, in practice, it could be highly non-trivial for non-experts to specify secret variables: declaring too many degrades the performance while declaring too less compromises privacy. To address this problem, in this work, we propose an automated security policy synthesis approach to declare as few secret variables as possible but without compromising security. Our approach is a synergistic integration of type inference and symbolic reasoning. The former is able to quickly infer a sound, but sometimes conservative, security policy, whereas the latter allows to identify secret variables in a security policy that can be declassified in a precise manner. Moreover, the results from the symbolic reasoning are fed back to type inference to refine the security types even further. We implement our approach in a tool, named PoS4MPC. Experimental results on five typical MPC applications confirm the efficacy of our approach.
PoS4MPC: Automated Security Policy Synthesis for Secure Multi-Party Computation