zkSummit - Marlin: Preprocessing zkSNARKs with Universal and Updatable SRS - Pratyush Mishra

12 Nov 2019 · 30:48

Pratyush Mishra presents Marlin, a construction for preprocessing zkSNARKs with a universal and updatable structured reference string, at this Zero Knowledge Summit talk recorded in San Francisco. He walks through the general methodology behind the construction and how it improves on Sonic, the prior state of the art, across every efficiency metric: proving is an order of magnitude faster, verification runs three times as fast, and proofs stay just over a kilobyte in size. The talk covers zk-SNARK design, universal setup ceremonies, and proof system efficiency tradeoffs.

Speakers

Topics

Transcript

[Music] hi everyone I'm pratik and I'm here to talk about Marlin which is our work which constructs pre-processing Zika snacks with universal set up this is joint work with Alli who is here in song who also might be here is that Mary who is I think in London right now no I was also in the audience and Nick at Berkeley so if you want to take a look go ahead okay so let's dive in so as I mentioned before we talk about you know stacks let's take a look at in a soccer-specific it's not such a circuit specific setup so let's say I have some circuit and I want to prove that you know I know some secret witness witness

would satisfy the circuit to do so I would use an argument system for circuits add as are they already mentioned and this consists of these three algorithms right so you have your set up algorithm you have which this this thing takes in a description of the circuit and produces circuit specific proving and verification keys you have your proof proving algorithm which takes in a circuit specific proving key and if you have a witness gives you a valid proof and finally you have your verification key which takes in a proof and checks whether or not it's a valid proof right and I already mentioned some of the nice properties that we have for today like with snacks - if I cross 16 you get very fast verification and relatively fast proving but the problem

is that you know the set up algorithm needs to be run by a trusted party obvious some sort of expensive NPC ceremony and even worse you know as Ollie mentioned if you are using this circuit specific setup you have to rerun this set up algorithm every time you change your circuits even if you modify it a tiny bit you have to rerun the entire very expensive NPC ceremony which is a logistical and operational nightmare right so the new goal that we want is what's called Universal setup so we want to be able to perform you know the trusted part of a set of just once just you know independent of any individual circuit we just take in the maximum size

of the computation that we want to support and we get Universal proving and verification keys and the eye that once we have these universal keys we should be able to do circuit specific pre-processing in a deterministic manner so what this means is that after we do this universal set up we take a universal proving key and the specific circuits a c1 and produce circuit specific keys for proving and verification in an entirely deterministic fashion and you can do this for any number of circuits that we have and the idea is that now because this process is deterministic anybody can go ahead and rerun the pre-processing step and check you know whether the result is correct whether the parameters were generated correctly

all right so this is our goal in this talk so what we do in modern to it to you know work towards this goal is we have three contributions the first is we provide a methodology that you know explains how to construct D stocks this is one of the paradigms that are they mentioned right and how what this what this paradigm looks like is that we have a compiler which takes in two components so an algebraic holographic proof and polynomial commitment which is extractable and produces your pre-processing snack with universal SRS all right the nice thing about this compiler is that you know this modularization is really beneficial for a understanding the construction but also you know if you're a snack designer

you can go ahead and focus on improving each of these components individually and what the compiler theorem guarantees is that as long as you satisfy the requirements of the compiler you can just plug in your very optimized component and you'll get out a secure snack which is like zero knowledge sound all the nice properties that you want okay and actually if you look at all the exciting works that have come out over the past year such as sonic long marlin supersonic what they're co-contribution really is is an optimizing one of these two components so you'll hear about I think how you know about these optimized components later today okay so our compiler is exciting it's not so useful if you don't have ingredients to plug it plug in so what we do and also also do in Marlin is to construct some of these

efficient ingredients the first thing that we construct is a HP for our one CS and also we extend the kzg 10 polynomial commitment scheme which is used for example also in Sonic to fit in the requirements of our compiler so and when you plug these into the compiler what you end up with is Marlin which is a pre-processing syke snack for our 1cs which has Universal setup okay so this is all nice but it's not really super helpful it's just you know a theoretical construction so what we do also is provide an implementation in rust that's available at this URL and basically this performs very well as we can see quickly

here we compared it we compared Marlin implementation with the state of the art circuit specific non-universal pre-processing stock which is grad 16 and what we found was that for the relevant parameters like you know proof size proved a time verify time we're at most like an order of magnitude away from you know the state-of-the-art scheme so proof size is like 6 X or something proved over time this is roughly 10 X verify time is at 4 X off and I think all these numbers will only shrink as you know people optimize the two components the commitment and the AHP alright we weren't able to compare that you know sonic which kick-started this entire area of universal SRS research because I mean we I don't think

we found our implementation of the fullest extent variant there's also another concurrent work which you'll hear about I think in the next talk and the difference between marlin and plunk is really in some sense qualitative marlin is good for our 1 cs and plunk it it works with arithmetic circuits so it's better when you're like computation or when your system is working with their synthetic circuits we haven't been able to again compare because I think the implementation only came up a couple of weeks ago so we haven't done like a qualitative comparative comparison yet but I think the high-level bit is that you know they're roughly similar in performance I don't think there should be a massive difference ok all right so that's all I'm gonna say about the implementation

in this talk I'll be focusing mostly on the methodology because AI think it's you know construction is a very straightforward and clean construction once you have your two components so we I think educational to look at how a snack is actually constructed and also what I say technical point our construction really highlights that the key to achieving pre-processing and hence you know succinctly era fication is what's a technical term called holography like in retrospect this connection and we will see like is in some sense obvious but you know we haven't been prior to this able to make this connection okay all right any questions all right so let's dive in so we'll proceed step by step right we will

first look at each of the components so the holographic proof and the pollen equipment and then we'll see how our compiler and it combines these two components to get out the snack that we want all right okay so so the algebraic holographic proof is you know quite a mouthful it's two very heavy words let's see what each of these adjectives means in this context so at a high level and algebraic proof is just an interactive proof where the proven messages have some sort of algebraic structure concretely like in in our formalization this algebraic structure is a low degree polynomial so what we do is we restrict the prove of messages to be low degree polynomials if you only send for example

univariate polynomials that are much smaller than the size of the field so the prover sends along this polynomial and the verifier is not required to read the polynomial in its entirety you can just leave the Oracle there or leave the polynomial there and actually access it as an Oracle it can ask you know hey polynomial what's your value at you know point 10 and the polynomial tell it and the idea is that by not reading it you know you don't have to pay the cost of you know might be like really high degree so the verify doesn't have to you know pay this entire cost of reading the entire degree alright so the prover sends its polynomial or maybe a bunch of polynomials the verifier replies with some random challenge so here we're

working in the public coin setting so the verifier only sends random messages and this continues until proven Zout of polynomials descent so you go P 1 through P n and the verify gives us last challenge and so now the approver doesn't talk right what the verifier does is it tries to query each of these polynomials at some some set of points that it wants to query these points at so it makes a query set right and the idea is that it asks a p1 what's your value at some point Z 1 and n p1 certain my values v1 and this goes on for all the polynomials and once the verifier has these evaluation results or query results it plugs them in into some decision

procedure and decides whether or not to accept right sophisticate okay so this is know in a diagram what an algebraic proof is to the messages of polynomials the verify can query these polynomials and make a decision based on whether to accept based on these query results ok so the properties of this are pretty standard properties of interactive proofs right you have completeness so whenever the prover has a satisfying circuit and it follows oh hazards flying witness and it follows the protocol the verify should accept you have proof of knowledge which I'll briefly mentioned which says that whenever the verifier accepts is the

case that the prover actually knows a corresponding witness right that there's some witness living inside the poopers head and finally you have slightly wonky notion of your knowledge but all this says is that you know as long as the verifier doesn't make too many queries to the polynomials then it learns nothing about the witness and we have this like query bounded notion only because that's all we need for our compiler you could consider more advanced notions but we don't need them so we don't discuss that ok so that's nice so we have now this algebraic proof but me you know we came here for 16 clarification right what's the complexity of the verifier right that's the next question the problem is right

now the verify complexity is at least linear in the size of the circuit right because it has to read the circuit as input so at the very least you know will be run running linearly and maybe it does some more computation based on the circuit so it could even be you know more than linearly could be like polynomial inside a circuit and that's not what you want that we want be like 6 and at most logarithmic in a circuit size right that's the goal of the talk and sigilyph reprocessing snacks in general ok so if you want to do is in some sense take the circuit out of the verifier right and how do we do this and but ok so we've done this let's say we take a circuit out of the verifier the verify still needs to know

what sort of computation is checking right right now it doesn't have any such idea so what we want to do is instead of having the verifier read the circuit in its entirety we want to verify to just be able to access encoded or algebraic version of the circuit right and to do this this is where the holography comes in we have some sort of holographic pre-processing algorithm which takes in the circuit and produces algebraic encoding of the circuit so namely in our case it looks like a polynomial representation of the circuit and the idea is that now the verify can access these polynomials as in Oracle just like it was accessing the proving messages as an Oracle

right so yeah now the verify no longer has a sort of linear dependence on the circuit so what we do now is you know the proven verify interact is before the exchange of messages the prove of generates its queries and now instead of you know so we make a queries as before you query the proper messages but you also make queries to the circuit polynomials right and based on the results of all of these queries so all of them you go ahead and make a decision and decide not to accept now this is nice because now we no longer have a dependence on the circuit size in the verify runtime so as long as

your query and decision procedures are you know independent or at most logarithmic of in the circuit size then your entire algebraic verifier your HP verifier is logarithmic in the circuit size at most right ok so to recap an algebraic holographic proof is an attractive proof where the prover messages are polynomials and the verifier gets to look at the circuit only in some sort of encoded form as an article that's the key takeaway from this and then coding allows you to get succinct verification all right any questions so far that was like a somewhat heavy technical portion yeah

so no because the index polynomials are all public right as I said the pre-processing sorry the circuit polynomials they're the output of information leakage that also prevents the verifier from making as many queries so the very query okay so maybe I should have explained this a little bit better but this pre-processing step is a public step it occurs offline information theoretically and it's a deterministic process and anybody can be run the pre-processing at any point in time and until they'll get at the same set of polynomials and the idea since these polynomials or any of the circuit is anyway public right it doesn't matter if you query a 10 times or a hundred

times or thousand times so there's no additional leakage from zero knowledge found there okay oh yeah thanks for the question okay all right so now we have one of our components complete right let's take a look at the second one so at a high level a polynomial commitment is a cryptographic primitive that allows you to commit to a polynomial and then later you know prove that the committed polynomial evaluates to some point to some value added chosen challenge point right and the idea is that as long as its commitment is extinct there and the proof is extinct then this verification procedure is much more efficient ok so let's take a look in a bit more detail

so polynomial company has the sort of set up algorithm which takes in the maximum degree that you want to support your polynomial and outputs is Universal committer and verifier keys that work for any polynomial up to that degree okay and then later a committer can take its commuter key and commit to a polynomial and provide and send over the commitment to the verifier I think the idea is this commitment is supposed to be smaller than the polynomial in this coefficient form for example okay so you send over the commitment and the verify says okay I want to know the value of

your committed polynomial at some point Z so it sends over the challenge point Z the committee the committee evaluates the polynomial at that point and then also it provides what's called a proof of evaluation of the commitment at that challenge point all right and it sends over both the proof and the evaluation and the verify can can then go ahead and check the proof evaluation to make sure that the prover is not you know making a false claim about the evaluation right so after this point what the verifier knows is that you know if the proof is satisfied then the committed polynomial actually does evaluate to the value V at

the point Z okay so the properties that you want of this Paloma clinton scheme are basically the same as I mean very similar to what we had with HP you want completeness which says that you know if the polynomial actually does evaluate to the value V at Z then the verifier all those accepts right you want extract ability which says that whenever the verifier does accept the commitment actually you know in some sense contains a polynomial of degree at most D that has this you know this relation and finally you also want hiding which says that as long as the verifier doesn't make too many queries it learns nothing about the polynomial beyond like the

evaluations and this hiding this you know this query about is necessary because if you make I don't know up - if you make degree D queries like these many queries and you learn all the coefficients via Lagrange interpolation or whatever okay so these are the properties that you want and this is like the very simple notion of pollen comeuppance you've known about this for I would almost like ten years now it's called the kisi g10 I mean the kata a tall paper in 2010 I believe introduced this notion but to plug into a compiler we actually need more properties basically you want to intern you support some of the properties of our HP so what we need to be able to do is support like

batch commitment because each round in the HP can has multiple polynomials you won't be able to commit to multiple power Long's at once you want to be able to commit to polynomials across multiple rounds and then have extract ability also hold for this you know multi round notion you want to be able to open your polynomials not at like a single point but at a query set Q and finally this is a bit of a technical notion you also want to be able to have per polynomial degree bounds okay this is technical you know it doesn't quite fall straightforwardly from the simpler notion you have to do a little bit of work to make sure extract ability and all the other properties hold when you have these additional properties but you can look at the paper if you want to see how it's done okay so now we have both

of our components right we have the AHP and the polynomial commitment any questions about the commitment scheme yeah maybe could you use fry in this case to commit to a polynomial instead of using the [Music] there's paper from the matter Labs folks where they used fry to get basically a transparent polynomial commitment and if you make that commitment fit you know the interface required by our compiler so you know have all these properties then you could plug that in and have a transparent parlament as well and you

know a bit Frey is the underlying mechanism and generally any low degree test would work for that okay all right so so let's now so we have we have our components let's take a look at how our compiler actually works and the key idea here is to you know leverage the holography in the AHP to achieve pre-processing so let's take a look so let's quickly first recap you know what a pre-processing stock with universal setup is so you have these four algorithms right you have setup this is the universal parameters you have a soccer-specific pre-processing which produces a circuit specific keys you have your proven verify which produces proof and verify approved respectively and the properties are again the

standard once you know of completeness book of knowledge and the you knowledge I won't go over this because you know it's a standard notion you can look at any paper okay so let's take a look let's look at how a compiler constructs each of these algorithms in step-by-step manner starting with the universal set up okay so set up you takin you know the maximum size of the circuit that you want to support for example and you ask the AHP hey this is the maximum circuit size that I want to support what's the maximum degree of the polynomial sent by either the prover or inside the you know the pre-processing step and the HP says okay the maximum degree is D and then

what you go ahead and do is you run your PC your polymer can set up for that maximum degree and the idea is that now these you know these keys will support anything that the HP prove our pre-processing output right and you just said these basically as your universal keys okay so that's very simple not nothing complicated here you just invoke polynomial and set up a 15 okay so this is a bit more involved so let's take a look at how you would do circuit specific pre-processing so now you get in your universal Coover key as well as the circuit and we want remember you want this entire process to be

deterministic right so first we run the deterministic HPP processing alright which takes in the circuit and gives us like the encoded form of the algebraic encoded form of the circuit so you could have the circuit polynomials and then you just commit to these using your pedometer and the idea is that these commitments or this process is a deterministic process if you don't want hiding technical detail and so you make these deterministic commitments and now you're basically a circuit a verifier key consists of the commitments here and so approver key consists of the index of the circuit that I should be a/c sorry all right any questions about this it's

very simple we just run the AHP pre-processing take the polynomial set it outputs and commit to them using the problem with commitment in a deterministic way yeah the index is some formalization in the in the paper just think of this as a circuit is a circuit yeah okay yeah you say that the secretary processing is deterministic because if it is randomized it doesn't help can it be put if it's randomized you have to publish the randomness for the commitment basically basically we don't need it you don't need because these polynomials are

you know deterministic generated from the circuit we don't need for their commitments to be hiding I don't know if you can prove or not whether or not I guess like the point of this step is that anybody should be able to rerun the pre-processing right and maybe also check that the resulting circuit specific parameters are correct so if you have some secret randomness then it doesn't help with that okay processing I said very simple run the HPP processor and commit to the power gamma theta dolphins okay so let's take a look at you know the big algorithms you need of the protocol proven verify right so you have your argument prove oh and your

argument verifier this one has a witness this one doesn't is very simple you run the argument prover runs the AHP prover inside it and whenever it produces a commitment instead of sending the commitment as is you send a longer commitment to sorry whenever it produces a polynomial instead of sending along the polynomial as is you send along a commitment to the polynomial right so the argument Provo takes p1 makes the commitment see m1 and sends that to the argument verifier then the argument verifier asks the HP verify for the randomness and this continues until the HP prove or runs out of polynomials right and then we're done and then now comes like the query and

decision phases right so the HP verifier runs its query algorithm you get your set of you get your query set and you know the argument prove evaluates the polynomials at this query set and sends back the evaluations and now the verify can run the decision procedure and decide what not to accept is this sufficient be passing isn't a previous thing that people are saying is in is you know that bitter people awesome comes as input then okay maybe I'll answer the question myself

this is insufficient right because we have no idea whether or not the prover is giving us the actually correct evaluations so instead we have the prover prove to us that these evaluations are correct and we do this by you know using the polynomial commitment to produce a proof of evaluation so we prove that you know the committed polynomials these ones as well as the index polynomials when evaluated at the query set result in these evaluations so we get out of proof and then the argument verifier in addition to running the decision procedure also checks that the evaluation proof is correct right so that's pretty much it so yeah this is an interactive protocol you can make it non attractive by

theorem here because all these messages are all random the queries are supposed to be random the challenges are all very random because it's public coin so you can get a non track document at the end of this very clean construction the idea is use holography to you know pre-process the circuit and then instead of sending polynomial to send commitments to polynomials and true that their evaluations are correct okay the nice thing is that not only is a construction clean but all of the properties that you want like completeness proof of knowledge and your knowledge they all follow very cleanly from the corresponding properties of the two components of the HP and the polymer equipment and you also get succinctness you know if the HP and the polynomial

verify as a PC verify are all 16 and this is the case for for example in Sonic in plonk in Marlin both of these components are 16 ok so that's it so today in the stock we saw how to construct these universal pre processing syke snarks from these two components of the algebraic holographic proof and the extractable polynomial commitment scheme right and the people you can find more details about you know some of the ingredients that we have so you can our HP for our ones yes is in there and deadline protocol is you know cool protocol for evaluating low-degree loaded korean coatings up the oven CS matrices and we also show how you can

extend clears each end to achieve the properties that we require for the compiler all right so thank you everyone the paper is available online at this link and the code is also there all right there are some quickly I understand that it's in the paper but it would be great if you could perhaps tell us how you extend the polynomial commitment scheme because that's what makes the proofs can you use your mic mic yeah so it's

not the case that you know be extended and like adding some new proof films or something we just take that scheme and then show that if you want to the obvious extension like batching proofs or something then the proof follows through it's not super complicated but you know it requires some legwork to actually make it work out George's can you pass the mic to the person behind you Hey so it's very nice to have this kind of like conceptual framework where you plug in these different pieces and then you get this proof system out of it and I'm wondering if if we think that we want to have like conceptual unity between the

theory and the actual implementation is it actually possible to implement this kind of compiler in practice that you would have like one library and you like just plug in different pieces in different like places and you get like either marlin or something else yeah so actually if you look at implementation that already has sort of this separation it's not quite the fully vetted compiler but a compiler but you can all this is structure like we have a separate library for paloma commitments the AHP is like a completely separate module within within library I think we'll just a little bit more work and we should be able to generalize that and get the compiler out so yeah I think that and you can just plug in and a bullet-proof

spaced PC or any other PC and I think every other time no it wasn't about time I wanted to add that I think from the perspective of sort of practice and developer community this type of modularity is rather important if anything for for gaining confidence in the security of code that is written these are rather I mean already we have issues in simple the digital signature scheme implementations there are much simpler construction than these a full snark implementation is much much more complex so making sure that the implementations that we do have have

these conceptual separations into simpler and smaller modules that we can dependently verify and fix I think it's rather important if we actually want to run like a sort of serious infrastructure on top of these things [Applause]