ZK14 - VEIL: Lightweight Zero-Knowledge for Hash-Based Multilinear Proof Systems - Ron Rothblum

Transcript

Cool. Uh, hi everyone. Um, really great to be here. I'm Ron Rothblum. Um, I'm going to be talking about, uh, a joint work with some of my colleagues at Succinct, uh, Rahul, Tamir, and Eugene. It's called Veil. It is very much um, sort of related to Jakamo's talk. It's also about adding zero knowledge to hashbased um, and specifically multi-linear proof systems. um using a somewhat different approach where we're really targeting it for to be very sort of practical and lightweight. Even sacrif even if that forces to sacrifice an asymtoics as long as it's sort of practical and lightweight we're we're happy.

Cool. So um can you see? Okay. So now throughout this uh conference throughout this this sort of exciting week with a lot of events we're going to be interested in in proof systems and cryptographic proof systems and cryptographic proof systems are are really really uh cool because they can offer kind of like two things um or they come in two flavors where you might be interested in one thing and not the other or or in both. So, so what I specifically mean um so the first thing maybe that cryptographic proofs can offer is what's known as succinctness.

Meaning that you can take a very complex or long computation and give a very short proof uh proving that it is indeed correct and maybe you know have this proof also be very efficiently verifiable. And this sort of comes from a very beautiful line of works already in the early 90s showing how to do this in theory. And you know amazingly this has grown into this sort of like industry and something that's being done uh in the real world and securing billions of dollars. So you know that's really exciting. So that's the aspect of succinctness. Um you might be familiar with uh ZKVMs where you know even though they are kind of designed for succinctness they got the ZK part mainly out of coolness. Um and then ZK rollups um verifiable computation for all these

uh aspects a lot of things that we actually need say in the domain of blockchains all you really want is a syncness you want to sort of compress a computation so that's sort of one thing that proof systems can offer you the second thing which is really cool and that's kind of the the zk acronym is zero knowledge this amazing uh idea introduced already in the in the 80s by god vaser miki and rakov u so um turning award for it and the idea there is you know we already heard Jakamo's talk I won't repeat the same things you know sometimes when we prove stuff it involves our secrets and we don't want um information about our secrets to be revealed to whoever we're proving information and you know you have applications like anonymous credentials

that Jakamo spoke about which are actually deployed in Google wallet via this beautiful work by Frigo and Chelat which we'll we'll talk about um people are interested in anonymous payments private blockchains. So, especially I think uh in the past year there's been a huge husely growing interest in zero knowledge. So, we have uh you know in some applications you might be interested in succinctness in other applications you might be interested in zero knowledge and sometimes you might want both. And something you might uh be thinking about you know if you have succinctness you have sort of such a short proof how much information can can it reveal? Maybe just a sing by itself implies zero knowledge. And there is actually some

truth to that. But I what what I want to actually show you now is that in general it's not true. And to do that I'm going to take some inspiration from the air uh here in Rome. And I want to uh prove to you the following claim. We have here uh two pizzas. Okay. And you know here in Italy we you know people take uh their pizzas very very seriously. And my claim is that these pizzas are are different. They're not the same. Maybe you can already see it. I tried it out on my kids. They couldn't tell. No one is shouting. So I claim they're different. And I want to prove it to you. Okay? So I'm going to provide you a very very uh succinct proof that they're different. Here it is. Okay? That point

is different. Very succinct. I just needed to give you the coordinates, show you that the proofs are different. But is this proof zero knowledge? No. Right? You did not just learn that the pizzas are different. You actually learned the difference. You learned, you know, the literally the secret sauce of, you know, why the second one is better. Okay. So, succinctness by itself does not imply zero knowledge. And we have to kind of work in order to get zero knowledge. So, you know, I already have a succinct proof system. Let's say um it's not zero knowledge because, you know, you learned the secret sauce. How can I turn my succinct proof system and make it zero knowledge? And actually this question has been sort of asked for you know kind of decades and kind of the common wisdom is you know zero not is not you know you

add some randomness you pad here you pad there it'll be fine and there's truth to that um and it sort of it kind of feels like a solve problem. There are a lot of papers people have studied this it kind of seems like a solved problem in some senses it is. The places where it starts to be tricky is you know when once you become sort of more practical and you really care care about efficiency then you know you start reading the off-the-shelf solution that claims that it's asytoically optimal and everything is great about it but then you know it says it has a linear time prover but then you know you go into page 38 and you realize that actually this uh linear prover is actually twice like 2x more slow than if it were not zero

knowledge. which is unacceptable uh for us nowadays. So you have to be careful with like what off-the-shelf solution you want to use. Um there are more recent works including the one uh this exciting work that Jakamo just talked about which really really tries to push the envelope uh and do things very very optimally. We saw some kind of very intense slides at the end showing you that it's it's non-trivial. It's it's it's kind of hard. Um it's hard to implement. It's hard uh it's hard to invent but Jakammon co-authors already did that but it's then hard to implement hard to audit hard to maintain and the question is whether we can do something that's kind of more lightweight okay so you know before going into our solution I want to kind of cover two

main approaches um that we have nowadays to how to zky a proof system approach number one is what's known as proof composition and the idea is the following so you take your succinct proof You know, if I were to just send it to you, you might learn interesting information. So, instead of sending you this succinct proof, which I'm going to call an outer proof, I'm going to generate an additional inner proof which doesn't prove the original computation. Rather, what it proves is that the outer proof exists. Okay, so there's an inner proof. This inner proof is ZK. So, you give an inner ZK proof. proving that an outer proof exists or that the outer verifier would have accepted. So the

outer proof system is succinct, the inner proof system is ZK and when you combine them, when you compose them, you kind of get the best of both worlds. So so that's kind of great and this is like very widely deployed. But in practice if you look at um ZKVMs for example um like R ZKVM SP1 you know the proof system the the main proof system itself is not zero knowledge but what you can do at at the very end uh sort of wrap the proof using something like gross 16 or plunk to make it zero knowledge okay so that's kind of the approach of proof composition the um maybe different approach which is kind of related to what Jako was was speaking about is to just you So take your proof system and kind of add armor

to every single point ZKI each and every component in your proof system and this is something that you can do. Um I think in the univariate case this sort of we have pretty great uh solutions by now. It's kind of a solved problem. So you can do it and uh to the best of my understanding it's it's not too complex. It's it's fine. In the case of uh multilinear hashbased schemes it's more complex. You kind of have more uh components floating around. You have sum checks, you have your your GKRs, you have your proximity tests and you can indeed go and optimize and like ZKI each and every one which is sort of what Jako did uh in described in in in his talk but it's in it's complicated. Okay, but two competing approaches proof

composition or ZKI everything. So what are the trade-offs? So in the composition approach the thing that's really nice about it that it's very simple and modular, right? you can kind of like optimize to death your succinct uh ZKVM not worry uh too much about you know ZK and then at the end you just run your inner ZK proof system it's totally separate modules when you like change your uh outer succinct uh proof you don't need to worry about auditing maintaining and so on the inner proof and vice versa um so that's the the benefit the two problems I have with it first it is costly because this uh inner ZK proof system needs to prove the

verification of the outer succinct proof. But you know in the hashbased uh world this uh proof is going to involve a lot of uh hashes particular Merkel paths. So the inner ZK proof system turns out to be kind of quite expensive. Okay. So that's kind of uh overhead that we don't like. The second thing is you know I told you we need a ZK inner proof system but our goal was to build a ZK proof system. So where am I getting this inner zk proof system from? And you know if you don't care about uh postquantum or don't care about assumptions then you might just do gross 16 but I do care and I think you should also care about postquantum and in this case it's not clear what proof system to use. Okay so that's the issue with proof composition.

What about zk everything? We already talked about it. You can get uh fantastic asmtoics um using uh Jako's new work. you can get it uh very concretely efficient but it is it's complicated and you need to touch each and every part of your proof system and once you go from like were to word 2.0 or 3.0 you will need to kind of redo everything. So what we would like is to get the best of both worlds. Um and that's what we try to do with this work veil. So it's a lightweight uh non-intrusive ZK compiler that sort of takes a large class of hashbased multilinear proof systems and can make them zk. Um it is sort of combines in a careful way both of the approaches both

composition and zki everything. Um what we are aiming to get is kind of avoid like a 2x proverhead. So proverhead that's only additive uh and quite small in practice. It is purely hashbased. It's plausibly postquantum, no annoying trusted setups and so on. Um, it is very heavily inspired by Abby and Mateo's work on the u Google long fellow and it's formally verified. I'll touch upon that at the end of the talk. We also implemented we gave a p uh implementation of this. So we just sort of had a basic nonzk uh inner product check proof system and then we benchmarked it when we sort of compose it with veil or not.

uh the overhead of composing with veil um was very small for the prover uh a little bit larger but still manageable for both a verifier and in terms of the proof size. Okay, so I want to tell you a little bit about how how we do this. And I guess I was already uh zooming in, but good to highlight that throughout this talk I'm going to uh focus exclusively on hashbased proof systems and specifically on multilinear ones, not versus univariat proof systems. And these proof systems tend to follow a very common pattern um which is the one that we deal with and I guess Jacob also talked about it in in his talk but the framing is as

following. You have in the beginning you sort of commit to your trace and the commitment is via what's known as a polinomial commitment or PCS. So you commit to your trace and this involves sending some oracles. After you send your oracles you prove stuff. So you run some checks or GKRs or stuff like that. At the end of running the you know this proving stuff phase what you get will be a multilinear evaluation claim on your trace and the last thing you do is to uh prove this multilinear evaluation. Okay. So that that would be the PCS opening.

Okay. So that this is kind of the common pattern for uh multilinear hashbased proofs. Commit GKR sum check whatever and then uh open. Let's talk a little bit more about how the uh PCS looks like. And again, this should remind you of Jakomo's talk. So the way that um sort of modern multilinear PCs work uh work is that you take your trace. This is the interle codes that Jako was talking about. You take your trace, you put it inside a matrix and then you take each column of the matrix and encode it using typically the resolment code. Okay. So apply something like an FFTD.

Okay. And then um this entire encoded matrix you send over as an oracle. That's the the commitment to your trace. Um so that's the commitment. When you want to do an evaluation, we do our favorite trick which is to choose a random linear combination of the columns um and then apply a proximity test on this random linear combination. Okay, so this is kind of the typical uh setting. Um and you know our goal in veil is to compile any such proof system and make it zero knowledge. By the way even like complex systems like a ZKVM can all be framed exactly like this. So SP1 hyper cube the newest one uh can be viewed this way.

Okay. So you know we understand how the succinct nonZK proof system looks like. Let's see what is the the the secret sauce that can leak when you just run it as is. So first of all um when eventually we'll run the proximity test we what we'll get are oracle queries that are openings of rows of the encoded matrix that we had on the right before and these are actually in some sense the scariest part because they are kind of most directly related to your trace. Um so these are sort of direct row openings that we're worried about. Second thing that we're worried about is that throughout all of this like proving stuff phase, everything we send are sort of proofs in the clear, they involve some computation involving your trace.

We don't like that. Lastly, when we run the proximity test, you know, we've uh we've introduced some randomness by the random linear combination, but still it's not a lot of entropy in the system, and it's not clear what can leak from the proximity test as well. Okay, so sort of three potential sources of uh leakage of information. So we have these three sources of potential leakage but kind of our I think our main insight with veil is that there's this curious uh asymmetry in terms of the leakage. So the protocol roughly has two parts. There's the PCS which we had like commitment in the beginning and evaluation at the end. Um and that part actually if you look at

the eventual proof is by far the most dominant. So in hashbased proof systems usually just the opening of these oracles is by far the most dominant part. So that is uh by far the large part. The se the the second component which was the middle one the proving stuff that's usually very short right there. These sum checks uh GKRS these are very very efficient protocols. They're very short. So it's good to think of you know the PCS part of the proof is maybe 95%. The sum tricky parts are maybe 5%. Okay, so that's um sort of the sizes between when you run your multilinear hashbased proof system, the ratio between the sizes.

However, on the ZK side, when you think about ZK a little bit, actually protecting the PCS, which was this 95% of the proof, turns out that you can do that with very simple techniques, especially if you're uh not targeting optimal asmtoics, but just like very very practical numbers. That's easy to do. The thing that turns out to be tricky, annoying, and complicated is protecting this part that is only like say 5% of the proof. Some checks and GKRs. There's been a ton of literature about this because it is complicated um buggy. There have been bugs also around this. Um and yeah, so it's it's kind of like interesting where 95% of the proof is easy to ZKFI, but 5%

is annoying or difficult. Okay. Um so let's talk about how how to zky these components. So starting with uh with sort of the PCS we said that the first potential leakage are these oracle queries that we have reading entire rows of the encoded uh of the encoded trace. And this turns out to be quite easy to solve as promised and the idea again Jakamo uh already talked about it is to add some padding to the trace. So you take the trace, you add a tiny bit of padding, a tiny bit of extra rows, say 100 or so extra rows, and you apply the read Solomman encoding to that. Once you do that, turns out that because read

Salman is what's known as a ZK code, just by adding these 100 extra random uh padding rows, it means that when you read your 100 rows from uh the encoded matrix, you'll just see random stuff. Okay, so no leakage there. So just padding as we said in the beginning of the talk just padding solves this problem. So that's good. Let's oh uh just in terms of like concrete overhead here um right so if uh eventually you're going to make Q you want to make Q queries uh read Q Q rows think of Q as about 100 um or 128 here then it means that your distance just drops from like whatever it was

before delta now it's just going to be delta minus Q over M. In practice, instead of delta being one half, you're going to have your delta be 0.49999. So kind of very very lightweight. Cool. So that's about hi hiding the queries into the rows. Let's jump uh jump over the second part which was the annoying one and talk about the proximity test. Right? Remember what we did was take a random linear combination of the columns and run a proximity test on that. How do we protect that? Well, again easy and again same solution pad. So what we'll do now is just add a random column as well. The effect will be remember that the encoding is just

column by column. So the last encoded column will be an encoding of random junk. And when we take a random linear combination of the encoded columns, the result is again going to be just random because once your random linear combination involves a random column, it will be itself random. So super duper easy and that protects your proximity test. The overhead here and this is uh worse than what uh Jako had say about it in a second is if we originally had something like t columns we need to add one extra column so the overhead is kind of this one plus one over t very practical numbers would again have t be 128 meaning that the overhead is maybe 1% or less.

Okay, cool. So, component one, easy, component three, easy, component two, oh, before that comment here kind of if you think about it, we added this entire random column, but then ran a proximity test which only revealed very little information about it. So, we were somehow like putting in way too much entropy by adding a full column because only a little bit of information would be revealed in the proximity test. So, it feels like an overkill and indeed it is. And that's what Jakamo shows. But in practice, who cares? I mean, this 1% is fine. Okay. So that's uh yeah. Okay. So that's you know the elephant in the room is we have all these sum checks, all

these GKRs. They're a tiny part of the proof, but they are the hard part to to protect. So how can we do it nevertheless? Well, the our observation here is that all that you have in these sum checks and GKRs is just algebra, just you know, very very simple algebra. In fact, most of it is purely linear. Um, and this phase we already said it's really short, less than 5% of the overall thing. And it doesn't involve any cryptography. There's no hashing, none of that. Just pure simple algebra. It's just field arithmetic. So in this context, composition turns out to be actually very cheap. Okay. Okay, so the idea uh in a nutshell will be that uh just for this phase in advance the

prover is going to commit to an additional short vector R. Now when running your GTRS or your sum checks, you're going to one time pad all the interaction using R and then at the end so you've kind of like masked the entire interaction and run an inner ZK proof proving that you know if you were to uh cancel out this one time pad the verifier would have accepted and this is where we actually do use proof composition. But the key insight is that we're doing proof composition to a statement that is purely arithmetic. It does not involve any hashing. Okay. So it's quite lightweight.

Yeah. Okay. So again, we're running this inner zk proof system on a statement that's purely algebraic, very succinct, um doesn't involve hashing and actually vastly dominated by linear checks. Um, and because we're doing this, you know, we're proving this like 5% proof. We don't care if the inner proof system, even if it were say to double the length, you know, you double your 5% overall the tax you pay in proof size is going to be 5%.

Yeah. So just like the the high level view of the veil protocol, we start off by an interled readment code. I guess the the order of the two first two bullets should be uh flipped. We pad each column with you know a hundred or so random field elements. Um we add one extra random column. We encode all of this using an interled read solomman code. Then in preparation for phase two we additionally commit to a random vector R. We run our sum checks or whatever masked with R. Then sort of in parallel we can run an inner zk proof proving that if you were that you know the commitment to R is a commitment to a string where if you unmask the

interaction using what's there would have made the verifier accept and you run your your uh PCS evaluation which can be vanilla based fold were whatever it's being run on a totally random vector so you don't mind. Yeah. Um so you know one thing I haven't told you is what is the inner proof system that we're using right in order to prove this like unmasked GKR let's say um and the observation is again we only have um very simple algebra that we're proving so you can frame it as an R1CS like statement and you can try to use an off-the-shelf solution so a proof system that would work great here is the Lgerero proof system um which is the

kind of precursor to the company but it's a it's a proof system um And that proof system is zero knowledge uh out of the box and it also gets bonus points for being partially succinct. It has sort of square root succinctness. So leg would work well here. We actually uh implemented in some sense a variant of the leg. Lger works sort of in matrix form. We just worked in a vector. We found it uh easier to do and it's uh sort of our because our setting has way more linear constraints than anything else. It turned out to be a little bit uh lighter weight.

But we mainly did it because it was simpler. Um yeah, in terms of the let me skip the asmtoic overhead. Today we're in practical mindset. Um yeah, in terms of benchmarks, we already saw so we benchmarked this on like different size uh like statements um for kind of as a statements grew the overhead became uh smaller kind of as expected. In particular in 2029 we have this 3% proverhead. verify overhead is 22% and uh all additive and 12% proof overhead.

Um yeah, one thing I want to kind of briefly point out is that when using veil inside improving a ZKVM, you should be thinking about it a little bit differently. So usually what ZKVMs do is that they break the computation into multiple shards, prove each shard separately and then combine them via 2 to1 process. The point is that all of this can remain exactly as is. It doesn't need to be zk just at the root of the tree. You can just make that part be zk. So you're only suffering this like zk overhead once at the end. Moreover, something I want to point out is, you know, if you're unhappy with our 12% overhead improved size, what you can always do is that once it is already zk, you can do,

you know, nonzk further compression. So, if you want, you can also do that. Yeah. Let me briefly mention formal verification. Um, so kind of this fun uh post we saw on on Reddit uh posted a few weeks ago about Veil. Maybe it's from someone into the room. If so, please let me know. I'd love to know. Uh saying the following analysis of the ZK property seems really nasty in these systems. Airgo, they are likely to have major ZK failures. Um yeah, so thanks for the comment. Um which you know I partially uh buy in the in the sense that you know arguing intuitively that system is ZK is

usually not difficult. Formalizing it is hell. It is not fun. um you know very simple protocols if you look at the the their proof of zk it's pages and pages and it's it's it's a mess so what we we did as sort of an experiment with veil is a formal verification so we sort of uh using a lot of help from our our best friend Claude um we had kind of like under close human supervision translated all the the theorem statements and definitions from the paper into lean and then used claw to generate proofs uh based on the paper but you know once you have the theorem statement it's all formally verified so you can check.

Yeah. And uh was kind of a fun experience and you know uh Reddit posters all around the world can can be happier. Um yeah one maybe interesting point and this actually caught uh I would say minor but not insignificant bug where because we were not careful um this DK property was only statistical rather than perfect. Um but you know with uh after this was pointed out we fixed it to be perfect. Cool. So just to summarize um Veil is this lightweight and we think non-intrusive ZK compiler which you can kind of like tack on to an existing nonZK system. Um

the modifications are kind of fairly minimal. you um do this kind of like padding which we already know is good to your trace and you just run a lightweight inner proof system on on the sum checks let's say um purely hashbased plausibly postquantum pretty minor overhead from our PC um yeah and the paper the code and the formal verification are all online and if you're interested to hear more please let me know ask me questions uh at any Yeah thanks.

>> So, I think we have time for one question. Oh, I'm gonna Sorry, I'm going to take the one that's a bit closer. >> Um, so I think the formation part is very very cool. But I think when I looked at the potentially partial work that Tamir sent over maybe two weeks ago, there were quite a few things that were aimatized even like somehow the mar code stuff wasized and so I don't know if you have plans to try to flesh it out and I think Sony maybe with respect to the definition of ZK um it would be interesting to try to do go the whole way and do ZK from the very basics that you'll see in you know the textbooks and things like this beyond just taking the statements from the paper and I don't know if there are any plans or ing how

you feel maybe as a serist of going from single paper statements to trying to fit it into the broader abstractions. >> I see. So, so you're asking about the formalification being only about sort of veil rather than you know all of SP1 compiled with veil to be ZK. Is that sort of the question? >> Um so, so I think if you were to define zero knowledge on paper, you would go through a bunch of different abstractions, right? Uh that are not I think in the formalization you have if I understand correctly. And so I'm asking I guess what your opinion is on um what the delta is maybe between having all of these foundational abstractions that you have from the Siri literature to having what you have for a single paper. Right.

>> I guess I'm not exactly sure what you mean. So maybe we can talk about it after and discuss. Yeah. >> All right. Well, thank you so much Ron. Great.