ZK10: Fiat-Shamir security of FRI and related SNARKs - Albert Garreta (Nethermind)

30 Sept 2023 · 27:35

Albert Garreta of Nethermind presents at Zero Knowledge Summit 10 in London on the Fiat-Shamir security of FRI-based SNARKs, joint work with Justin Thaler, Jonathan Katz, and others. The talk covers why FRI cannot serve directly as a polynomial commitment scheme, the soundness properties needed to safely apply the Fiat-Shamir transform, and results proving that Plonky2 and ethSTARK are secure as non-interactive protocols.

Speakers

Topics

Transcript

[Music] okay uh thanks for the introduction and also thank you for the invitation I'm really glad to be here and have the opportunity to talk about our work with FR Bas around FR Bas Nars so this is Joint work with the researchers that appear here and let's begin with defining terms so what is a Fred based Nar so it's a kind of a loose term that for the purposes of this talk I will use to have the following meaning so a FR Bay snark will be a a snark that is built following the this re the

following recipe which is you take a piop polinomial interactive Oracle proof you compile it with fry and Merkle trees and then you do the fu transform so if your snark is built in this way then it we call it Fred Bas snark so so just uh to set up some notation and terminology let's review what's a piop in a piop it it's an interactive protocol there's a prover and verifier there's a problem statement and a witness the witness is only known to the approver and then the prover and the verifier exchange messages for a certain number of rounds and uh yeah and then the verifier takes so so the the particularity of um a piop

is that the messages that the Prov sense are polinomial of low degree so the the Prov sense polinomial of low degree and at the end of this interactive phase the verifier opens these polinomial at random points and then based on whether or not these opening satisfy some algebraic relations it accepts or rejects the proof okay um a key point in poops when one analyzes the security of of poops is that you assume that the maps that the Prov sends are polinomial and it this is a key assumption so you assume this and then you prove that the piop is secure under this assumption

and this is actually a very strong assumption which makes um the security analysis of poops relatively easy I would say usually if you've work with with poops or read some papers on them you you usually end up finding an a statement of this form so you start analyzing the security of piop and you end up proving that unless the verifier is very unlucky and sends a route to some low degree polinomial then the attacker cannot break the protocol for sure and then you use this barle LMA which says that degrey polinomial have a few number of roots and you get that the attacker can break the protocol only with a with negligible probability so

the degree of the polinomial the maximum number of rules it can have over the size of the challenges the verifier can send so analyzing the security of piop is relatively easy because they rely on this very strong assumption the assumption that the prover sends um polinomial so this is very nice analyzing P poops is like P the piop is a very nice abstract framework that um facilitates reasoning about the zero knowledge proofs but in practice poops are not usable there's several issues with them first of all how does the verifier check that the maps it receives are low degree

polinomial like one thing it could do is to check all the evaluations of the maps and see if they if they um are consistent with being a polinomial but this would make the verifier extremely slow another uh issue is that the maps are too large to be sent so you cannot just have the provs and the maps and this would make the proof size huge and it would be be very similar to the to the pr just sending the the witness altogether so the typical solution to this issues are to compile the poop with a polinomial commitment scheme in which the in a you take the piop take a polinomial commitment scheme and replace

the messages that the prover sends by commitments to the polinomial so now the prover instead of sending polinomial sends commitments and recall that at the end of the interactive phase the verifier opens the polinomial at some random points now the verifier has commitments so it cannot just open the the commitments so it interacts when it wants to open one of the maps it interacts with the prover um according to the specification of the PCS and opens the the polinomial at the points it wants to to open them so examples of pcss are the kg1 the inner product argument based uh pcss and Fry based uh polinomial

commitment schemes though we will discuss we will talk more about FR based polinomial commitment schemes because in the literature well not in the literature but practitioners often use them as if they were pcss but they are not actually pcss unless you configure them in a very restrictive way which makes fry um quite slow so in practice the way fry is configured um makes fry not be a PCS and we will come back to this later and it's one of the key points that we address in this work so you have the piop you have the commitment scheme and now there's a theorem that says that if the piop is

secure and the polinomial commitment scheme is secure then the new protocol is secure U so you can design your piop prove that it is secure that's easy relatively easy as I argued before take a PCS which is from the literature which is already proven secure you compile it and you get a secure protocol so if you follow this recipe you get it's it's kind of easy you get a secure uh succinct argument uh just by looking at the piop okay and the so in a f Bas Nar the the we take a piop compile it with fry and Merkle trees let's pretend that fry and Merkle trees

make a PCS which do not but let's pretend it is and then we apply the FIA chamir transformation and for in the interest of time I will not go over the Fatam transformation probably everybody know everybody here knows how it works the idea is that you replace the the the challenges the verifier would send by hashes of all the messages exchanged before and if you model the hash as a random Oracle then it's as if if the prover is simulating the very fire okay yeah um so I'll just mention some examples of fry based Nars the most welln example is Stark the Stark protocol uh from starware and then

there's a flurry of other protocols now that can be seen as Fred based Nars for example plony 2 which is you could say it's plun but changing the fry protocol changing the kcg commitment scheme by fry and plony to Z bu are kind of similar protocols that um that do this okay so there's this recipe and our work analyzes two potential pitfalls one is around the F transformation of protocols and the other is as I mentioned the issue that fry is not really a PCS a a commitment scheme so let's discuss FIA chamir so in general you can have an interactive

protocol and then you can consider the F transform of the protocol and get a protocol that is not secure so you can have a very secure interactive protocol FIA chamir transform it and get a disaster as a result there is a wellknown example which is the sequential repetition of a smaller protocol you take a protocol with sound error one half repeat it two times and the interactive version of this repetition has a soundness error one over two to the T however if you do the F transform of of this new protocol it's a disaster like the security is basically one half very roughly speaking you almost

gain nothing from sequential repetition uh there's another example which is less well known and actually was described very recently last year which is the par repetition of a smaller protocol and I will focus on this example because it's less well known so what do I mean by by par repetition let's assume we have a small protocol Pi Z which has 64 bits of security or 32 bits of security and we want to increase its security by repeating it in parallel so we create a new protocol where now the prover instead of sending one message as it first as its first message it sends two messages and the verify replies with two challenges and

so on so it's just like executing Pi zero but with two threads in parallel and the verifier accepts the proof this proof even only the verifier in pi Z would accept each of the columns as a valid proof for pi Z so this is the 2x par repetition of of Pi 0 which I denote pi and this cartisian product so now I'll explain why if you do if you build so if you if you consider the inter active protocol obtained in this way the security is quadratically larger than the security of of Pi Z if the soundness error of Pi

Z is Epsilon the soundness error of this one is Epsilon square but now I'll argue that when you do the F Shamir transform the soundness error is Epsilon pretty much two times Epsilon so how can an attacker um attack this par repe parall repeat protocol so here there's B but there should be approver because now we are in the in the F Shamir setting okay so this V is just Computing the hash of previous messages so the attacker proceeds as follows it chooses any two messages first messages M1 and M1 Prime and it computes the challenges by hashing the

previous messages and now comes the key point which is it checks if the first component of the challenge is a special challenge that would allow the pr in the small protocol to break the protocol so to make this more concrete if you have work with poops for example you've probably seen that if the verifier sends you a root to certain polinomial then the pr can break the protocol that's typical situation that you don't want the you you you make sure that the verifier can um that it is very hard for the verifier to send you a root

because if you make sure of that then it cannot break the protocol so imagine that this C1 is a root to to this type of polinomial so if this C1 the first component is a root it means that if it was only execut if prover was only executing Pi Z it could break by zero so the pro comput the challenges and tries to and sees if this C1 is special if it is uh then it moves to the next phas to the next light otherwise it repeats and goes back to Step One chooses a new message gets new challenge and checks again if the new challenge is the first component is

special and in expectation it needs basically to to the land iterations to succeed where land is the security parameter of the interactive protocol uh that's a very rough and loose uh statement but just to to simplify things basically what what the prover is doing here is breaking Pi 0 and if Epsilon is the security of Pi Z well it needs to to make at least this amount of of uh of repetitions to in expectation make sure that it gets one of these roots okay so let's suppose that the pro has managed to get this special first

challenge how does it proceed well now it and now the first threat is basically broken the pr knows how to complete the first threat and get a valid proof for the 4 Pi Z what does it do next it um for the first threat it will choose messages and messages in a way that it allows it to to break this threat of uh of Pi Z and it chooses M2 Prime arbitrarily it proceeds like as before it computes the new challenges and again it checks if the second component now of the new challenges is a special challenge that allows it to Break by

zero so again for example it's it checks if C2 Prime is a root to some polinomial that allows it that would mean that the pr breaks the the protocol by zero if it gets this special challenge it it is happy otherwise it goes back to this step chooses a new M2 Prime gets new challenges and so on so again it needs about two to the Lambda iterations where Lambda is the SEC the bit of security of the small protocol and what happens if it succeeds in the two steps it gets one uh one column which contains a valid proof 4 Pi 0 and another column which contains a

valid proof 4 pi zero so the verifier accepts if the prover succeeds in these two steps the verifier accepts um yeah and we saw that succeeding at step one requires to do the Lambda work and succeeding ad step two requires to to the Lambda work so in general theover needs to make two times two to the Lambda work so two to the lamba plus one work so in a sense the the security has only increase by one bit but we were expecting it to increase by two times because the interactive um the interactive version of the of the par repetition has this

soundness so using the par repetition has done nothing basically it like you repeated the protocol in parallel applied the F transform and didn't gain any security essentially and I'll skip this for the interest of time so okay we just saw that you can have a super secure interactive protocol apply the fmu transform and get a disaster so this raises the question when can we be sure that if we apply the fu transform we get something that's as secure as the initial protocol and the answer for example you can do several things but one of the things you can do

is prove that your initial protocol the interactive one satisfies uh some strong notion of of security you can there are several to choose from but the typical one is special soundness if you prove that your protocol is special sound which I'm not going to Define now then the F transform of the protocol is roughly speaking as secure as as the initial protocol Sor and you can also prove that uh you can choose a different type of of security notion of strong security notion for example round by round knowledge soundness or round by soundness if you prove that your protocol satisfies this notion then the resulting F Shamir transform protocol is

roughly as secure as as the initial protocol and just to give a since round by round soundness is a bit less known than special soundness I'll try to give an intuitive idea of what it is without getting into formal into the formal definition so in the in the example example of par par repetition and sequential repetition you could say intuitively speaking that the overall soundness of the big protocol is the accumulation of smaller smaller checks um made during this big protocol so it's like you are accumul you you are making several

checks on the final soundness in the interactive version is the the conjunction of all these soundness but this is precisely what the fimir what the attacker in the fimir transform can exploit it can rewind proofs and try to break this small uh soundness uh checks this these checks that have small soundness and then the F transform doesn't work as expected so that's the issue with with these examples I gave and round by round knowledge soundness is a notion that tries to state that this this doesn't happen so it's the formal formalization is different than what I'm just saying

but this is the intuition of what round by round knowledge sound is uh says basically that the security of the protocol is not the accumulation of several uh checks that are not very secure so to basically to prove that your protocol is round by round sound or knowledge sound you have to end up showing that every check you make has the soundness error that you are targeting like if you are targeting 128 bits all checks should have 128 bits um and if you are wondering what's the relation between special soundness and round by round soundness in a recent uh paper we put on prep print we prove

these relations so round by round by round knowledge soundness is um the strongest it implies special soundness which in turn implies round by round soundness and we also show that special soundness does not imply round by round knowledge soundness so it's strictly more strong okay so now uh let's discuss fry so just to set things up in Fry the prover has a function uh in a field and the verifier can access the values of the function in some subset of the field and the pro the goal of the pro is to convince that is to convince the verifier that F the function is a

polinomial of low degree well that's that's what we would like that would be the ideal world but unfortunately f is a bit more complicated and the it only allows the pr to convince the verifier that FX behaves similar to a to a polinomial of low degree but not that it is a polinomial of of low degree and what does similar mean it means it's captured by the definition of delta closeness which which means that um FX is Delta close to a polinomial if it agrees uh with it on a relatively large subset of this D this domain and here you have it the math the math behind it it's not important for for our

purposes so one of our results is that the FY protocol is round by round knowledge sound this also implies that it is special Sound by the previous result I mentioned because round by round knowled sound this impli special soundness this was proved concurrently by starware they published it pretty much at the same time as we put it online and in particular it means that you can use fry safely with um with a f transform okay and about using fry as a polinomial commitment scheme so I mentioned at the beginning of the talk that this is a problem and I'll try to explain why now when

close so recall that fry proves that a map is close to a low degree polinomial when close is very close then fry you can prove that you can use it as a PCS a polinomial commitment scheme um the way you do it is you you use the typical kcg like check if you want to open a map that has been committed uh you use fry to check that this quoti is a a low degree polinomial this is kind of a standard thing in kyg and you also do this in in Fry here very close just to um be clear it means that the proximity parameter is within the so-called uh unique decoding radius

however this choosing Delta in this form leads into leads to a inefficient fry protocol that is not used in practice so in practice you never choose this proximity parameter to be so low and all all protols I mentioned before for example Stark plunky 2 risk zero they use a larger proximity parameter that goes up to the so-call Johnson bound and when you take this large proximity parameter then this protocoling here is no longer a a polinomial commitment scheme and the reason is that you can have many you can have multiple polinomial that are Delta close to to your map and this allows the

pr to open any of these polom so when when you query the commitment the prover can choose between a a certain list of of polinomial and gives you give you that evaluation so you are the pro is not really committing to a polinomial anymore it's committing to a list of pols and this is a problem this was studied for example in the rief work work on the context of using Fry on plunk however if you do the if you take the rief approach you get an issue which is that the soundness error scales exponentially on the width of the trace and for example planky 2 I think uses traces of uh with more than 100 so you cannot just

use red shift to to prove that plank2 is secure for example because you would get like the result you get is sound sound error of of two to the 100 which is not what you want and yeah and um also St St type tools attempt use uh fry so they compile poops with fry but they don't treat the fry as a PCS and this is a This was um there are several papers by starware on this topic recently urri Havok published a a summary or survey on on the fry protocol and uh he improv a little bit the

soundness estimates that appear in this in this uh in deep fry and start and all this work so here is our main result is um the main result of the talk is the following we describe a large class of P Ops with the following property so if you take a piop in this class and you prove that it is round by round knowledge sound or round round by round sound then the fry based narc that you you obtain from it is sound or it's knowled sound so it's a Nar with K and by fry based Nar I mean you take the piop use fry and Merle trees and then

the F transform so the key point the the nice thing of this result is that it gives a wide class of PS where to analyze the security of the final snark you just you don't need to leave the piop setting you can just prove that the piop is round by round sound or knowledge sound which as I argued at the beginning of the talk it's relatively easy and for examp an application of this strategy is we show that e star and pl2 as in the piop forms are round by round knowledge sound and that they are in this class the class of the theorem and a corollary then is that the that

these Protocols are knowledge sound and they have the knowledge sound that we expected them to have and for Star if Stark in particular this was also proved by starware concurrently and that's the the end of the talk thank [Applause] you questions was that clear oh there we go I guess I can reach over to you thanks for the talk so in that diagram where connected two parallel um protocols is it do they necessarily have

to be the same or could it be two different protocols but just applied independently they can be two yeah H different protocols for sure okay yeah the same attack applies do you know if that has like bigger implications for I guess other protocols that we use today like I guess yeah the the knowledge soundness and around or round by round says something about uh whether the protocol could be decomposed into those uh like independent chunks or independent provs yes but if you take the par repetition of a protocol or two protocols repeated in parallel and you prove that you try

to prove that it is round by round sound you will get a bad soundness error you will get the soundness error of the less secure protocol and that's it you and don't you won't G gain anything okay so that already captures that like that the around by round sound protocol can't be uh split into those independent Parts yeah okay yeah yeah have a question over that did we have a question in the back no oh sorry no no any other questions no thank you very much Albert

[Applause] thanks