{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T12:35:10Z","timestamp":1770294910996,"version":"3.49.0"},"publisher-location":"Cham","reference-count":45,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783031131844","type":"print"},{"value":"9783031131851","type":"electronic"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2022,8,7]],"date-time":"2022-08-07T00:00:00Z","timestamp":1659830400000},"content-version":"vor","delay-in-days":218,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>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 variables secret only for these which are to be protected. However, in practice, it is usually 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\u2014but sometimes conservative\u2014security 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 symbolic reasoning are fed back to type inference to refine the security types even further. We implement our approach in a new tool <jats:bold>PoS4MPC<\/jats:bold>. Experimental results on five typical MPC applications confirm the efficacy of our approach.<\/jats:p>","DOI":"10.1007\/978-3-031-13185-1_19","type":"book-chapter","created":{"date-parts":[[2022,8,6]],"date-time":"2022-08-06T19:29:09Z","timestamp":1659814149000},"page":"385-406","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["PoS4MPC: Automated Security Policy Synthesis for\u00a0Secure Multi-party Computation"],"prefix":"10.1007","author":[{"given":"Yuxin","family":"Fan","sequence":"first","affiliation":[]},{"given":"Fu","family":"Song","sequence":"additional","affiliation":[]},{"given":"Taolue","family":"Chen","sequence":"additional","affiliation":[]},{"given":"Liangfeng","family":"Zhang","sequence":"additional","affiliation":[]},{"given":"Wanwei","family":"Liu","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2022,8,7]]},"reference":[{"key":"19_CR1","unstructured":"The LLVM compiler infrastructure. https:\/\/llvm.org"},{"key":"19_CR2","unstructured":"The source code of our benchmarks (2022). https:\/\/github.com\/SPoS4\/PoS4MPC"},{"key":"19_CR3","doi-asserted-by":"crossref","unstructured":"Almeida, J.B., Barbosa, M., Barthe, G., Pacheco, H., Pereira, V., Portela, B.: Enforcing ideal-world leakage bounds in real-world secret sharing MPC frameworks. In: CSF, pp. 132\u2013146 (2018)","DOI":"10.1109\/CSF.2018.00017"},{"key":"19_CR4","doi-asserted-by":"crossref","unstructured":"Amtoft, T., Bandhakavi, S., Banerjee, A.: A logic for information flow in object-oriented programs. In: POPL, pp. 91\u2013102 (2006)","DOI":"10.1145\/1111320.1111046"},{"key":"19_CR5","doi-asserted-by":"crossref","unstructured":"Andreea, I.: Private set intersection: past, present and future. In: SECRYPT, pp. 680\u2013685 (2021)","DOI":"10.5220\/0010525800002998"},{"key":"19_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"84","DOI":"10.1007\/978-3-662-53413-7_5","volume-title":"Static Analysis","author":"G Balatsouras","year":"2016","unstructured":"Balatsouras, G., Smaragdakis, Y.: Structure-sensitive points-to analysis for C and C++. In: Rival, X. (ed.) SAS 2016. LNCS, vol. 9837, pp. 84\u2013104. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-53413-7_5"},{"key":"19_CR7","doi-asserted-by":"crossref","unstructured":"Beaver, D., Micali, S., Rogaway, P.: The round complexity of secure protocols. In: STOC, pp. 503\u2013513 (1990)","DOI":"10.1145\/100216.100287"},{"key":"19_CR8","doi-asserted-by":"crossref","unstructured":"Ben-David, A., Nisan, N., Pinkas, B.: FairplayMP: a system for secure multi-party computation. In: CCS, pp. 257\u2013266 (2008)","DOI":"10.1145\/1455770.1455804"},{"key":"19_CR9","doi-asserted-by":"crossref","unstructured":"B\u00fcscher, N., Demmler, D., Katzenbeisser, S., Kretzmer, D., Schneider, T.: HyCC: compilation of hybrid protocols for practical secure computation. In: CCS, pp. 847\u2013861 (2018)","DOI":"10.1145\/3243734.3243786"},{"key":"19_CR10","unstructured":"Cadar, C., Dunbar, D., Engler, D.R.: KLEE: unassisted and automatic generation of high-coverage tests for complex systems programs. In: OSDI, pp. 209\u2013224 (2008)"},{"key":"19_CR11","doi-asserted-by":"crossref","unstructured":"Chen, J., Feng, Y., Dillig, I.: Precise detection of side-channel vulnerabilities using quantitative cartesian hoare logic. In: CCS, pp. 875\u2013890 (2017)","DOI":"10.1145\/3133956.3134058"},{"issue":"7","key":"19_CR12","doi-asserted-by":"publisher","first-page":"504","DOI":"10.1145\/359636.359712","volume":"20","author":"DE Denning","year":"1977","unstructured":"Denning, D.E., Denning, P.J.: Certification of programs for secure information flow. Commun. ACM 20(7), 504\u2013513 (1977)","journal-title":"Commun. ACM"},{"key":"19_CR13","unstructured":"Doerner, J.: The absentminded crypto kit. https:\/\/bitbucket.org\/jackdoerner\/absentminded-crypto-kit\/"},{"issue":"2\u20133","key":"19_CR14","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1561\/3300000019","volume":"2","author":"D Evans","year":"2018","unstructured":"Evans, D., Kolesnikov, V., Rosulek, M.: A pragmatic introduction to secure multi-party computation. Found. Trends Priv. Secur. 2(2\u20133), 70\u2013246 (2018)","journal-title":"Found. Trends Priv. Secur."},{"key":"19_CR15","doi-asserted-by":"crossref","unstructured":"Fan, Y., Song, F., Chen, T., Zhang, L., Liu, W.: Pos4mpc: automated security policy synthesis for secure multi-party computation. Technical report, ShanghaiTech University (2022). https:\/\/faculty.sist.shanghaitech.edu.cn\/faculty\/songfu\/publications\/CAV22full.pdf","DOI":"10.1007\/978-3-031-13185-1_19"},{"key":"19_CR16","doi-asserted-by":"crossref","unstructured":"Gao, P., Xie, H., Song, F., Chen, T.: A hybrid approach to formal verification of higher-order masked arithmetic programs. ACM Trans. Softw. Eng. Methodol. 30(3), 26:1\u201326:42 (2021)","DOI":"10.1145\/3428015"},{"issue":"3","key":"19_CR17","first-page":"973","volume":"48","author":"P Gao","year":"2022","unstructured":"Gao, P., Xie, H., Sun, P., Zhang, J., Song, F., Chen, T.: Formal verification of masking countermeasures for arithmetic programs. IEEE Trans. Softw. Eng. 48(3), 973\u20131000 (2022)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"19_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1007\/978-3-030-17462-0_9","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"P Gao","year":"2019","unstructured":"Gao, P., Xie, H., Zhang, J., Song, F., Chen, T.: Quantitative verification of masked arithmetic programs against side-channel attacks. In: Vojnar, T., Zhang, L. (eds.) TACAS 2019. LNCS, vol. 11427, pp. 155\u2013173. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-17462-0_9"},{"key":"19_CR19","doi-asserted-by":"crossref","unstructured":"Gao, P., Zhang, J., Song, F., Wang, C.: Verifying and quantifying side-channel resistance of masked software implementations. ACM Trans. Softw. Eng. Methodol. 28(3), 16:1\u201316:32 (2019)","DOI":"10.1145\/3330392"},{"issue":"3","key":"19_CR20","doi-asserted-by":"publisher","first-page":"431","DOI":"10.1145\/233551.233553","volume":"43","author":"O Goldreich","year":"1996","unstructured":"Goldreich, O., Ostrovsky, R.: Software protection and simulation on oblivious RAMs. J. ACM 43(3), 431\u2013473 (1996)","journal-title":"J. ACM"},{"key":"19_CR21","doi-asserted-by":"crossref","unstructured":"Hamada, K., Kikuchi, R., Ikarashi, D., Chida, K., Takahashi, K.: Practically efficient multi-party sorting protocols from comparison sort algorithms. In: ICISC, vol. 7839, pp. 202\u2013216 (2012)","DOI":"10.1007\/978-3-642-37682-5_15"},{"key":"19_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"169","DOI":"10.1007\/978-3-319-44618-9_9","volume-title":"Security and Cryptography for Networks","author":"B Hemenway","year":"2016","unstructured":"Hemenway, B., Lu, S., Ostrovsky, R., Welser IV, W.: High-precision secure computation of satellite collision probabilities. In: Zikas, V., De Prisco, R. (eds.) SCN 2016. LNCS, vol. 9841, pp. 169\u2013187. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-44618-9_9"},{"key":"19_CR23","doi-asserted-by":"crossref","unstructured":"Holzer, A., Franz, M., Katzenbeisser, S., Veith, H.: Secure two-party computations in ANSI C. In: CCS, pp. 772\u2013783 (2012)","DOI":"10.1145\/2382196.2382278"},{"key":"19_CR24","doi-asserted-by":"crossref","unstructured":"Keller, M.: MP-SPDZ: A versatile framework for multi-party computation. In: CCS, pp. 1575\u20131590 (2020)","DOI":"10.1145\/3372297.3417872"},{"key":"19_CR25","doi-asserted-by":"crossref","unstructured":"Kerschbaum, F.: Automatically optimizing secure computation. In: CCS, pp. 703\u2013714 (2011)","DOI":"10.1145\/2046707.2046786"},{"key":"19_CR26","doi-asserted-by":"crossref","unstructured":"Laud, P., Randmets, J.: A domain-specific language for low-level secure multiparty computation protocols. In: CCS, pp. 1492\u20131503 (2015)","DOI":"10.1145\/2810103.2813664"},{"key":"19_CR27","doi-asserted-by":"crossref","unstructured":"Li, P., Zdancewic, S.: Downgrading policies and relaxed noninterference. In: POPL, pp. 158\u2013170 (2005)","DOI":"10.1145\/1047659.1040319"},{"issue":"1","key":"19_CR28","doi-asserted-by":"publisher","first-page":"86","DOI":"10.1145\/3387108","volume":"64","author":"Y Lindell","year":"2021","unstructured":"Lindell, Y.: Secure multiparty computation. Commun. ACM 64(1), 86\u201396 (2021)","journal-title":"Commun. ACM"},{"key":"19_CR29","doi-asserted-by":"crossref","unstructured":"Liu, C., Wang, X.S., Nayak, K., Huang, Y., Shi, E.: ObliVM: a programming framework for secure computation. In: S &P, pp. 359\u2013376 (2015)","DOI":"10.1109\/SP.2015.29"},{"key":"19_CR30","doi-asserted-by":"crossref","unstructured":"Malacaria, P., Khouzani, M.H.R., Pasareanu, C.S., Phan, Q., Luckow, K.S.: Symbolic side-channel analysis for probabilistic programs. In: CSF, pp. 313\u2013327 (2018)","DOI":"10.1109\/CSF.2018.00030"},{"key":"19_CR31","unstructured":"Malkhi, D., Nisan, N., Pinkas, B., Sella, Y.: Fairplay - secure two-party computation system. In: USENIX Security Symposium, pp. 287\u2013302 (2004)"},{"key":"19_CR32","doi-asserted-by":"crossref","unstructured":"Mood, B., Gupta, D., Carter, H., Butler, K.R.B., Traynor, P.: Frigate: a validated, extensible, and efficient compiler and interpreter for secure computation. In: EuroS &P, pp. 112\u2013127 (2016)","DOI":"10.1109\/EuroSP.2016.20"},{"key":"19_CR33","doi-asserted-by":"crossref","unstructured":"Pasareanu, C.S., Kersten, R., Luckow, K.S., Phan, Q.: Chapter six - symbolic execution and recent applications to worst-case execution, load testing, and security analysis. Adv. Comput. 113, 289\u2013314 (2019)","DOI":"10.1016\/bs.adcom.2018.10.004"},{"key":"19_CR34","unstructured":"Patra, A., Schneider, T., Suresh, A., Yalame, H.: ABY2.0: improved mixed-protocol secure two-party computation. In: USENIX Security Symposium, pp. 2165\u20132182 (2021)"},{"key":"19_CR35","unstructured":"Poddar, R., Kalra, S., Yanai, A., Deng, R., Popa, R.A., Hellerstein, J.M.: Senate: a maliciously-secure MPC platform for collaborative analytics. In: USENIX Security Symposium, pp. 2129\u20132146 (2021)"},{"key":"19_CR36","unstructured":"Qin, Q., JiYang, J., Song, F., Chen, T., Xing, X.: Preventing timing side-channels via security-aware just-in-time compilation. CoRR abs\/2202.13134 (2022)"},{"key":"19_CR37","unstructured":"Schoenmakers, B.: MPyC: secure multiparty computation in Python (2020). https:\/\/github.com\/lschoe\/mpyc"},{"key":"19_CR38","doi-asserted-by":"crossref","unstructured":"Shamir, A.: How to share a secret. Commun. ACM 22(11), 612\u2013613 (1979)","DOI":"10.1145\/359168.359176"},{"key":"19_CR39","doi-asserted-by":"publisher","unstructured":"Terauchi, T., Aiken, A.: Secure information flow as a safety problem. In: Hankin, C., Siveroni, I. (eds.) SAS 2005. LNCS, vol. 3672, pp. 352\u2013367. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11547662_24","DOI":"10.1007\/11547662_24"},{"key":"19_CR40","doi-asserted-by":"crossref","unstructured":"Volpano, D.M., Irvine, C.E., Smith, G.: A sound type system for secure flow analysis. J. Comput. Secur. 4(2\/3), 167\u2013188 (1996)","DOI":"10.3233\/JCS-1996-42-304"},{"key":"19_CR41","unstructured":"Wagh, S., Gupta, D., Chandran, N.: SecureNN: efficient and private neural network training. IACR Cryptology ePrint Archive, p. 442 (2018)"},{"key":"19_CR42","doi-asserted-by":"publisher","unstructured":"Yang, W., Vizel, Y., Subramanyan, P., Gupta, A., Malik, S.: Lazy self-composition for security verification. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10982, pp. 136\u2013156. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-96142-2_11","DOI":"10.1007\/978-3-319-96142-2_11"},{"key":"19_CR43","doi-asserted-by":"crossref","unstructured":"Yao, A.C.: Protocols for secure computations. In: FOCS, pp. 160\u2013164 (1982)","DOI":"10.1109\/SFCS.1982.38"},{"key":"19_CR44","unstructured":"Zahur, S., Evans, D.: Obliv-C: a language for extensible data-oblivious computation. IACR Cryptology ePrint Archive, p. 1153 (2015)"},{"key":"19_CR45","doi-asserted-by":"publisher","unstructured":"Zhang, J., Gao, P., Song, F., Wang, C.: SCInfer: refinement-based verification of software countermeasures against side-channel attacks. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10982, pp. 157\u2013177. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-96142-2_12","DOI":"10.1007\/978-3-319-96142-2_12"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-13185-1_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,11,3]],"date-time":"2022-11-03T17:14:41Z","timestamp":1667495681000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-13185-1_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783031131844","9783031131851"],"references-count":45,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-13185-1_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"7 August 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Haifa","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Israel","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7 August 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"10 August 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"34","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/i-cav.org\/2022\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"209","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"40","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"11","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"19% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3.9","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"9.7","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}