ZK12: Memory checking in IVC-based zkVMs - Jens Groth

Transcript

[Music] yeah so so I'm going to talk about uh ckvm uh and I'll give a bit of introduction to these Concepts since um you there's a lot of teams and projects that are building ckvm and working with IBC and so forth um the problem I'm going to talk about is in ckvm if you sort like use incremental verifiable computation you sort of like slice the computation in multiple Parts those parts may be computed by different provs and then the question is how do you check that they have a consistent memory throughout that computation right because there might be a write in one

place and a read in a completely different place of that one um and it's a topic I've talked about before but there sort like a new twist be been exploring this concept of multiset hashing um and how efficient one can prove multiset hashing and it's one of the techniques that one can use to do memory checking um we go okay so so it's something that people have worked on uh before uh there sort like a a standard techniques based on Merkel trees which is not very efficient um but then there are also some efficient techniques the multi set hashing technique was uh actually came

out in in a paper in 2018 by setting um called spice um and then the other techniques uh to pass offline memory checking um uh which is quite recent um and if you want to know about that one you can check out my talk on on CK proof which was talking about that topic U and there's also a nice idea by by B and and Chen in in the paper approves for deep thought where they're sort like doing a Peterson commitment to the full memory and then just making sort like an update of Delta the changes of the memory in each step um at a low cost um okay so I'll start by giving

some some background uh to ckvm and and the problem that we are looking at in memory checking so let's start without the CK so a virtual machine uh is a machine uh that can take a as input a a program um an explicit input X and another input W and then it outputs some result and the question we are asking ourselves when we're building ckvm is why how do we know that this output why is actually true so the idea in a ckvm is that you would also output a proof that this has

been computed correctly and then there will be a matching verification algorithm that can take us input the program and and the input X and the output Y and and prove and check whether this is correct or not and it's important actually here that the then the reason I split the input in two parts right so the W input is not part of what the verifier sees and that's part of why you can have succinct proes that are much shorter than computation that you don't actually give that to the verifier and therefore the verifi doesn't have to read it and and the computation the verifier invest doesn't have to depend on the size of w so this means that we can have proofs

that are succinct that are really small really cheap to verify and cheap in the sense that the verifier has to look at the program and the explicit input and the output and the proof but not W okay if we Peak inside the ckvm typical design is that you would have the virtual machine um that produces an execution trace of every step that it executes and produces the output and then you have AAL that looks at that execution trace and then proves that there exist a valid execution Trace so every step in the execution Trace corresponds to a correct execution of an

instruction and those execution traces may be big right and Computing proofs is a expensive operation um so one strategy could be that you would want to slice that up and you would have multiple provs you would have many machines uh that are proving that this execution Trace is correct okay so let me so like dig into a little more technically speaking what happens here uh so this is increment verifiable computation concept that was proposed in

2008 um so think of this function VM as a state transition machine it's s like takes what is the current state it produces a batch of cycles and it outputs s like what is the next state of the machine and you can sort of do that in a sequence and there may be some auxiliary inputs as well right and at the end you would output y okay and there's a s like a lot of details into how you actually prepare that right so for instance maybe it's a big program and big input X right and you wouldn't want to give everything in one go so maybe you instead you have

some sort like digest of that and then you're not actually giving so like keeping that as state but you're instead sort like inputting that along the way as part of the auxiliary inputs Omega 0 Omega 1 and so forth so so you can for for the purposes of this talk think of the Omega as I saw like this is the execution Trace that we drip feeding into the c v ckvm and then you would have a Prov that sort like proves that the first iteration has been computed correctly and the next Pro would sort like consume the proof for the from the first prover and so like the next slice

of the execution Trace prove that is correct and so forth right and that way you accumulate these kind of proofs and you get a proof in the end that everything is correct so so let's look inside now what what is it that this machine does right um so so think of this as we have a virtual machine it has a CPU it has a random access memory and one way we could think of of this or like the naive approach and what people were doing in the early days when they were looking into their knowledge

proofs uh for for execution of of programs is that you have the state is everything that you have in the virtual ma machine so it have like a snapshot of what the register values of the CPU and so forth it would have like the memory uh and so forth right and then you execute it and it outputs the new memory and the new state of the CPU now this is super expensive though right because now you actually have to keep track of the full memory in each of these transitions right and and who knows how many cycles maybe you're executing a few cycles and then it's really costly proportionally speaking to keep track of

the full memory right and you have to place constraints when you're proving that this is a correct transition that constrains all of the memory right and a lot of the memory cells would just be unchanged but you have to say this one is equal to what it was before this one is equal to what it was before and so forth so so the natural idea now is okay let's try to externalize the memory so the state now will just be the state of the CPU what are the register values and things like that and where is the program counter

at but now we give the memory axises as external input so it would say look I was writing this value to address three I was reading the this uh value from address 17 and so forth okay and this reduces the cost for the Prov right because now we just have to keep so like the relatively small state of the CPU so like what are the registers values and thing where's the program counter at okay but everything else is has been externalized okay so you only pay for what you use right so you still have to prove something about the memory accesses you do make but you

don't have to prove something about the rest of the memory okay so let's um be naive and and go go with that straight away right what happens okay so now the initial state is just the CPU State and that's what we are progressing and now we've externalized the memory accesses so the memory would be so memory would be a batch of memory accesses some some reads and some writes memory one would be some accesses again to the memory and so

forth and we're basically giving that as advice to to the to the CPU okay and now we can run the Prov and we can prove that all of these transitions are correct now there's an obvious problem here right which is that if you're cheating Prov and you're running this system right you get sort like to choose what is the external input you would feed to each of these things that the provs are proving so you can feed them an inconsistent memory pattern right so you could have for instance a memory where you know you're saying to the CPU yeah yeah you are writing to this address

this value here and then a few steps later you can say oh yeah and you're reading from this address and by the way it's this value here which is a completely different value right and you will get out the wrong output from the computation but none of the provos will be know that something is wrong because their local view everything looks great right I mean you have some state of the CPU you have some memory accesses that you're getting from the external and you're doing the right transition right so the proofs will look great and the problem is that you're proving things

that Lo about the local transitions but you're not proving that that globally speaking the memory is consistent so that's a problem of of memory checking and and people have come up with several different techniques to address that um so the high level of these ideas is um we want to insert some memory protection for the CPU right so we still want to prove that the CPU transitions are correct and they're progressing correctly but then we need to give them some protection that also the

memory uh axises they get to see are actually correct so we can imagine augmenting the state of the CPU uh zi with a digest of the memory right so think this for now just as like a hash or commitment to the memory and then when we give the transition function these kind of memory addresses then let's also give it some information so it can check that these aises are correct so let me give

you um okay so so the big picture here then is okay so now with these additional checks with these additional digest when we do this incremental verifiable computation now we also have memory protection and now when we get out the correct proof for the result we know that both the CPU has executed correctly and also all the m memory access are consistent with one Global random access memory so let me give an example of how this could be done okay so think of a miracle commitment to the memory so we

start by giving committing to the full memory in a Merkle tree and we give the root as a digest as input right so part of the state okay that's just like small hash value so it's a very small addition to the state and now whenever you are accessing the memory we will not only give the accesses to memory but we will also give miracled paths to the root right now it's something you can for every access to the memory you can check that this is actually consistent with the memory that's committed in that Merle tree route okay and the cost is well so sort of the

logarithmic size of of the the memory we write is is sort like the length of this path right and you have to check each of those right and that's s like you know if if it's a large memory and you're only doing a few memory accesses and that's going to be cheaper than having constraint constraints for the full memory so so this is great it works um however it's inefficient right because for each access to the memory the Prov now has to prove that it's seen a Merkel path to the root of the tree and proving hashes is expensive right so it cost a

lot of constraints uh so we implemented this with posidon which is like a fairly friend CK friendly type of hash function right and we're talking about like hundreds of constraints that we have to uh Implement and to check this path here so the question is can we do better okay and the answer is going to to to be yes um so let me give you first a little bit of background is what it is that we really want to prove in order for the memory to be cons consistent so

here's a a common technique that is often used is to think of a a read set and a right set that tracks all the memory accesses okay and we will think of the execution as first we will do some initialization that's just where we're writing what is the initial memory in this case I only have two addresses in in here right then we'll have the execution okay and and when we do an execution if we load a value then we would read that value and then we will write that value back again okay so for every access to the memory we both do a read and a

write if we store a value then we will read a value and then we would write the new value that we're storing and the reason we're doing this is that well every time we write something to a cell then we update what is the time stamp when we accessed and what was like the last time this cell was used so when we have a like always read and then write pattern we make sure that every cell has been written just once before that was the last time was written to and then we s like read that and then Rew write a new thing right so we always making sure that the read set s like Trails the right set and then we when we are done with the computation then we'll just have a

final read of everything and discard that and the reason we do that is that we can actually now check that the memory consistent it is equivalent to the um constraint that the reset is equal to the right set okay so you'll have some local checks so you will check locally that for instance whenever you load a value then you should be reading that value but you have to write exactly the same value back right cannot change the value whereas if you have a store operation then you would read a value but you can write something different back so there these kind of local constraints okay and then if those local constraints are satisfied and we

also have that the read set is equal to the right set at the end then we know that the memory is consistent throughout the question is now how to check that right because these resets and right sets they also grow really big okay so that's not something we want to store inside the ckvm and for that uh I'm going to talk about using multiset hash functions okay so something that was proposed uh in the CK uh context by setal in 2018 so multi set hash function um takes um a set of uh values from a message

space okay and produces a small digest okay and should have this compression functionality that that digest should be really small regardless of the size of the multiset the other property we want is that if we have a couple of multiset hashes to two sets we should be able to compute the multiset hash of their Union okay and remember these are multisets so all the elements are counted with multiplicities they may be repeating in the set and finally we should have Collision resistance that if we had two different multisets then it should be hard to find them so they're actually mapped to the same

thing so let me give you a standard construction for that so we're using here uh a group G okay and think of this like a standard Prime order um Group which um where the discrete logorithm problem should be hard and then we take a hash function um and you may think of that as a random Oracle for now so and then we just take go through the all the elements in the multic set hash them and we add together these hashes right because hash outputs group elements okay and it has the compression functionality right because now

regardless of the size of multiset the multiset hash is just one group element it's also pretty easy to see that we have the incrementality property right so if you want to you know if you have the multi set hash for one set you have the multi set hash for the second set when you add those two right then you're just taking the sum of all the hashes in both of the sets you get the multi set hash of the Union of those two sets and finally you have the Collision resistance uh property right right if you have two multiset hashes that are equal to each other well the first one is just the sum

of hashes in that set you can subtract then the hashes in the second set and that should be zero and if those two sets well if the two sets are identical yes obviously you get zero right but if they're different then when you count with multiplicities so those are the A's right you would actually get a non-trivial sum to zero and if you model the hash function as a random Oracle that means that now you have some group elements where you don't know the discrete logs and you have made them sum to zero right so now you've broken the discrete log problem so how can we use a multi set

hashing to check memory well the idea is now that instead of directly keeping track of the reset and the right set we will just have the digest of those we will have the multi set hash of the read set and the right set and keep updating that okay so on the right hand side here we have the digest of the reset and digest of theet the digest of the reset well we've not actually had read any value so that's does zero to start with um the bright set starts with the first initialization we do and then we hash that right and then we keep on updating whenever we do one of these operations

we update those two sets accordingly okay and at the very end right if the read set is equal to the right set then those two digests they match and if the read set and right set is not equal to each other then by the Collision resistance property the digest do not match so that gives us a guarantee that resets and right sets match in the end and the cool thing is that this is like you only keep track of the group elements right that these set hashes along the way and update those okay and even if you have different workers that

are doing different slices of computation then that's still fine right it's just a local operation I'm getting some digest and I'm updating that Digest regardless of what has happened elsewhere in the execution so multiset hashing is a way to allow you to check that the memory is consistent just with local operations and then this multi has digest that you're evolving over time okay okay so how does that usually work well you have the group that could be an itic curve let's say it has a prime number of points for Simplicity we

can generalize that we have a cryptographic hash function that Maps into the field fq and then we typically have a map to group function that Maps into the group right and then the hash to group function is the composition of those two so that's the standard construction and it's an expensive construction right because what is the cost here well you have to do this hash function first and then you do sort like a mapping okay and that hashing function is an expensive operation like this is a cryptographic hash function so now you have to compute and verify a hash in every

step and and this is where we sort of like starting to think then okay what are the minimal requirements that we want from this uh hash function hash to group function we want it to have ition resistance right because you if you have two elements that hash to the same value then it's very easy to find Multi sets with just singl ton elements that has to the same but maybe we don't need cryptography for that maybe we can just use an injective map right that's so so that's s like the idea we're exploring here okay so can we just use that that map to group function instead of having

a hash okay and of course this requires that the message spaces of modest size right because if it was arbitrary large uh multi elements then well you do need a CIS resistant cryptographic function for that but if it's a small size set then maybe actually the size of the set is smaller than the group and it's possible to have an injective function and get Collision resistance through injectivity um and interestingly when we do memory checking then we do actually maybe have small sizes right so think of like what would in practice be the size of like you have

an address you have a value you have a time stamp well maybe there 32 bits 32 bits 32 bits or something like that that's 96 bits right that is modest size so we are actually in the situation where we could use just a hash function for mod siiz sets uh for mod size elements right and therefore maybe injectivity is something that we can use when we're doing memory checking in ckvm so there's one other thing that we need to be careful now when we don't have like this hash function inside to make things look random and that is you may also be able to find two elements

where we're mapping to the then inverse of the element right because in an elliptic curve group it's very easy to just in take the inverse of a point by flipping the y-coordinate so we actually need and if you can find that right then you can also find a nonempty set that maps to the same multi set hash as the empty set right because M1 and M2 would the multic set have hash of those would they would just cancel out right and you would get zero okay so we need to be careful about that so we actually need a map to group function which is injected with respect to the X chord inates right so it's s like U resistant to the sign

flip okay and interesting we can show that if we have those two properties then we can actually get um um just use the map to group function and it is secure in the elliptic curve generic group model okay let me see I have two three minutes left yeah okay so I'll just very quickly give you sort like a feel for what could this function look like okay so so it's pretty straightforward um you take the message you add a little tweak to it and you try to use that as the x coordinate right and The Tweak is there because only not

not all the x coordinate only half of the mic good x coordinate so we need the tweak to just make sure that we get something which is a valid x coordinate and then the function also needs to make sure that we cannot flip the sign um we suggest if Q is equal to 3 mod 4 that would just make sure that Y is the quadratic residue right because only one of Y or minus y is going to be a quadratic residue and you return that point okay and let me okay and okay so what are the constraints we need for to ensure

this well we need to make sure that X is actually a something that matches a point on the in the group right we need to make sure that X is a valid jump with this tweak we need to make sure that it Y coordin is unique so we cannot flip the sign okay and all of those are pretty straight simple constraints to verify okay so using this kind of um multiset uh hashr map to group function then we have a um deterministic map that can be used to sample such

points okay there's a one more thing to be little careful um about which is that um you could imagine that the pro instead of using the smallest tweak used a different tweak um and this is why I'm I'm switching from map to group functions to map to group languages because actually turns out that it doesn't help the provs if they're cheating that way and that means that don't have to go through the trouble of proving that The Tweak is the smallest possible one right it just has be one of the valid tweaks okay so the construction if we

instead use the map to group function looks like this just as before um and as you seen we only need a very small number constraints to check that a map to group function is evaluated correctly okay and with that I'll stop my talk thank you [Applause]