search

ZcashFoundation / GrantProposals-2018Q2

Submission site for 2018Q2 Zcash Foundation grant proposals.
26 stars 2 forks source link

Integrating MPC and ZK-compiler technology #33

Closed bhemen closed 6 years ago

bhemen commented 6 years ago

Motivation:

In recent years, several efficient, open-source compilers have been developed that translate code from a high-level language into a secure multiparty-computation (MPC) protocols. Starting with the FairPlay compiler 1 , MPC compiler technology has improved dramatically in the intervening years. Most MPC compilers convert a high-level language into an optimized circuit representation that can then be computed securely using a circuit-based MPC protocol like Garbled Circuits, GMW or BGW.

Compilers for ZK proof systems have many similar constraints to MPC protocols, and the ZK programming pipeline is similar. Indeed the libsnark documentation suggests the following workflow: “Express the statements to be proved as an R1CS (or any of the other languages above, such as arithmetic circuits, Boolean circuits, or TinyRAM). This is done by writing C++ code that constructs an R1CS, and linking this code together with libsnark.”2

The similarities between ZK compilers and MPC compilers have been recognized, and the some ZK compilers actually use the FairPlay infrastructure to convert a high-level language (SFDL) into a circuit 3. The Pepper project has improved dramatically in the past few years, can compile a c-based language into a constraint system suitable for proof using libsnark 4.

Approach:

We propose integrating more modern MPC compilers with the zk-SNARK toolchains. MPC compilers like Wysteria 5,6 and EMP-toolkit 7 provide high-level languages for generating circuits and executing them securely. There are also circuit generators like Frigate 8,9 and CBMC-GC 10,11 that convert c-code into highly optimized boolean circuits. The circuits generated by these MPC compilers are intended to be executed using an MPC protocol, but they could be translated into R1CS format and executed with zk-SNARK technology (e.g. libsnark). Other advanced MPC compilers like ABY 12,13, Obliv-C 14, PICCO 15 and SPDZ 16 build and execute arithmetic and boolean circuits internally, but unlike the compilers listed above, these do not provide an easy method to export the underlying circuit, and thus it would be somewhat more difficult to integrate into the zk-SNARK pipeline.

Moving in the other direction, it would be interesting to explore whether the tools used compile and verify tinyRAM programs 17–19 could be used for more versatile MPC compilers.

Benefits:

There are many potential benefits from research in this area.

Front-end flexibility: Circuit-conversion utilities that convert circuits generated by MPC compilers into formats suitable for ZK (e.g. readable by libsnark) would immediately provide new front-end flexibility. For example, Wysteria creates circuits from a functional programming language (based on OCaml), whereas CBMC-GC and Frigate use a c-like language. Connecting these compilers to a ZK-backend would make it possible to program zk-SNARKs using a variety of different high-level languages.

Circuit optimization: Some circuit generators for MPC (e.g. CBMC-GC and Frigate) have invested significant effort in circuit-optimization, and it would be valuable to see how the size of these circuits compare to those generated within the ZK community.

MPC improvements: Most MPC compilers have focused on securely executing functions encoded as circuits. Garbled RAM programs 20–24 are designed to securely compute functions in the RAM model, but these theoretical advances have not yet made it into practical compilers. On the other hand, within the ZK community, tools for verifying RAM-model computations have been implemented. These tools cannot be ported to the MPC model directly because they are designed for verifying a RAM computation rather than executing it fully, but it would be valuable to explore whether any of the underlying ideas or implementations could be used to improve garbled RAM systems.

Standardization and interoperability: As compiler technology improves in both the MPC and ZK communities, maintaining interoperability will benefit both communities. Our team has already built conversion tools that link different MPC compilers, and allow interoperability between different front-ends and back-ends. Similar tools in the ZK space would benefit both communities.

MPC for parameter generation: MPC protocols are used in parameter generation ceremonies for ZK proof systems 25. MPC compiler technology makes it easy to prototype such secure parameter generation protocols. In this direction, our team has already implemented and benchmarked secure key generation for public-key cryptosystems using MPC.

MPC-in-the-head: The ZKBoo system 26–29 implements the “MPC-in-the-head” paradigm 30 to generate ZK proofs based on a simulation of an MPC computation. It would be interesting to explore in what ways improvements to MPC compilers and protocols could be translated into improvements in ZK proofs through the MPC-in-the-head paradigm.

Who we are:

Our team at Penn consists of Research Assistant Professor Brett Hemenway Falk and graduate students Marcella Hastings and Daniel Noble. We have been deeply immersed in MPC-compilers, and funding from the ZCash Foundation would allow us to to translate some of this knowledge to improve zk-SNARK compiler technology.

References:

  1. [Fairplay project. Available at:] https://www.cs.huji.ac.il/project/Fairplay/. [(Accessed: 18th May 2018)]

  2. [scipr-lab. scipr-lab/libsnark. GitHub Available at:] https://github.com/scipr-lab/libsnark. [(Accessed: 17th May 2018)]

  3. [Setty, S. et al. Taking proof-based verified computation a few steps closer to practicality. in USENIX]

  4. [pepper-project. pepper-project/pequin. GitHub Available at:] https://github.com/pepper-project/pequin. [(Accessed: 17th May 2018)]

  5. [aseemr / Wysteria / wiki / Home — Bitbucket. Available at:] https://bitbucket.org/aseemr/wysteria. [(Accessed: 18th May 2018)]

  6. [Rastogi, A., Hammer, M. A. & Hicks, M. Wysteria: A Programming Language for Generic, Mixed-Mode Multiparty Computations. in 2014 IEEE Symposium on Security and Privacy (2014). doi:]10.1109/sp.2014.48

  7. [emp-toolkit. GitHub Available at:] https://github.com/emp-toolkit. [(Accessed: 17th May 2018)]

  8. [Mood, B., Gupta, D., Carter, H., Butler, K. & Traynor, P. Frigate: A Validated, Extensible, and Efficient Compiler and Interpreter for Secure Computation. in 2016 IEEE European Symposium on Security and Privacy (EuroS&P) (2016). doi:]10.1109/eurosp.2016.20

  9. [bmood / FrigateRelease. Available at:] https://bitbucket.org/bmood/frigaterelease. [(Accessed: 17th May 2018)]

  10. [CBMC-GC | Security Engineering Group | TU Darmstadt. Available at:] https://www.seceng.informatik.tu-darmstadt.de/research/software/cbmc-gc/. [(Accessed: 18th May 2018)]

  11. [Holzer, A., Franz, M., Katzenbeisser, S. & Veith, H. Secure two-party computations in ANSI C. in Proceedings of the 2012 ACM conference on Computer and communications security - CCS ’12 (2012). doi:]10.1145/2382196.2382278

  12. [Demmler, D., Schneider, T. & Zohner, M. ABY - A Framework for Efficient Mixed-Protocol Secure Two-Party Computation. in Proceedings 2015 Network and Distributed System Security Symposium (2015). doi:]10.14722/ndss.2015.23113

  13. [encryptogroup. encryptogroup/ABY. GitHub Available at:] https://github.com/encryptogroup/ABY. [(Accessed: 17th May 2018)]

  14. [samee. samee/obliv-c. GitHub Available at:] https://github.com/samee/obliv-c. [(Accessed: 17th May 2018)]

  15. [PICCO-Team. PICCO-Team/picco. GitHub Available at:] https://github.com/PICCO-Team/picco. [(Accessed: 17th May 2018)]

  16. [bristolcrypto. bristolcrypto/SPDZ-2. GitHub Available at:] https://github.com/bristolcrypto/SPDZ-2. [(Accessed: 18th May 2018)]

  17. [Ben-Sasson, E., Chiesa, A., Genkin, D., Tromer, E. & Virza, M. SNARKs for C: Verifying Program Executions Succinctly and in Zero Knowledge. in Lecture Notes in Computer Science 90–108 (2013).]

  18. [Ben-Sasson, E., Chiesa, A., Tromer, E. & Virza, M. Succinct Non-Interactive Zero Knowledge for a von Neumann Architecture. in USENIX]

  19. [pepper-project. pepper-project/tinyram. GitHub Available at:] https://github.com/pepper-project/tinyram. [(Accessed: 18th May 2018)]

  20. [Lu, S. & Ostrovsky, R. How to Garble RAM Programs? in Lecture Notes in Computer Science 719–734 (2013).]

  21. [Gentry, C. et al. Garbled RAM Revisited. in Lecture Notes in Computer Science 405–422 (2014).]

  22. [Garg, S., Lu, S. & Ostrovsky, R. Black-Box Garbled RAM. in 2015 IEEE 56th Annual Symposium on Foundations of Computer Science (2015). doi:]10.1109/focs.2015.22

  23. [Garg, S., Lu, S., Ostrovsky, R. & Scafuro, A. Garbled RAM From One-Way Functions. in Proceedings of the Forty-Seventh Annual ACM on Symposium on Theory of Computing - STOC ’15 (2015). doi:]10.1145/2746539.2746593

  24. [Canetti, R. & Holmgren, J. Fully Succinct Garbled RAM. in Proceedings of the 2016 ACM Conference on Innovations in Theoretical Computer Science - ITCS ’16 (2016). doi:]10.1145/2840728.2840765

  25. [Bowe, S., Gabizon, A. & Miers, I. Scalable Multi-party Computation for zk-SNARK Parameters in the Random Beacon Model.]

  26. [Giacomelli, I., Madsen, J. & Orlandi, C. ZKBoo: Faster Zero-Knowledge for Boolean Circuits.]

  27. [Sobuno. Sobuno/ZKBoo. GitHub Available at:] https://github.com/Sobuno/ZKBoo. [(Accessed: 18th May 2018)]

  28. [Chase, M. et al. Post-Quantum Zero-Knowledge and Signatures from Symmetric-Key Primitives. in Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security - CCS ’17 (2017). doi:]10.1145/3133956.3133997

  29. [Microsoft. Microsoft/Picnic. GitHub Available at:] https://github.com/Microsoft/Picnic. [(Accessed: 18th May 2018)]

  30. [Ishai, Y., Kushilevitz, E., Ostrovsky, R. & Sahai, A. Zero-Knowledge Proofs from Secure Multiparty Computation. SIAM J. Comput. 39, 1121–1152 (2009).]

alc-nmff commented 6 years ago

Hi, could you please provide more details on the budget and timeframe? Thank you!

tromer commented 6 years ago

The Zcash Foundation Grant Review committee has reviewed your pre-proposal, including the above discussion, to evaluate its potential and competitiveness relative to other proposals. Every pre-proposal was evaluated by at least 3 (and typically more than 4) committee members .

The committee's opinion is that your pre-proposal is a promising candidate funding in this round, and the committee therefore invites you to submit a full proposal. Please submit a full proposal by June 15th, following the detailed structure described in the Call for Proposals. We encourage you to submit a draft as early as possible, to allow for community feedback.

marsella commented 6 years ago

Thanks for the invitation. Our full proposal is attached, including budget and timeframe details.

proposal.pdf

tromer commented 6 years ago

@bhemen:

There are numerous compilers (ZK proof "front-ends") for creating constraints systems for modern SNARKs. These include (alphabetically): Buffet+Pantry, Bellman, C0C0, jsnark, DSL Snarky, libsnark’s gadgetlib1+gadgetlib2, Pequin, Pinocchio+Geppetto, Snarkl, TinyRAM, xJsnark, ZoKrates (see some links on zkp.science). What advantages do you expect to your approach compared to these?

Also, while the high-level idea of SNARK and MPC compilers are similar, there are some essential techniques that are applicable only in SNARK setting. The biggest one is that MPC computers a function, whereas the SNARK verifies a predicate whose inputs are fully known to the prover. This means the prover can perform auxiliary "helper" computations, and provide the results as untrusted advice to the predicate being proven by the SNARK (a simple example: computing integer division requires a complex circuit; but verifying the result of a division, whose purported output is given as untrusted advice, is trivial). Most applications of SNARKs cruciall rely on this for performance, and the aforementioned compilers generally support it.

Additional differences stem from the fact that most zk-SNARK schemes have a native constraint system native language consisting of bilinear constraints over large finite fields, which is a different model than most MPCs and enables specific optimizations as well as introducing new considerations (e.g., in many cases costs are dominated by checking that variables are 0/1).

The implementation papers linked above have ample discussion of these points (e.g., see the discussion of nondeterminism in SNARKs for C), and you can see concrete examples in the implementations (e.g., the libsnark gadget libraries associated with the above paper).

What are your plans for this "impedance mismatch" between the MPC and SNARK worlds?

bhemen commented 6 years ago

The question of "impedance mismatch" between MPC and ZK compilers is an important one, and we have been actively thinking about how to address this issue. Below, we outline some of our ideas on this subject, but we will likely need to dive deeper into the details of many implementations in order to answer them all fully.

While many ZK Proof compilers have been developed, and we used the list at zkp.science extensively when planning this project, we believe that a ZK Proof front-end based on an MPC compiler would be a useful contribution to the ZK community. In part, this is because many of the compilers listed there are important historical works, but do not represent the state-of-the-art in terms of practical snark compilers. For example:

Bellman: "Bellman is still under development and shouldn’t be used in production software yet. In fact, its API deliberately does not expose anything that would allow you to actually use it!" -- Sean Bowe (https://blog.z.cash/bellman-zksnarks-in-rust/) Buffet and Pantry: were developed by the team responsible for the Pepper project, and seem to be subsumed by Pequin Pinocchio and Geppetto: do not seem to be under active development, it appears that libsnark provides a strict improvement to their functionality ZoKrates: does not provide a general purpose snark compiler, but instead aims at integrating snarks into ethereum CoCo, jsnark, and xjsnark: were all developed by the same team, and only xjsnark provides a high-level programming language Snarkl: Provides a high-level functional programming language (and uses libsnark as a back-end) TinyRAM: there seem to be performance issues with TinyRAM: “TinyRAM incurs a significant overhead compared to expressing computation directly as constraints using custom gadgets. In applications where the statements are of a simple fixed form (e.g., as a Boolean circuit), using tailored gadgets can provide better performance than going through TinyRAM. In Zerocash, we used the latter.” -- Eran Tromer 2014 (https://github.com/scipr-lab/libsnark/issues/2) The Buffet paper suggests similar performance issues with TinyRAM: "in BCTV, every program step compiles to one to two thousand constraints, of which several hundred are for memory checking" (https://www.pepper-project.org/buffet-ndss15.pdf)

This leaves Pequin, xjsnark, snarkl and snarky remain as the "front-ends-to-beat." Most systems use libsnark as a back-end (including, Pequin, jsnark, snarkl, snarky), and we intend to do the same. The MPC circuit compilers we propose to use (Frigate in particular) have usability as a primary goal, and are designed to make circuit specification easy. The main contribution of our work, therefore, is to simplify and make accessible the function specification step of zk-SNARK toolchain.

The difference between computing a function and verifying it is indeed one of the main differences between the MPC setting and the ZK setting. This problem does not seem insurmountable though. The key question is at what point the optimizations occur. Consider the example of division: verifying the corresponding multiplication is easier, and (we believe) that in most systems, the developer makes this optimization "by hand," by using a multiplication circuit as input, instead of a division circuit. This method of optimization, although not ideal, is clearly compatible with MPC-compiler front-ends. On the other hand, if the snark back-end receives a division circuit and automatically performs circuit-level optimizations to create a simpler circuit that is more amenable to ZK arguments, then this is also compatible with circuits generated by MPC-compiler front-ends. It is true, however, that MPC compilers generally do not have methods for easily specifying useful "helper advice," and to make these systems as efficient and usable as possible would probably require modifying the the MPC compilers slightly to naturally support such advice.

Although most ZK proof systems have a native language consisting of bilinear constraints, this does not make them incompatible with MPC-based circuit generators. Most ZK systems have a workflow: high-level-specification → Arithmetic circuit → R1CS → QAP, and we are interested in the first step of the chain: converting a computation specified in a high-level language to an arithmetic circuit. The snark back-end (e.g. libsnark) will then handle many of the issues revolving around optimizing the QAP representation, and technical details (like proving the variables are 0/1).

As we continue this line of research, we expect to encounter many details that affect the performance, usability and overall workflow of these ZK compilers.

sonyamann commented 6 years ago

We regret to inform you that your submission was not selected by the Grant Review Committee, and hence the Zcash Foundation will not be funding this proposal. Thank you very much for your thoughtful contribution!

Please consider subscribing to the Zcash Foundation newsletter so that you will be notified of future funding opportunities.

The Grant Review Committee’s comments:

The proposers, researchers from University of Pennsylvania, suggest to create new front-end compilers for creating statements to be proven by zk-SNARK cryptosystems. This will make the creation of new applications that use zk-SNARKs easier and less prone to errors. They observe that several analogous compilers exist for another cryptographic technique for securely executing code: Secure Multiparty Computation (MPC). They propose to adapt those existing compilers to the zk-SNARK setting.

While the idea is appealing, there are several reservations:

First, to date the implementation fo zk-SNARK statements (using existing tools) has not been a major bottleneck in the creation privacy-preserving payment systems: the relevant efforts have typically been dominated by the high-level design work of the statements and associated cryptographic protocols, and the building low-level components (e.g., Merkle tree path verification) that require manual hand-crafting for efficiency. Thus, while zk-SNARK front-end compilers may be of use for other applications or more complex financial assets, at present their direct furtherance of the Zcash Foundation's goal is limited.

Second, there are substantial differences between the zk-SNARK and MPC settings (for example, in that zk-SNARK statements can exploit helper computation providing advice, which seems to require a differenty way of framing and compiling the high-level programs). While this was acknowledged and discussed by the proposers, there is not yet a detailed approach to tackling this crucial issue.

Third, there are already several ongoing and forthcoming efforts to create highly capable zk-SNARK front-end compilers (motivated by more complex applications), so supporting the proposal does not appear necessary for progress to be made in this area.

For these reasons, and in light of the budget's magnitude, the committee does not recommend funding this proposal.