信息學院宋富課題組提出安全多方計算程序的安全策略自動綜合方法

安全多方計算(MPC)是實現隱私保護的重要技術手段。它是指允許一組相互獨立的數據所有方在互不信任且不信任任何公開第三方的條件下，以各自的秘密為輸入聯合完成某個函數的計算。開發MPC程序需要實現MPC協議, 涉及到諸多密碼原理, 為了降低開發MPC程序的負擔, 幫助非密碼專業人員快速開發和部署MPC應用程序, 出現了許多封裝了MPC協議的MPC開發框架。

為了提高性能，近年來的MPC開發框架允許開發者利用秘密類型來指定需要保護的變量。然而在實踐中，指定秘密變量對非專家來說既困難又十分重要，聲明太多秘密變量會降低性能，聲明太少秘密變量則可能有泄露隱私的風險。如何幫助非密碼專家的開發人員開發既安全又高性能的MPC程序? 如何在不損害隱私保護能力的前提下，盡可能地聲明盡量少的秘密變量? 信息學院宋富課題組就這一問題展開了長期深入的研究，并取得了重要成果。

現有的秘密類型系統過于保守, 聲明秘密變量受到秘密類型系統的約束, 卻無視秘密類型系統的警告從而導致無法保證程序的隱私保護能力。為此研究團隊提出了一個集成類型推導和符號推理的安全策略自動綜合方法。該方法針對MPC公開計算結果的特點對MPC程序的信息泄露進行建模，并設計安全策略橋接MPC程序的信息泄露和MPC協議的信息泄露。兩方安全計算場景下的實驗結果顯示, 該方法減少了測試程序集在混淆電路協議中31%至1.56×10⁵%的執行時間，38%至3.61×10⁵%的電路尺寸，39%至4.17×10⁵%的通信比特數，以及在秘密共享協議中17%至2.5×10⁴%的執行時間。

圖|安全策略自動綜合系統的總體流程。圖中展示了該系統的示意流程，該系統接收一個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%。

此項工作由上?？萍即髮W主導，倫敦大學伯貝克學院和國防科技大學協作完成。信息學院研究生樊雨鑫為論文的第一作者，信息學院宋富教授位列第二作者和通訊作者。