安全多方计算(MPC)是实现隐私保护的重要技术手段。它是指允许一组相互独立的数据所有方在互不信任且不信任任何公开第三方的条件下，以各自的秘密为输入联合完成某个函数的计算。开发MPC程序需要实现MPC协议, 涉及到诸多密码原理, 为了降低开发MPC程序的负担, 帮助非密码专业人员快速开发和部署MPC应用程序, 出现了许多封装了MPC协议的MPC开发框架。
为了提高性能，近年来的MPC开发框架允许开发者利用秘密类型来指定需要保护的变量。然而在实践中，指定秘密变量对非专家来说既困难又十分重要，声明太多秘密变量会降低性能，声明太少秘密变量则可能有泄露隐私的风险。如何帮助非密码专家的开发人员开发既安全又高性能的MPC程序? 如何在不损害隐私保护能力的前提下，尽可能地声明尽量少的秘密变量? 信息学院宋富课题组就这一问题展开了长期深入的研究，并取得了重要成果。
现有的秘密类型系统过于保守, 声明秘密变量受到秘密类型系统的约束, 却无视秘密类型系统的警告从而导致无法保证程序的隐私保护能力。为此研究团队提出了一个集成类型推导和符号推理的安全策略自动综合方法。该方法针对MPC公开计算结果的特点对MPC程序的信息泄露进行建模，并设计安全策略桥接MPC程序的信息泄露和MPC协议的信息泄露。两方安全计算场景下的实验结果显示, 该方法减少了测试程序集在混淆电路协议中31%至1.56×105%的执行时间，38%至3.61×105%的电路尺寸，39%至4.17×105%的通信比特数，以及在秘密共享协议中17%至2.5×104%的执行时间。
图|安全策略自动综合系统的总体流程。图中展示了该系统的示意流程，该系统接收一个MPC程序，首先通过类型推导产生较为保守的安全策略，然后利用符号推理对安全策略中秘密变量进行降级产生更加高效的安全策略，并将此安全策略在MPC框架中实现，最后可得该框架编译产生的MPC可执行程序。
该成果日前以“PoS4MPC: Automated Security Policy Synthesis for Secure Multi-Party Computation”为题被第34届International Conference on Computer Aided Verification (CAV 2022)会议接受。CAV会议是中国计算机学会(CCF)推荐的A类国际学术会议，有三十余年历史，是计算机辅助验证领域的知名学术会议。2022年CAV会议的录用率约为26%。
此项工作由上海科技大学主导，伦敦大学伯贝克学院和国防科技大学协作完成。信息学院研究生樊雨鑫为论文的第一作者，信息学院宋富教授位列第二作者和通讯作者。
沪公网安备 31011502006855号