ZK10: Revisiting the Nova Proof System on a Cycle of Curves - Wilson Nguyen

Transcript

foreign [Music] and today I'll be presenting our work revisiting the Nova proof system on a cycle of Curves this is Joint work with jambonne from Stanford and Triana assetti from Microsoft research the cryptographic Primitive that we'll be talking about today is incrementally verifiable computation or IVC schemes for short this was introduced by Valiant in 2008 and the goal of IVC schemes are to efficiently prove the outcome of some long continuous operation so here we have a function so here we have a function f that's being repeatedly applied on these Z elements and the

claim that we would like to convince a verifier of is that some element in zi is the result of applying this function f i times on some initial element zero so why would we care about proving claims of this form well some Modern Day applications of IBC schemes are verifiable delay functions and so if F instead now is some slow function f if I prove to you that zi is a result of executing I or executing f i times in session then it must have some verified delay in addition IVC schemes can be used to construct ZK EVMS or more broadly State machines and so now instead of arbitrary elements Z

they are now States so you can imagine this is snapshots of RAM and F is now a state transition function you can imagine this as executions of some CPU so the Nova paper in 2021 introduced a novel construction of IVC schemes while the construction the paper was proven secure if instantiated in practice it was incredibly inefficient and the reason why is because it used a single elliptic curve Group which meant that a lot of non-native arithmetic had to be represented within constraint systems and so because of this inefficiency the Nova authors over the course of the following year implemented a modified

version of the Nova IVC scheme which instead operated over a cycle of Olympic a cycle of elliptic curves so now there are two curves and this dramatically reduced the amount of non-native arithmetic that they had to represent within their constraint systems but because of this oh sorry yeah because this it was incredibly efficient in practice but this modified scheme had prior never been formally described nor proven secure and it turns out there was a major soundness of vulnerability in this modified scheme and The Motif that I would like to leave with you all today is that if a cryptographic scheme has never been

formally written down nor proven secure we as cryptographers and as implementers should definitely question its security and whether we should extend or Implement these results so to give y'all a rough timeline of the discovery of this bug in the modified IVC scheme in 20 in March of 2021 the ePrint version of the Nova paper was released over the course of the following year the Nova authors implemented the modified version of the Nova IVC scheme that operated on a cycle of Curves and roughly a year later a lot of renewed interest in IVC schemes picked up as a potential method to implement

zkavms and so there were a lot of follow-up works such as hypernova protostar Supernova which altered and optimized the fulling schemes used to construct IVC and it is in this period in which I became interested in IVC in particular I was interested in researching how IVC operated on a cycle of Curves because in this whole two-year period a formal description of how any IVC scheme operates on a cycle of Curves was never given and it turns out that after a little bit of research there was a pretty big bug found in May for the Nova the modified version of the Nova IVC scheme and so zooming in to that month of April I first tried to find some just formal

description of Nova on a cycle of Curves and so the first paper the first thing I looked at was of course the updated version of the Novi print paper there was a small maybe one page section about the implementation details but this section did not give a formal description of how the scheme actually operated instead there was this obtuse table which is figure one which basically described a number of constraints required on the primary and secondary curves of the cycle and that was the summary of basically a description of Nova on a cycle I also looked in Justin thaler's textbook which is an incredibly well written textbook so I totally recommend it and which described folding schemes and different instructions of IVC from folding but the description of IVC on a

cycle of Curves was limited to this like quarter page footnote which motivated why you would want a cycle curves and two different constraint systems but it didn't go over its operation and so I realized that I would probably have to just go through the whole code base reverse engineer it and write down a formal description of how Nova operated on a cycle of Curves and hopefully write its proof of security and you know and also yeah and maybe annotate the code base but during this attempt to actually formally describe the system I realized that there was a pretty significant bug and so over the course of that April I collaborated with my advisor danbone and

SRI who is the lead author on Nova and also the lead implementer for the modified scheme and we wrote revisiting the Nova proof system on a cycle of Curves in this work we formally describe the soundest vulnerability that occurred in the modified scheme and we demonstrated that this vulnerability was indeed Real by generating a false but accepting proof of 2 to the 75 iterations of the minroot vdf and only 115 milliseconds so it turns out that in the paper I wrote 1.5 seconds but it's because I compiled it in the bug mode so it's actually a little faster and so

so yeah it's pretty that's pretty big bug in that thing okay so all right so um uh okay where was that oh yeah so since it only took 115 milliseconds or one and a half seconds if the Nova IV scheme IVC scheme had actually been secure this would have taken hundreds or thousands of years so indeed there was a real vulnerability in the system and all hope is not lost we found a fix that actually optimized the efficiency of the recursive verifier and the proof size and in doing so we formally describe it we write down a security proof but in we also provide a somewhat generic-ish compiler from folding schemes to IVC

over a cycle of Curves and so it's red it can be readily generalized like protostar or hypernova so while this short is sorry while this talk is a little bit short I'll hopefully give an intuition on how Nova operates on a cycle but maybe not the full description so what changed from the Nova paper to the implementation well instead of a choice of a single function f and a single constraint system over one field this constraint system you can roughly think constrains the execution of this one function there is now a pair of functions operating on a pair of inputs and a pair of constraint systems called the primary

and secondary constraint systems which operate on two different fields and these two functions operate on the respective two different fields as well and so now we're zooming in to the IFC Construction in particular we're first going to discuss how the IFC approver operates and so here is a diagram which represents the computation Trace that the prover wants to prove to a verifier in particular at every step we apply the pair of functions on the pair of inputs and the claim is that these pair of outputs were produced by repeatedly applying the pair of functions

and so at every step there are the two constraint systems the primary and secondary constraint systems which constrain the execution of one step of their respective function and now at every step the prover has to prove the satisfaction of these constraint systems but it doesn't suffice for the prover just to prove satisfaction of these constraint systems we need to know that at all prior steps these constraint systems were satisfied by the respective function inputs and outputs and so I'm lying to you with this very simple diagram here and so what we're going to do is we're going to take a deep dive into each of these steps but I'm going to wait a little bit just so that

diagrams in your mind okay and so at every step of the of the IVC approver they're of course the primary and the respective and the secondary constraint systems now in addition to the function inputs we also take these additional but critical elements these elements here which have a one and two to indicate primary and secondary are called accumulators which accumulate or collect the claim that all prior executions or all prior constraint systems were satisfied this green element indicated also with this 2 represents the satisfaction of

the most recent secondary constraint system in the prior IVC step so this would be step I instead now this constraint system constrains one step of the execution of the primary function but also folds together this accumulator and this fresh instance which is the green instance to produce a new accumulator which represents the satisfaction of all prior secondary constraint systems and now the satisfaction of this constraint system can also be represented as this new green element which then also gets fed

into the secondary constraint system which constrains one step of the secondary function execution but also folds together the claim that the prior constraint system so the primary constraint system and the accumulator are together into a new accumulator and so the output of every IVC step is symmetric with its inputs is oh sorry the satisfaction of this secondary constraint system can also be similarly represented as a green instance and so now we have two function outputs a secondary instance sorry a secondary element which represents a satisfaction of this secondary constraint system but also two new accumulators which have now

folded um the prior two green instances and so let's say this was the final step of the IEC prover what remains for the prover to show to the verifier is that these elements here are indeed valid Elements which accumulate the claims of all prior instances I won't go into that but these accumulators along with that proof that these are valid accumulators represents the proof of that the IVC proof at the ice that the IVC verifier actually accepts cool so now that we have a rough

intuition hopefully about how the IVC approved operates and how the IFC verifier verifies the execution what was the vulnerability that happened in the modified IVC scheme well the structure of the IVC proof could actually uh sorry the structure of the vulnerable IVC proof allowed it to be split into two independent halves a left half and a right half you can think about these as accumulators for the primary and secondaryances but also the fresh green instances for the primary and secondary and now that vulnerable verification equation took in this vulnerable proof

and could actually be split into two independent checks for the left and right halves of the proof now because this verification was missing some critical hash checks is what allowed it to actually be split into two independent checks and now is the fact that they could be split into two independent checks which allowed for a sort of symmetric attack which we'll describe in the next slide so it turned out that because we could split the verification equation into two halves we could shortcut the computation in particular the IFC prover only had to execute a single step of the the honest nov approver but instead on malicious inputs

and now these accumulators along with the proof that they were valid accumulators represented the malicious left and right halves of the proof and because certain hashtags were missing from the modified Nova verifier these were accepting proofs and so the takeaways of the presentation today hopefully are that modified modifications to even secure schemes or even slight modifications to secure schemes can lead to completely broken schemes and as cryptographers when we make modifications to schemes we should prove that the modification is secure or at least write down a formal description for people to analyze and as

implementers if a scheme has never been written down formally nor proven secure we should definitely question its security but also question whether we should pour so much effort into implementing it and so for further exploration I definitely recommend of course reading our paper which is available on ePrint on this little short link here if you want instead to watch a technical Deep dive lecture on how the new Nova IVC approver and verify actually work but also a formal description of the sound's vulnerability walking through the attack I recommend watching our uh or watching a lecture I gave to the Privacy scaling aspirations group available on this YouTube channel

and that's it [Music] [Applause] any questions uh thank you for a great talk and three the Fantastic paper I can truly say it fantastic because I personally spent several months reverse engineering Nova from the same perspective as you did but I didn't discover the bug so I'm surprised the question actually is how should we prevent this kind of attacks in the future I mean in general not for this particular Nova paper but in general for proof systems who uh inevitably switch from uh single domain

to cycles of curves or something like this how how should we design new proof systems to avoid this kind of bugs what do you think I guess the first off is if you're trying to generalize some IBC construction based on folding schemes from a single curve to a cycle of Curves I recommend just following the construction we have in the paper so the construction the paper only assumes a generic following scheme not particular construction and so you can just go ahead and just use the the paper construction otherwise if it's some other proof system I definitely think there's no easy workaround you just have to write out the formal description and write a soundness proof and so I don't know if there's any way around that

but as implementers maybe you could request that the cryptographers uh you know write the proofs for the paper you mean right the soundness proofs for the two curve version yes exactly describe formally describe the two curve version and then write a sound as proof anyone else oh uh hi so so uh just to see if I followed so the you could say the the bug was only in not including enough data in the Fiat chamir challenge you could

characterize it like that or oh yeah so this wasn't actually a Fiat schmear bug so I include the full diagram but I didn't actually describe the full diagram uh basically the issue is that um in the actual construction you needed to check whether two accumulators were valid and hence all prior uh executions of those prospective constraint systems are valid but the issue is that they provided too much information actually they provided both accumulators but they never checked uh the x0 hashes which for both of these accumulators and because of that there was no guarantee that this first accumulator was the result of an extraction of this sorry how do I say it uh

in the diagram I presented a very like linear sort of diagram but the modified node implementation instead viewed it as not a linear but as like a pair that we're progressing and so instead they provided this um only this accumulator oh sorry this fresh instance and that accumulator and this uh and then this fresh instance and that accumulator and they checked them independently but the thing is though you don't actually need to provide this accumulator here you only have to provide the last one and buy a knowledge soundness you can actually extract the other accumulator and so there was a

right yeah and so what ended up happening x0 here is a random challenge or uh oh sorry my bad um basically when you operate on a cycle of Curves they wanted to keep the instances and the constraint systems content size and so x0 actually hashes the prior instance so as you can see as I followed here by Red I'm saying like um instances that were not satisfiable were like placed in the hashes so this red line is sort of where that broken accumulator went and so you would say for example if you included UI one in the hash uh in the public instance of

R1 CS2 or R1 cs1 I guess then that would that would fix it uh yeah it's just yeah they were missing a hash check yes so so uh there is an easy solution which is that you could just add an additional hash check but it turns out that you didn't actually need to include this extra element at all and so hence the the fix that you optimized this and so now there's like one less instance to check and it's because it's sort of inductively checked by the last constraint system oh okay and you're saying your optimization was you you only need to spit out one of the uis exactly exactly okay yes okay do we have time for yeah we do any more

questions no well oh oh there's a one question one more uh you mentioned that uh the verifier can be split into two independent uh Jacks when you fix the bug by introducing the hashtags is that still true or was that the problem that it was splitable in the first place yeah so if you introduce an additional hash check then the verification creation uh cannot be split into two independent house because now one half depends on the other half because this hash check but the issue is that um I say it you didn't

actually need to do that hash check in the first place because simply by omitting the elements as I described earlier you don't have to worry about there being an independent half and so the new proof after the fix doesn't have two halves you can split I see makes sense thank you oh there's a all right uh yeah I hope there's there's so hypothetically say they did all the Fiat Shamir stuff they delegated it to some Library like all right Merlin that does feature always correct would that have avoided the bug oh so if all the feature stuff

was handled by another library that oh so this is that this is not a Fiat smear bug this is just the hashes are just to make sure that the instances are constant size and so they provide the rest of the instance in the witness but then the public instance is just a hash okay so it wouldn't all right it's about what you okay yeah so it's like the choice of what you include basically and yeah uh yeah I guess but this is like outside of the constraint system it was just that the it's like the proof had two independent Haves and the verifier didn't check that these halves were together but it's outside of the actual concern yeah but some somehow I still I mean I don't follow the full detail I still wonder if right you had some Fiats

from your library that always has this transcript object that it keeps in mind if that would have somehow indirectly like brought the bug up to the surface I'm not totally following the details so maybe what I'm saying is nonsense oh no that's interesting I think I think the proper way would be to maybe Implement some generic object using our compiler and then just plug in plug and play whatever falling seam that probably would have prevented this issue um but these um but like before this paper The View was that you would do a pair of constraint systems um in parallel instead of a linear chain but I think this linear chain is the uh the appropriate View and it didn't occur before uh the discussion yeah but I'm

saying right there are these fiatremier libraries that always have a one transcript object that they're keeping in mind so I'm okay this is too complicated it'll take it offline yeah yeah here Okay so all right we still have a couple of minutes oh okay well I guess no I get man I guess I ran through those slides yeah see real quick okay quick and concise we can do one more question or we can move on to the next talk oh yeah yeah I gotta edit this you know

I don't want to dub you yeah I guess they don't have a single fetched hamir for the same reason they don't have a single curve basically you this object should reside in either field if you have like a state uh where you accumulate everything then it should be non-native demand domain for either of the field so if they had like such a state they would be they would be tempted to have like two feature mirrors in parallel and they have pretty much the same problem library that ensures you know that the challenges have to all the right thing in the free image it would I think it would it would force to have that actual

line in the in the implementation it wouldn't compiled um I think I agree with you in terms of the general implementation construction um but yeah the I don't know if it came up because I didn't have the microphone but the the question I'd asked before was was this uh effectively a missing constraint um now you said it was outside the circuit um but so is that purely because the the real input the real instance variables even though they're in the witness are still public so it takes a lift out of the circuit because there's no need to check it exactly yeah yeah so um so in the modified scheme the constraint systems actually remain the same and so it wasn't um like a

fiatrimir issue or a set of missing constraints or malformed constraints within the constraint system it was just the verifier at the end yep yeah and it's because um as I was uh okay hopefully I was you know the lecture that I give the Privacy scaling aspirations a lot more in depth so hopefully that's a little clearer but it's because um yeah what's in that x0 hash is actually the opposite instances uh green element and so you the the verifier has all these elements and are able to verify the hashes themselves and so that as you were saying earlier and so so it's sort of a it Vin is sort of a hybrid between it it's in its connections of the sorry microphone so it's a connection of the uh it's the

flow between the proofs but it's not the flow in terms of like a standard interactive to non-interactive yeah exactly exactly yeah and so it turns out that you didn't even need to have this uh check and so then it's like it's it's now different so yeah all right thank you very much Wilson [Applause] foreign