Unconstrained Machines

Transcript

Um I'm going to talk about uh security review of ZISK. So the agenda is what is ZISK? Some security properties, some vulnerabilities we found, some thoughts on tooling. This is going to be very very quick. So if you see something on the slides that I don't cover or you just want to talk to me about something uh about it afterwards, I'll leave my details on the screen. Okay. So what's this? CISK is a ZKVM. It's compatible with 64-bit risk. Importantly for our point of view, it's optimized for low latency proofs, which is really good if you want real-time proofing. Um, first big win, it's open source. That means it's transparent. No lockins for users.

Lots of love from Open Zeppelin because of that. But the one I'm going to highlight at the moment is it's lots of well- encapsulated components, which is really useful. So that makes it good for security reviews. Uh, quick anatomy of aisk program. So if you start with some program counter at the start and then you execute a bunch of instructions and you get to the end then you have a valid CIS program. So to make sure we're executing the correct instructions, there's a ROM component that's a whole separate circuit and that's its job is to make sure that every instruction we execute was preloaded as part of the valid instruction. Uh one of those instructions might access memory.

There's a separate component to make sure that you're doing that consistently and making sure you're aligning all the addresses correctly. One of those instructions might use a register. We want to have a separate component to make sure that we're uh uh that we're reading and writing the latest state. The time stamps have to have a range check, a separate component for that. Once we're sure we're executing the right instruction, we have a separate component to make sure that the execution was done correctly. And as you can see, the pattern here is what we're doing is just breaking it up into all sorts of little components uh to try and handle each part individually. Uh if it turns out the program itself is just too long, then we just break that into a separate component and then just have a sub separate point there. So the

intuition here about what ZISK is trying to do is that they've broken this into a bunch of different components. Each of these can be proven independently and therefore the latency goes down because you can do them all in parallel. Uh and then you can get like real-time proving and that they're really trying to optimize for that. From my point of view, the other thing I'm going to say is this also just happens to be really good for security because whenever we're reviewing the system, it has very very clean interfaces and you can like sub them in and out. So it's really easy that way. Uh so I just think it happens to be a good little um it's a very complicated system that is broken into very simple components. So I think that just makes it uh makes it really useful.

Cool. Let me just go through some of the bugs that we found just for the sake of it. Uh some background. If you try to do a lookup like an exor, you want to validate that a x or b equals c. Keep in mind the prover gets to pick all of these. So it's our job to make sure it's consistent. What we do is we construct one of these binary tables where we have all of the possible one byte values of A, all of the possible one byte values of C and sorry B and then the corresponding value of C. And then we just go from least significant bytes to most significant bite one at a time just making sure it's all consistent. We have a separate one of those for every single uh up code, every binary up code at least. So the problem here, if

we're looking at the less than or equal to up code, uh what they were doing was just checking the high bite, which works in most cases, but if they happen to be equal, the actual answer depends on checking the next most significant bite. Uh they were missing that particular check. So we just had to recommend doing a uh a carryover for that. This one's a little complicated complicated to explain. I won't go through it in detail just because uh we won't have time. But I might just mention that if you're looking at a 32-bit op code in a 64-bit machine, uh, one question that comes up is what do you actually count as the high bite? Should I consider bite number three or bite number seven to be the high bite? It doesn't actually matter as long as you do it consistently, but there was like an inconsistency in two

parts of the system and that caused a couple of bugs in this case when you're trying to do that correction. And the last one I'm going to talk about is the carry. If you trying to add let's say a plus b equals c, if you have an overflow in one of the bytes, you need to carry the one obviously. Um sometime some of the oper operations have a carry, some of them don't. Some of sometimes a carry should start at one, sometimes it should start at zero. The way this is all handled is with this has initial carry uh flag uh that wasn't constrained. So that means that it was always possible to turn the ones into zeros and zeros into ones when you're just doing the initial carry. So you get an off by one error. There is a slight subtlety with this factor of two which I

won't bother explaining other than just noting that it is still possible. Even though there's a slight complication there, it's still possible to turn the zeros into ones and the ones into zeros. Okay, so a couple of observations. Those first two bugs were like logic bugs. And as it turns out, they were um they have a transpiler where they start with uh with a risk program, turn it into a ZISK program, and then they just transpile those operations and they weren't using any of the buggy op codes. So that was like a part of the reason why they didn't detect those. Those are the kinds of things you detect with a the test suite. But uh the under constrained bugs actually hard to detect. They're a bit more subtle. You kind of have to figure them out from either direct reasoning, sat solving or some sort of tooling

mechanism. Okay, so this is my last slide. I'll just mention that we did experiments some tooling. Uh we used the Z3 SAT solver. It managed to reproduce some of the findings and also found a regression bug was kind of interesting. I would love to be able to do that interactively. Maybe it's already possible. Some people have mentioned a couple of these tools. I personally haven't used them. If you have any uh insight into that, please let me know. I'd love to talk about it. The last thing I'm going to say is I was on a panel about four years ago being skeptical of formal verification. Uh mainly because people were talking about it for DeFi and I was claiming it has a bunch of requirements that I don't think DeFi was meeting. But as it turns out, I think it actually does make sense for

something like a ZKVM. So I'm actually excited to see that happen. I hope they they will do that soon. Cool. Any questions, please hit me up in Twitter or email. Thank you.