research-article

Open access

Viaduct: an extensible, optimizing compiler for secure distributed programs

Authors:

Joshua Gancher,

Andrew C. Myers,

Elaine ShiAuthors Info & Claims

PLDI 2021: Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation

Pages 740 - 755

https://doi.org/10.1145/3453483.3454074

Published: 18 June 2021 Publication History

Abstract

Modern distributed systems involve interactions between principals with limited trust, so cryptographic mechanisms are needed to protect confidentiality and integrity. At the same time, most developers lack the training to securely employ cryptography. We present Viaduct, a compiler that transforms high-level programs into secure, efficient distributed realizations. Viaduct's source language allows developers to declaratively specify security policies by annotating their programs with information flow labels. The compiler uses these labels to synthesize distributed programs that use cryptography efficiently while still defending the source-level security policy. The Viaduct approach is general, and can be easily extended with new security mechanisms.

Our implementation of the Viaduct compiler comes with an extensible runtime system that includes plug-in support for multiparty computation, commitments, and zero-knowledge proofs. We have evaluated the system on a set of benchmarks, and the results indicate that our approach is feasible and can use cryptography in efficient, nontrivial ways.

References

[1]

[n.d.]. https://github.com/scipr-lab/libsnark.

[2]

Coşku Acay, Rolph Recto, Joshua Gancher, Andrew Myers, and Elaine Shi. 2021. Viaduct: An Extensible, Optimizing Compiler for Secure Distributed Programs (Technical Report). https://eprint.iacr.org/2021/468

[3]

Abdelrahaman Aly, Daniele Cozzo, Marcel Keller, Emmanuela Orsini, Dragos Rotaru, Peter Scholl, Nigel P. Smart, and Tim Wood. 2019. SCALE–MAMBA v1.6 : Documentation. https://homes.esat.kuleuven.be/~nsmart/SCALE

[4]

Owen Arden, Jed Liu, and Andrew C. Myers. 2015. Flow-Limited Authorization. In 28superscript th IEEE Computer Security Foundations Symp. (CSF). 569–583. https://doi.org/10.1109/CSF.2015.42

Digital Library

[5]

Peter Bogetoft, Dan Lund Christensen, Ivan Damgård, Martin Geisler, Thomas Jakobsen, Mikkel Krøigaard, Janus Dam Nielsen, Jesper Buus Nielsen, Kurt Nielsen, Jakob Pagter, Michael Schwartzbach, and Tomas Toft. 2009. Financial Cryptography and Data Security. Springer-Verlag, Berlin, Heidelberg. 325–343. isbn:978-3-642-03548-7 https://doi.org/10.1007/978-3-642-03549-4_20

Digital Library

[6]

Niklas Broberg, Bart van Delft, and David Sands. 2013. Paragon for Practical Programming with Information-Flow Control. In 11superscript th ASIAN Symposium on Programming Languages and Systems, APLAS 2013. 217–232. https://doi.org/10.1007/978-3-319-03542-0_16

Digital Library

[7]

Niklas Büscher, Daniel Demmler, Stefan Katzenbeisser, David Kretzmer, and Thomas Schneider. 2018. HyCC: Compilation of Hybrid Protocols for Practical Secure Computation. In 25superscript th ACM Conf. on Computer and Communications Security (CCS). ACM, New York, NY, USA. 847–861. isbn:9781450356930 https://doi.org/10.1145/3243734.3243786

Digital Library

[8]

Ran Canetti. 2000. Security and Composition of Multiparty Cryptographic Protocols. Journal of Cryptology, 143–202. https://doi.org/10.1007/s001459910006

Digital Library

[9]

Ran Canetti. 2001. Universally Composable Security: A New Paradigm for Cryptographic Protocols. In 42superscript nd Annual IEEE Symposium on Foundations of Computer Science. 136–145. https://doi.org/10.1109/SFCS.2001.959888

[10]

Ran Canetti, Yehuda Lindell, Rafail Ostrovsky, and Amit Sahai. 2002. Universally composable two-party and multi-party secure computation. In 34superscript th Annual ACM Symposium on Theory of Computing. ACM, 494–503. https://doi.org/10.1145/509907.509980

Digital Library

[11]

Ethan Cecchetti, Andrew C. Myers, and Owen Arden. 2017. Nonmalleable Information Flow Control. In 24superscript th ACM Conf. on Computer and Communications Security (CCS). ACM, 1875–1891. https://doi.org/10.1145/3133956.3134054

Digital Library

[12]

Hao Chen, Kim Laine, and Peter Rindal. 2017. Fast Private Set Intersection from Homomorphic Encryption. In 24superscript th ACM Conf. on Computer and Communications Security (CCS), Bhavani M. Thuraisingham, David Evans, Tal Malkin, and Dongyan Xu (Eds.). 1243–1255. https://doi.org/10.1145/3133956.3134061

Digital Library

[13]

Craig Costello, Cédric Fournet, Jon Howell, Markulf Kohlweiss, Benjamin Kreuter, Michael Naehrig, Bryan Parno, and Samee Zahur. 2015. Geppetto: Versatile verifiable computation. In IEEE Symp. on Security and Privacy. IEEE, 253–270. https://doi.org/10.1109/SP.2015.23

Digital Library

[14]

Leonardo de Moura and Nikolaj Bjørner. 2008. Z3: an efficient SMT solver. In Proceedings of the Theory and Practice of Software, 14th Int’l Conf. on Tools and Algorithms for the Construction and Analysis of Systems. Springer-Verlag, Berlin, Heidelberg. 337–340. isbn:3540787992 https://doi.org/10.1007/978-3-540-78800-3_24

[15]

Christian Decker and Roger Wattenhofer. 2014. Bitcoin transaction malleability and MtGox. In 19superscript th European Symposium on Research in Computer Security. Springer, 313–326. https://doi.org/10.1007/978-3-319-11212-1_18

Digital Library

[16]

Daniel Demmler, Thomas Schneider, and Michael Zohner. 2015. ABY - A Framework for Efficient Mixed-Protocol Secure Two-Party Computation. In Network and Distributed System Security Symp. The Internet Society. https://doi.org/10.14722/ndss.2015.23113

[17]

Manuel Egele, David Brumley, Yanick Fratantonio, and Christopher Kruegel. 2013. An Empirical Study of Cryptographic Misuse in Android Applications. In ACM Conf. on Computer and Communications Security (CCS). 73–84. http://doi.acm.org/10.1145/2508859.2516693

Digital Library

[18]

Cormac Flanagan, Amr Sabry, Bruce F. Duba, and Matthias Felleisen. 1993. The Essence of Compiling With Continuations. In ACM SIGPLAN Conf. on Programming Language Design and Implementation (PLDI) (PLDI ’93). 237–247. isbn:0-89791-598-4 https://doi.org/10.1145/155090.155113

Digital Library

[19]

Cédric Fournet, Guervan le Guernic, and Tamara Rezk. 2009. A Security-Preserving Compiler for Distributed Programs: From Information-Flow Policies to Cryptographic Mechanisms. In 16superscript th ACM Conf. on Computer and Communications Security (CCS). 432–441. https://doi.org/10.1145/1653662.1653715

Digital Library

[20]

Cédric Fournet and Tamara Rezk. 2008. Cryptographically sound implementations for typed information-flow security. In 35superscript th ACM Symp. on Principles of Programming Languages (POPL). 323–335. https://doi.org/10.1145/1328438.1328478

Digital Library

[21]

2016. General Data Protection Regulation. https://gdpr-info.eu

[22]

Martin Georgiev, Subodh Iyengar, Suman Jana, Rishita Anubhai, Dan Boneh, and Vitaly Shmatikov. 2012. The most dangerous code in the world: validating SSL certificates in non-browser software. In 19superscript th ACM Conf. on Computer and Communications Security (CCS), Ting Yu, George Danezis, and Virgil D. Gligor (Eds.). ACM, 38–49. https://doi.org/10.1145/2382196.2382204

Digital Library

[23]

Joseph A. Goguen and Jose Meseguer. 1982. Security Policies and Security Models. In IEEE Symp. on Security and Privacy. 11–20. https://doi.org/10.1109/SP.1982.10014

[24]

Oded Goldreich, Silvio Micali, and Avi Wigderson. 1987. How to Play any Mental Game. In 19superscript th Annual ACM Symposium on Theory of Computing, Alfred V. Aho (Ed.). 218–229. https://doi.org/10.1145/28395.28420

Digital Library

[25]

Anitha Gollamudi, Stephen Chong, and Owen Arden. 2019. Information Flow Control for Distributed Trusted Execution Environments. In 32superscript nd IEEE Computer Security Foundations Symp. (CSF). IEEE, 304–318. https://doi.org/10.1109/CSF.2019.00028

[26]

S. Dov Gordon, Feng-Hao Liu, and Elaine Shi. 2015. Constant-Round MPC with Fairness and Guarantee of Output Delivery. 63–82 pages. https://doi.org/10.1007/978-3-662-48000-7_4

Digital Library

[27]

Marcella Hastings, Brett Hemenway, Daniel Noble, and Steve Zdancewic. 2019. SoK: General Purpose Compilers for Secure Multi-Party Computation. In IEEE Symp. on Security and Privacy. 1220–1237. https://doi.org/10.1109/SP.2019.00028

[28]

Muhammad Ishaq, Ana Milanova, and Vassilis Zikas. 2019. Efficient MPC via Program Analysis: A Framework for Efficient Optimal Mixing. In 26superscript th ACM Conf. on Computer and Communications Security (CCS). ACM, 1539–1556. https://doi.org/10.1145/3319535.3339818

Digital Library

[29]

David Kaplan, Jeremy Powell, and Tom Woller. 2016. AMD memory encryption.

[30]

Florian Kerschbaum. 2011. Automatically Optimizing Secure Computation. In 18superscript th ACM Conf. on Computer and Communications Security (CCS). isbn:978-1-4503-0948-6 https://doi.org/10.1145/2046707.2046786

Digital Library

[31]

Ahmed Kosba, Charalampos Papamanthou, and Elaine Shi. 2018. xJsnark: A Framework for Efficient Verifiable Computation. In IEEE Symp. on Security and Privacy. IEEE, 944–961. https://doi.org/10.1109/SP.2018.00018

[32]

Chang Liu, Yan Huang, Elaine Shi, Jonathan Katz, and Michael Hicks. 2014. Automating efficient RAM-model secure computation. In IEEE Symp. on Security and Privacy. IEEE, 623–638. https://doi.org/10.1109/SP.2014.46

Digital Library

[33]

Chang Liu, Xiao Shaun Wang, Kartik Nayak, Yan Huang, and Elaine Shi. 2015. ObliVM: A Programming Framework for Secure Computation. In 25superscript th ACM Symp. on Operating System Principles (SOSP). IEEE, 359–376. https://doi.org/10.1109/SP.2015.29

Digital Library

[34]

Dahlia Malkhi, Noam Nisan, Benny Pinkas, and Yaron Sella. 2004. Fairplay - A Secure Two-Party Computation System. In 13superscript th Usenix Security Symposium. 287–302. http://www.usenix.org/publications/library/proceedings/sec04/tech/malkhi.html

[35]

Frank McKeen, Ilya Alexandrovich, Alex Berenzon, Carlos Rozas, Hisham Shafi, Vedvyas Shanbhogue, and Uday Savagaonkar. 2013. Innovative Instructions and Software Model for Isolated Execution. In Workshop on Hardware and Architectural Support for Security and Privacy. https://doi.org/10.1145/2487726.2488368

Digital Library

[36]

Andrew C. Myers. 1999. JFlow: Practical Mostly-Static Information Flow Control. In 26superscript th ACM Symp. on Principles of Programming Languages (POPL). 228–241. https://doi.org/10.1145/292540.292561

Digital Library

[37]

Bryan Parno, Jon Howell, Craig Gentry, and Mariana Raykova. 2013. Pinocchio: Nearly practical verifiable computation. In IEEE Symp. on Security and Privacy. IEEE, 238–252. https://doi.org/10.1109/SP.2013.47

Digital Library

[38]

Benny Pinkas, Mike Rosulek, Ni Trieu, and Avishay Yanai. 2019. SpOT-Light: Lightweight Private Set Intersection from Sparse OT Extension. In Advances in Cryptology – CRYPTO 2019. Springer, 401–431. https://doi.org/10.1007/978-3-030-26954-8_13

Digital Library

[39]

François Pottier and Vincent Simonet. 2002. Information flow inference for ML. In 29superscript th ACM Symp. on Principles of Programming Languages (POPL). 319–330. https://doi.org/10.1145/503272.503302

Digital Library

[40]

Aseem Rastogi, Matthew A. Hammer, and Michael Hicks. 2014. Wysteria: A Programming Language for Generic, Mixed-Mode Multiparty Computations. In IEEE Symp. on Security and Privacy. 655–670. https://doi.org/10.1109/SP.2014.48

Digital Library

[41]

Jakob Rehof and Torben Æ . Mogensen. 1996. Tractable Constraints in Finite Semilattices. In 3rd International Symposium on Static Analysis (Lecture Notes in Computer Science). Springer-Verlag, 285–300. https://doi.org/10.1007/3-540-61739-6_48

[42]

Daniel Edwin Rutherford. 1965. Introduction to Lattice Theory. Oliver and Boyd.

[43]

Andrei Sabelfeld and Andrew C. Myers. 2003. Language-Based Information-Flow Security. IEEE Journal on Selected Areas in Communications, 21, 1 (2003), Jan., 5–19. https://doi.org/10.1109/JSAC.2002.806121

Digital Library

[44]

Emil Stefanov, Marten van Dijk, Elaine Shi, Christopher W. Fletcher, Ling Ren, Xiangyao Yu, and Srinivas Devadas. 2013. Path ORAM: an extremely simple oblivious RAM protocol. In 20superscript th ACM Conf. on Computer and Communications Security (CCS), Ahmad-Reza Sadeghi, Virgil D. Gligor, and Moti Yung (Eds.). 299–310. https://doi.org/10.1145/2508859.2516660

Digital Library

[45]

Nikolaj Volgushev, Malte Schwarzkopf, Ben Getchell, Mayank Varia, Andrei Lapets, and Azer Bestavros. 2019. Conclave: secure multi-party computation on big data. In ACM SIGOPS/EuroSys European Conference on Computer Systems, George Candea, Robbert van Renesse, and Christof Fetzer (Eds.). 3:1–3:18. https://doi.org/10.1145/3302424.3303982

Digital Library

[46]

Riad S. Wahby, Srinath Setty, Zuocheng Ren, Andrew J. Blumberg, and Michael Walfish. 2015. Efficient RAM and Control Flow in Verifiable Outsourced Computation. In Network and Distributed System Security Symp. The Internet Society. https://doi.org/10.14722/ndss.2015.23097

[47]

Andrew C. Yao. 1982. Protocols for Secure Computations. In 23superscript rd annual IEEE Symposium on Foundations of Computer Science. 160–164. https://doi.org/10.1109/SFCS.1982.38

[48]

Drew Zagieboylo, G. Edward Suh, and Andrew C. Myers. 2019. Using Information Flow to Design an ISA that Controls Timing Channels. In 32superscript nd IEEE Computer Security Foundations Symp. (CSF). https://doi.org/10.1109/CSF.2019.00026

[49]

Samee Zahur and David Evans. 2015. Obliv-C: A Language for Extensible Data-Oblivious Computation. IACR Cryptol. ePrint Arch., http://eprint.iacr.org/2015/1153

[50]

Steve Zdancewic and Andrew C. Myers. 2001. Robust Declassification. In 14superscript th IEEE Computer Security Foundations Workshop (CSFW). 15–23. issn:1063-6900 https://doi.org/10.1109/CSFW.2001.930133

[51]

Steve Zdancewic, Lantian Zheng, Nathaniel Nystrom, and Andrew C. Myers. 2002. Secure Program Partitioning. ACM Trans. on Computer Systems, 20, 3 (2002), Aug., 283–328. https://doi.org/10.1145/566340.566343

Digital Library

[52]

Lantian Zheng, Stephen Chong, Andrew C. Myers, and Steve Zdancewic. 2003. Using Replication and Partitioning to Build Secure Distributed Systems. In IEEE Symp. on Security and Privacy. 236–250. https://doi.org/10.1109/SECPRI.2003.1199340

[53]

Lantian Zheng and Andrew C. Myers. 2005. End-to-End Availability Policies and Noninterference. In 18superscript th IEEE Computer Security Foundations Workshop (CSFW). 272–286. https://doi.org/10.1109/CSFW.2005.16

Digital Library

[54]

Lantian Zheng and Andrew C. Myers. 2014. A Language-Based Approach to Secure Quorum Replication. In 9superscript th ACM SIGPLAN Workshop on Programming Languages and Analysis for Security (PLAS). https://doi.org/10.1145/2637113.2637117

Digital Library

Cited By

Chen XHe SSun LZheng YWu C(2024)A Survey of Consortium Blockchain and Its ApplicationsCryptography10.3390/cryptography80200128:2(12)Online publication date: 22-Mar-2024
https://doi.org/10.3390/cryptography8020012
Skalka CNear J(2024)Language-Based Security for Low-Level MPCProceedings of the 26th International Symposium on Principles and Practice of Declarative Programming10.1145/3678232.3678246(1-14)Online publication date: 9-Sep-2024
https://dl.acm.org/doi/10.1145/3678232.3678246
Ye QDelaware B(2024)Taypsi: Static Enforcement of Privacy Policies for Policy-Agnostic Oblivious ComputationProceedings of the ACM on Programming Languages10.1145/36498618:OOPSLA1(1407-1436)Online publication date: 29-Apr-2024
https://dl.acm.org/doi/10.1145/3649861
Show More Cited By

Index Terms

Viaduct: an extensible, optimizing compiler for secure distributed programs
1. Security and privacy

Recommendations

The jastadd extensible java compiler
Proceedings of the 2007 OOPSLA conference

The JastAdd Extensible Java Compiler is a high quality Java compiler that is easy to extend in order to build static analysis tools for Java, and to extend Java with new language constructs. It is built modularly, with a Java 1.4 compiler that is ...
A Full Proof of the BGW Protocol for Perfectly Secure Multiparty Computation

In the setting of secure multiparty computation, a set of n parties with private inputs wish to jointly compute some functionality of their inputs. One of the most fundamental results of secure computation was presented by Ben-Or, Goldwasser, and ...
Multiparty computation secure against continual memory leakage
STOC '12: Proceedings of the forty-fourth annual ACM symposium on Theory of computing

We construct a multiparty computation (MPC) protocol that is secure even if a malicious adversary, in addition to corrupting 1-ε fraction of all parties for an arbitrarily small constant ε >0, can leak information about the secret state of each honest ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

PLDI 2021: Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation

June 2021

1341 pages

ISBN:9781450383912

DOI:10.1145/3453483

General Chair:
Stephen N. Freund
Williams College, USA
,
Program Chair:
Eran Yahav
Technion, Israel

Copyright © 2021 Owner/Author.

This work is licensed under a Creative Commons Attribution International 4.0 License.

Sponsors

SIGPLAN: ACM Special Interest Group on Programming Languages

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 18 June 2021

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Badges

Author Tags

Qualifiers

Research-article

Funding Sources

NSF

Conference

PLDI '21

Sponsor:

SIGPLAN

PLDI '21: 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation

June 20 - 25, 2021

Virtual, Canada

Acceptance Rates

Overall Acceptance Rate 406 of 2,067 submissions, 20%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

12
Total Citations
View Citations
2,301
Total Downloads

Downloads (Last 12 months)944
Downloads (Last 6 weeks)68

Reflects downloads up to 23 Sep 2024

Other Metrics

View Author Metrics

Citations

Cited By

Chen XHe SSun LZheng YWu C(2024)A Survey of Consortium Blockchain and Its ApplicationsCryptography10.3390/cryptography80200128:2(12)Online publication date: 22-Mar-2024
https://doi.org/10.3390/cryptography8020012
Skalka CNear J(2024)Language-Based Security for Low-Level MPCProceedings of the 26th International Symposium on Principles and Practice of Declarative Programming10.1145/3678232.3678246(1-14)Online publication date: 9-Sep-2024
https://dl.acm.org/doi/10.1145/3678232.3678246
Ye QDelaware B(2024)Taypsi: Static Enforcement of Privacy Policies for Policy-Agnostic Oblivious ComputationProceedings of the ACM on Programming Languages10.1145/36498618:OOPSLA1(1407-1436)Online publication date: 29-Apr-2024
https://dl.acm.org/doi/10.1145/3649861
Lamba ATaylor MBeardsley VBambeck JBond MLin Z(2024)Cocoon: Static Information Flow Control in RustProceedings of the ACM on Programming Languages10.1145/36498178:OOPSLA1(166-193)Online publication date: 29-Apr-2024
https://dl.acm.org/doi/10.1145/3649817
Künnemann RPatrignani MCecchetti E(2024)Computationally Bounded Robust Compilation and Universally Composable Security2024 IEEE 37th Computer Security Foundations Symposium (CSF)10.1109/CSF61375.2024.00024(265-278)Online publication date: 8-Jul-2024
https://doi.org/10.1109/CSF61375.2024.00024
Acay CGancher JRecto RMyers A(2024)Secure Synthesis of Distributed Cryptographic Applications2024 IEEE 37th Computer Security Foundations Symposium (CSF)10.1109/CSF61375.2024.00021(433-448)Online publication date: 8-Jul-2024
https://doi.org/10.1109/CSF61375.2024.00021
Bogdanov DJääger JLaud PNestra HPettai MRandmets JRebane RSokk VTali KValdma S(2024)ZK-SecreC: a Domain-Specific Language for Zero-Knowledge Proofs2024 IEEE 37th Computer Security Foundations Symposium (CSF)10.1109/CSF61375.2024.00010(372-387)Online publication date: 8-Jul-2024
https://doi.org/10.1109/CSF61375.2024.00010
Smajlović HShajii ABerger BCho HNumanagić I(2023)Sequre: a high-performance framework for secure multiparty computation enables biomedical data sharingGenome Biology10.1186/s13059-022-02841-524:1Online publication date: 11-Jan-2023
https://doi.org/10.1186/s13059-022-02841-5
Ye QDelaware B(2023)Taype: A Policy-Agnostic Language for Oblivious ComputationProceedings of the ACM on Programming Languages10.1145/35912617:PLDI(1001-1025)Online publication date: 6-Jun-2023
https://dl.acm.org/doi/10.1145/3591261
Mangipudi SChuprikov PEugster PViering MSavvides S(2023)Generalized Policy-Based Noninterference for Efficient Confidentiality-PreservationProceedings of the ACM on Programming Languages10.1145/35912317:PLDI(267-291)Online publication date: 6-Jun-2023
https://dl.acm.org/doi/10.1145/3591231
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Table of Contents