Language-Based Security for Low-Level MPC
Article No.: 16, Pages 1 - 14
Abstract
Secure Multi-Party Computation (MPC) is an important enabling technology for data privacy in modern distributed applications. Currently, proof methods for low-level MPC protocols are primarily manual and thus tedious and error-prone, and are also non-standardized and unfamiliar to most PL theorists. As a step towards better language support and language-based enforcement, we develop a new staged PL for defining a variety of low-level probabilistic MPC protocols. We also formulate a collection of confidentiality and integrity hyperproperties for our language model that are familiar from information flow, including conditional noninterference, gradual release, and robust declassification. We demonstrate their relation to standard MPC threat models of passive and malicious security, and how they can be leveraged in security verification of protocols. To prove these properties we develop automated tactics in <Formula format="inline"><TexMath><?TeX $\mathbb {F}_2$?></TexMath><AltText>Math 1</AltText><File name="ppdp2024-14-inline1" type="svg"/></Formula> that can be integrated with separation logic-style reasoning.
References
[1]
Martin Abadi and Phillip Rogaway. 2000. Reconciling Two Views of Cryptography. In Theoretical Computer Science: Exploring New Frontiers of Theoretical Informatics, Jan van Leeuwen, Osamu Watanabe, Masami Hagiya, Peter D. Mosses, and Takayasu Ito (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 3–22.
[2]
C. Acay, J. Gancher, R. Recto, and A. Myers. 2024. Secure Synthesis of Distributed Cryptographic Applications. In 2024 IEEE 37th Computer Security Foundations Symposium (CSF). IEEE Computer Society, Los Alamitos, CA, USA, 315–330. https://doi.org/10.1109/CSF61375.2024.00021
[3]
Coşku Acay, Rolph Recto, Joshua Gancher, Andrew C. Myers, and Elaine Shi. 2021. Viaduct: An Extensible, Optimizing Compiler for Secure Distributed Programs. In Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation (Virtual, Canada) (PLDI 2021). Association for Computing Machinery, New York, NY, USA, 740–755. https://doi.org/10.1145/3453483.3454074
[4]
Aws Albarghouthi, Loris D’Antoni, Samuel Drews, and Aditya V Nori. 2017. Fairsquare: probabilistic verification of program fairness. Proceedings of the ACM on Programming Languages 1, OOPSLA (2017), 1–30.
[5]
José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Hugo Pacheco, Vitor Pereira, and Bernardo Portela. 2018. Enforcing ideal-world leakage bounds in real-world secret sharing MPC frameworks. In 2018 IEEE 31st Computer Security Foundations Symposium (CSF). IEEE, 132–146.
[6]
Aslan Askarov and Andrei Sabelfeld. 2007. Gradual Release: Unifying Declassification, Encryption and Key Release Policies. In 2007 IEEE Symposium on Security and Privacy (SP ’07). 207–221. https://doi.org/10.1109/SP.2007.22
[7]
Yaniv Aspis. 2018. A Linear Algebraic Approach to Logic Programming. Ph. D. Dissertation. Master thesis at Imperial College London.
[8]
Gilles Barthe, Justin Hsu, and Kevin Liao. 2019. A probabilistic separation logic. Proc. ACM Program. Lang. 4, POPL, Article 55 (dec 2019), 30 pages. https://doi.org/10.1145/3371123
[9]
Rikke Bendlin, Ivan Damgård, Claudio Orlandi, and Sarah Zakarias. 2011. Semi-homomorphic Encryption and Multiparty Computation. In Advances in Cryptology – EUROCRYPT 2011, Kenneth G. Paterson (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 169–188.
[10]
Eli Bingham, Jonathan P Chen, Martin Jankowiak, Fritz Obermeyer, Neeraj Pradhan, Theofanis Karaletsos, Rohit Singh, Paul Szerlip, Paul Horsfall, and Noah D Goodman. 2019. Pyro: Deep universal probabilistic programming. The Journal of Machine Learning Research 20, 1 (2019), 973–978.
[11]
Dan Bogdanov, Peeter Laud, and Jaak Randmets. 2014. Domain-Polymorphic Programming of Privacy-Preserving Applications. In Proceedings of the Ninth Workshop on Programming Languages and Analysis for Security (Uppsala, Sweden) (PLAS’14). Association for Computing Machinery, New York, NY, USA, 53–65. https://doi.org/10.1145/2637113.2637119
[12]
Chris Brzuska and Sabine Oechsner. 2023. A State-Separating Proof for Yao’s Garbling Scheme. In Proceedings - 2023 IEEE 36th Computer Security Foundations Symposium, CSF 2023(Proceedings - IEEE Computer Security Foundations Symposium). IEEE Computer Society, 137–152. https://doi.org/10.1109/CSF57540.2023.00009 36th IEEE Computer Security Foundations Symposium, CSF 2023 ; Conference date: 09-07-2023 Through 13-07-2023.
[13]
Bob Carpenter, Andrew Gelman, Matthew D Hoffman, Daniel Lee, Ben Goodrich, Michael Betancourt, Marcus A Brubaker, Jiqiang Guo, Peter Li, and Allen Riddell. 2017. Stan: A probabilistic programming language. Journal of statistical software 76 (2017).
[14]
Michael R. Clarkson and Fred B. Schneider. 2010. Hyperproperties. J. Comput. Secur. 18, 6 (sep 2010), 1157–1210.
[15]
Ivan Damgård and Claudio Orlandi. 2010. Multiparty Computation for Dishonest Majority: From Passive to Active Security at Low Cost. In Advances in Cryptology – CRYPTO 2010, Tal Rabin (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 558–576.
[16]
Ivan Damgård, Valerio Pastro, Nigel Smart, and Sarah Zakarias. 2012. Multiparty Computation from Somewhat Homomorphic Encryption. In Advances in Cryptology – CRYPTO 2012, Reihaneh Safavi-Naini and Ran Canetti (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 643–662.
[17]
David Darais, Ian Sweet, Chang Liu, and Michael Hicks. 2019. A language for probabilistically oblivious computation. Proceedings of the ACM on Programming Languages 4, POPL (2019), 1–31.
[18]
Luc De Raedt, Angelika Kimmig, and Hannu Toivonen. 2007. ProbLog: A probabilistic Prolog and its application in link discovery. In IJCAI 2007, Proceedings of the 20th international joint conference on artificial intelligence. IJCAI-INT JOINT CONF ARTIF INTELL, 2462–2467.
[19]
David Evans, Vladimir Kolesnikov, Mike Rosulek, 2018. A pragmatic introduction to secure multi-party computation. Foundations and Trends® in Privacy and Security 2, 2-3 (2018), 70–246.
[20]
Shang Gao, Zhe Peng, Feng Tan, Yuanqing Zheng, and Bin Xiao. 2022. SymmeProof: Compact zero-knowledge argument for blockchain confidential transactions. IEEE Transactions on Dependable and Secure Computing (2022).
[21]
Oded Goldreich, Silvio Micali, and Avi Wigderson. 2019. How to play any mental game, or a completeness theorem for protocols with honest majority. In Providing Sound Foundations for Cryptography: On the Work of Shafi Goldwasser and Silvio Micali. 307–328.
[22]
H. Haagh, A. Karbyshev, S. Oechsner, B. Spitters, and P. Strub. 2018. Computer-Aided Proofs for Multiparty Computation with Active Security. In 2018 IEEE 31st Computer Security Foundations Symposium (CSF). IEEE Computer Society, Los Alamitos, CA, USA, 119–131. https://doi.org/10.1109/CSF.2018.00016
[23]
Steven Holtzen, Guy Van den Broeck, and Todd Millstein. 2020. Scaling exact inference for discrete probabilistic programs. Proceedings of the ACM on Programming Languages 4, OOPSLA (2020), 1–31.
[24]
Sebastian Hunt, David Sands, and Sandro Stucki. 2023. Reconciling Shannon and Scott with a Lattice of Computable Information. Proc. ACM Program. Lang. 7, POPL, Article 68 (jan 2023), 30 pages. https://doi.org/10.1145/3571740
[25]
Yuval Ishai, Eyal Kushilevitz, Rafail Ostrovsky, and Amit Sahai. 2009. Zero-knowledge proofs from secure multiparty computation. SIAM J. Comput. 39, 3 (2009), 1121–1152.
[26]
Brian Knott, Shobha Venkataraman, Awni Hannun, Shubho Sengupta, Mark Ibrahim, and Laurens van der Maaten. 2021. Crypten: Secure multi-party computation meets machine learning. Advances in Neural Information Processing Systems 34 (2021), 4961–4973.
[27]
Karl Koch, Stephan Krenn, Donato Pellegrino, and Sebastian Ramacher. 2020. Privacy-preserving analytics for data markets using MPC. In IFIP International Summer School on Privacy and Identity Management. Springer, 226–246.
[28]
John M Li, Amal Ahmed, and Steven Holtzen. 2023. Lilac: a Modal Separation Logic for Conditional Probability. Proceedings of the ACM on Programming Languages 7, PLDI (2023), 148–171.
[29]
Xiling Li, Rafael Dowsley, and Martine De Cock. 2021. Privacy-preserving feature selection with secure multiparty computation. In International Conference on Machine Learning. PMLR, 6326–6336.
[30]
Yehuda Lindell. 2017. How to Simulate It – A Tutorial on the Simulation Proof Technique. Springer International Publishing, Cham, 277–346. https://doi.org/10.1007/978-3-319-57048-8_6
[31]
Jun Liu, Yuan Tian, Yu Zhou, Yang Xiao, and Nirwan Ansari. 2020. Privacy preserving distributed data mining based on secure multi-party computation. Computer Communications 153 (2020), 208–216.
[32]
Donghang Lu, Thomas Yurek, Samarth Kulshreshtha, Rahul Govind, Aniket Kate, and Andrew Miller. 2019. Honeybadgermpc and asynchromix: Practical asynchronous mpc and its application to anonymous communication. In Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security. 887–903.
[33]
Dahlia Malkhi, Noam Nisan, Benny Pinkas, and Yaron Sella. 2004. Fairplay—A Secure Two-Party Computation System. In 13th USENIX Security Symposium (USENIX Security 04). USENIX Association, San Diego, CA. https://www.usenix.org/conference/13th-usenix-security-symposium/fairplay-secure-two-party-computation-system
[34]
John C. Mitchell, Rahul Sharma, Deian Stefan, and Joe Zimmerman. 2012. Information-Flow Control for Programming on Encrypted Data. In 2012 IEEE 25th Computer Security Foundations Symposium. 45–60. https://doi.org/10.1109/CSF.2012.30
[35]
Emmanuela Orsini. 2021. Efficient, Actively Secure MPC with a Dishonest Majority: A Survey. In Arithmetic of Finite Fields, Jean Claude Bajard and Alev Topuzoğlu (Eds.). Springer International Publishing, Cham, 42–71.
[36]
Avi Pfeffer. 2009. Figaro: An object-oriented probabilistic programming language. Charles River Analytics Technical Report 137, 96 (2009), 4.
[37]
Aseem Rastogi, Matthew A Hammer, and Michael Hicks. 2014. Wysteria: A programming language for generic, mixed-mode multiparty computations. In 2014 IEEE Symposium on Security and Privacy. IEEE, 655–670.
[38]
Aseem Rastogi, Nikhil Swamy, and Michael Hicks. 2019. Wys*: A DSL for Verified Secure Multi-party Computations. In 8th International Conference on Principles of Security and Trust (POST)(Lecture Notes in Computer Science, Vol. 11426), Flemming Nielson and David Sands (Eds.). Springer, 99–122. https://doi.org/10.1007/978-3-030-17138-4_5
[39]
Feras A Saad, Martin C Rinard, and Vikash K Mansinghka. 2021. SPPL: probabilistic programming with fast exact symbolic inference. In Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation. 804–819.
[40]
Andrei Sabelfeld and David Sands. 2009. Declassification: Dimensions and Principles. J. Comput. Secur. 17, 5 (oct 2009), 517–548.
[41]
Chiaki Sakama, Katsumi Inoue, and Taisuke Sato. 2017. Linear algebraic characterization of logic programs. In Knowledge Science, Engineering and Management: 10th International Conference, KSEM 2017, Melbourne, VIC, Australia, August 19-20, 2017, Proceedings 10. Springer, 520–533.
[42]
Walid Taha and Tim Sheard. 2000. MetaML and multi-stage programming with explicit annotations. Theoretical Computer Science 248, 1 (2000), 211–242. https://doi.org/10.1016/S0304-3975(00)00053-0 PEPM’97.
[43]
Antonio Emerson Barros Tomaz, Jose Claudio Do Nascimento, Abdelhakim Senhaji Hafid, and Jose Neuman De Souza. 2020. Preserving privacy in mobile health systems using non-interactive zero-knowledge proof and blockchain. IEEE access 8 (2020), 204441–204458.
[44]
Frank Wood, Jan Willem Meent, and Vikash Mansinghka. 2014. A new approach to probabilistic programming inference. In Artificial intelligence and statistics. PMLR, 1024–1032.
[45]
Qianchuan Ye and Benjamin Delaware. 2022. Oblivious Algebraic Data Types. Proc. ACM Program. Lang. 6, POPL, Article 51 (jan 2022), 29 pages. https://doi.org/10.1145/3498713
[46]
S. Zdancewic and A.C. Myers. 2001. Robust declassification. In Proceedings. 14th IEEE Computer Security Foundations Workshop, 2001.15–23. https://doi.org/10.1109/CSFW.2001.930133
Index Terms
- Language-Based Security for Low-Level MPC
Recommendations
On the Communication Efficiency of Statistically Secure Asynchronous MPC with Optimal Resilience
AbstractSecure multi-party computation (MPC) is a fundamental problem in secure distributed computing. An MPC protocol allows a set of n mutually distrusting parties with private inputs to securely compute any publicly known function of their inputs, by ...
Revised Report on the Algorithmic Language Scheme
The report gives a defining description of the programming language Scheme. Scheme is a statically scoped and properly tail-recursive dialect of the Lisp programming language invented by Guy Lewis Steele, Jr. and Gerald Jay Sussman. It was designed to have ...
Two-Thirds Honest-Majority MPC for Malicious Adversaries at Almost the Cost of Semi-Honest
CCS '19: Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications SecuritySecure multiparty computation (MPC) enables a set of parties to securely carry out a joint computation of their private inputs without revealing anything but the output. Protocols for semi-honest adversaries guarantee security as long as the corrupted ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
September 2024
219 pages
ISBN:9798400709692
DOI:10.1145/3678232
Copyright © 2024 Owner/Author.
This work is licensed under a Creative Commons Attribution International 4.0 License.
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 09 September 2024
Check for updates
Author Tags
Qualifiers
- Research-article
- Research
- Refereed limited
Conference
PPDP 2024
PPDP 2024: 26th International Symposium on Principles and Practice of Declarative Programming
September 9 - 11, 2024
Milano, Italy
Acceptance Rates
Overall Acceptance Rate 230 of 486 submissions, 47%
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 98Total Downloads
- Downloads (Last 12 months)98
- Downloads (Last 6 weeks)60
Reflects downloads up to 25 Nov 2024
Other Metrics
Citations
View Options
View options
View or Download as a PDF file.
PDFeReader
View online with eReader.
eReaderHTML Format
View this article in HTML Format.
HTML FormatLogin options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in