ZK9: Linting Halo2 Circuits - Jan Gorzny (Quantstamp)

Transcript

foreign [Music] thank you uh so hi my name is John on the slide you might or on the little cards here you might see that this was supposed to be presented by uh Fatima unfortunately she couldn't make it today but I'm here to fill out a pillow take your spot um I'm a blockchain researcher at quantstamp we're a web 2 security company and we're going to talk to you about how to check for some errors in Halo 2 here today also if you have questions feel free to ask me at the end or find me but my colleague motion is also here he's sitting somewhere over there and if you find him you can also answer some questions about this so uh let's get started

this works okay too far uh okay so I won't introduce entirely what Halo 2 is uh because I think a lot of people here are familiar but I will give a very high level overview in case you aren't familiar with this proofing system so Halo 2 is essentially a zero knowledge proof uh Library that's written in Rust it uses planckish arithmetization so it's based on the plot proof system and some modifications to it and essentially circuits are tables and then we add some polynomial constraints over those tables so here we can see an example of a table that would represent some sort of a circuit you know it's got some values in it I don't know if this is a real circuit it almost certainly is not but essentially you have some columns that are available only to the prover in your system some columns that are available

to both the prover and the verifier like the fixed column and some input some instance which is available to both the verifier and the prover and these things are known at various times but essentially you build um in Rust these Gates and these Gates eventually get translated into these tables and into these constraints so um this is what a table looks like obviously with some dummy values what happens if we look at cons constraints well um abstracting they can be kind of arbitrary there's some limitation on how far you can sort of reference things within this table but essentially their polynomials over cells within this table so you might have something like some eight some ith column in or some I throw of column A plus you know the same Row in column B minus that same

row and C should be zero so that you know basically we have an addition gate or something like this or you can do multiplication you can do other things they can be sort of generic polynomials to some extent um maybe not fully generic but essentially you have these polynomial bugs uh sorry polynomials over tables and then what happens is of course this is a proof system that's written in Rust and therefore people have to somehow build this proof system and use it to build applications and do interesting things and because this is done mostly by humans and humans are error prone we have lots of bugs that come up into the real world naturally we've seen this a lot in the smart contract security throughout you know all of web 3's existence but also bugs are just not new and it should be no surprise that zero

knowledge proof systems also have um you know significant classes of bugs some of which are are very difficult and sort of in depth some need a really good understanding of the system to catch and are probably not something that the average developer will introduce into their code rather it'll be something that's introduced by the people developing that Library if it becomes a concern but others are possibly ones that the end user application can actually introduce into their Gates and systems so in particular um you know some things here like uh I think the frozen heart bug is listed here I think that's more of an issue with sort of how the proof system was created on the back end but things like if you don't constrain your your cells

on that table that we just showed you that's more the application side and so you know we can't aim to necessarily catch or look for all of them all the time and it doesn't make sense to do it but for those application layer ones certainly we want to see if we can reduce the likelihood of these errors coming into into you know the real world uh because obviously people are going to make mistakes so this this uh collection of bugs is by Xerox park I think it's a great selection we're not going to focus on trying to catch all these bugs a lot of them are hard like I said some of them don't apply to the application Level but some like un uh unconstrained cells or some of the ones they're the bottom of that left-hand column um are something that maybe we can look

at and we've been obviously we're a security company at constant so you know we've been looking at how bugs manifest in the real world and how do we catch them and how do we detect them and how do we prevent them from happening and we were looking around at a bunch of zero knowledge um systems and we found okay there's some unique bugs obviously here's a list uh you know what about for Halo 2 and while these bugs certainly might apply we didn't find any tooling to to find those and and tooling is very important in any audit that you should get um you should expect some level of tooling to be run because uh some things are easier by tooling and some things uh you know probably necessitate some tooling if things get really complicated

uh some manual inference is probably also going to be necessary because you can't catch everything automatically but you know we want to see what could we catch automatically is there something we can do Beyond just testing um and we we started to look and we didn't see anything for Halo 2 we we did decide that maybe we can try to do something for Halo 2 because the next slide we'll show you um there is some ideas for how to catch some classes of bugs on other proof systems in particular ones that compile to rank one constraint systems so in this talk I'll give a very high level overview of what we're sort of aiming to build and just sort of what we can try to catch automatically so in particular we're going to try to focus on sort of four classes of bugs one is under

constrained circuits this is probably the most sort of big problem that we're going to try to capture it's also the hardest one to try to catch in the code but we'll also try to see if we can find unused columns or Gates that might be a bug it might enable an optimization and assigned but under con but unconstrained cells because that's also an under constrained circuit and we're going to describe this tool sort of as a linter it's not going to spit out a proof saying you definitely have secure Halo 2 circuits at the end of the day uh we're not doing that there's no specification you're going to add to it uh there's there's no sort of heavy formal verification going under the hood there's just a bit of a SAT solver or SMP solver and so we envisioned that this is something that

if you know makes it to production and in the real world um is something that developers can can run and they sort of use it like Slither and they run it and they say Okay most of this probably is is not going to be something to cause me major concern but let me just double check the entries to make sure that they're just false positives at worst and so as I said there were some some work on automated detection of zero knowledge bugs in the wild already but not for for Halo 2 and not for rest um so varadise um and others have been working on things like this I don't remember I think one of these is very nice I think pikas uh but also acne exists and both of these aim to do sort of the same thing they CLA they catch some class of

bugs on rank one constraint system uh proof systems so that if an app developer goes and writes a circuit in that language they can check to see that maybe what they intended is actually there in the code right that's that's sort of the end game and if not they'll tell you how maybe there's some errors and so most of them are based on symbolic execution um often they support custom query so we'd like to do the same if we could and it's automatic in the sense that you sort of just push the button and it spits us some results and you don't need to worry too much about um writing additional stuff if you don't want to if you do want to you can um the alternative acne uses a fixed Point algorithm and you need to specify a little bit but again the important

part here is that both of these only target rank one constraint system inputs so they don't work out of the box for Halo 2. it's conceivable that you could probably massage one format into another but it seems like a lot of work so we decided to Target the the Halo uh directly and see what we can find and basically we're going to try to use some combination of both these approaches we're going to use some symbolic execution slash sat solver and some fixed Point algorithms which we'll call abstract interpretation okay so let's use a motivating example to figure out exactly why we're doing this and why this might actually be relevant to to you as a developer of these apps or um someone who wants to build a better tool than this one because as I said this only proof of concept you can probably do better

okay so we'll have a motivating example and for that we'll Target the first class of bugs we're trying to catch which is an under constrained circuit so we'll say that a Plancha circus C is under constrained is if um for a particular uh assignment of the instance column on the right which is the input to the Circuit there's two satisfying assignments in the advice column that would allow the prover to prove something about this so this might mean in the real world that you're proving something that you didn't mean to prove or someone else could prove this uh possibly and that would generally be be bad especially if that thing extra thing you could prove is an additional transfer of funds and a roll-up or something like this right so this is one definition there are other definitions that people use for under constrained circuits out there we'll use

this one so let's build one of these circuits inhaler two okay uh if we want to do that let's uh take the example and make it very explicit so here we'll just do the most stupid uh sort of example we can come up with this is just a range Tech to say hey is a number in zero or three right in our circuit and we can encode this um you know with a suitable table which is so small that I'm not going to show on the screen with the following constraints and essentially we'll have three constraints the first two just enforce that the variables representing the bit decomposition of our number are binary so if it's a number between zero and three you should be able to use two bits to to represent this number uh and both should be binary and those that's what it is what it is here so for

example B zero times you know v0 minus one V Zero's got to be zero one just to satisfy this and then the last constraint We'll add is um can you actually decompose your input X two bits where you know one of them is just zero one and and the other is going to have two or zero right and so that's that's all this example is going to be and if we want to write this in Halo 2 we're going to write something like this so this is sort of real Halo 2 code that is uh sort of legitimate in the sense you know this would be in some app potentially uh so we'll provide a gate here we'll say make sure that B1 is binary right and there's a bunch of sort of linguistical stuff there that I don't

think I need to uh to dig into but essentially we encode that polynomial that says you know a times a minus one uh or sorry a times 1 minus a uh and then the system just assumes it's equal to zero so we don't need to add that explicitly but it's there then I'm a lazy developer so I'm just going to copy and paste this make the modifications and then go to the last gate that matters and say something like um you know make sure I can decompose my input instance into these types of bits right and and it's very important to note here I was very lazy very fast developer when I wrote this right this might be a problematic circuit and if we want to try to run that through our system what we'll do is we'll convert all of that stuff into um an instance of a satchel and we'll

just say hey can you find two satisfying solutions to this because if you can do that we have exactly satisfied the definition of our under constrained circuit so what we what we'll do is we'll hook up a SAT solver into the rust code directly and you can do this through various libraries like smplib or Z3 natively and essentially you implement some some trait or some other relevant component in Rust and as you build your circuit you can just sort of query that circuit afterwards and say give me all the polynomials you got and then we'll convert them and we'll translate them automatically into something that is acceptable into the smt library or the solver itself directly and we'll just hey is it is it sat the answer should be yes if you have a circuit that's right you probably have at least one satisfying solution and then we'll just

check to say can you find me another sat solution if I tell you at least one variable has to be different in its value in the next model and if you can do that then actually we're going to have two models for the same problem and so we're under constrained I'm gonna take a breather here talking quite fast um and essentially uh the the tricky part here is this conversion from uh Halo 2 code to the s p library but it's sort of not incredibly challenging I think anyone in in this room who's a competent developer could eventually solve that problem and then we'll see what happens if we actually run it

and very quickly uh the code will actually say yep we have two sets instances and I'll show you why on the next case if you were paying attention on the last slide you probably already know why but essentially the tool within seconds can find that actually you know we have two Sat models that's not surprising this is an incredibly trivial example we don't want this to take hours right if we if it was taking hours or probably doing something wrong um but you know thankfully it passes the sanity check of being fairly quick and it's very push buttony right so the developer can actually take this put it through their system and run it and ideally they get two outputs or it says Nah you're good um it might also time up in fact we expected to time out on most systems uh that are sort of

real world because they're going to be a lot bigger than this uh but it's also nice because if the developer is really interested in improving other properties in principle two they can go into the rust code where you call a solver and add your own constraints and then you can do things like prop bounded model bounded model tracking by adding your own property if you want to see if it holds for a particular sat uh instance um kind of hoping to present that today but we didn't get a chance to sort of round that out since the last time the stock was given so uh push button but with the optionality of changing things later if you want and um the key part is yeah it's all automatic and so we did find this was under constrained why was the center constrained well when I was a lazy very quick editor

uh or developer I copied and pasted my my gate from the first case into the second one I've only changed the name of the gate not actually the variable it's being constrained by that gate and so what you have is actually there's no constraint on b0 being a binary variable which is exactly why in the previous slide in one instance both of them are binary in the next instance uh b0 is clearly three which is not zero one so um you know this is this is a contrived example but it's also possible in the sense that people are lazy developers are lazy we do see this all the time people make copy and paste errors uh everyone in this firm is probably made at least one of these errors in their life so um you know it does catch something but as I said we did also try to find

other things we could do because we anticipate that the SAT solving approach won't scale uh I can't imagine having the system sort of run on a roll-up and saying oh you found all of your satisfying assignments to uh um to your instance I mean if your polynomials look anything like what the one for the flock paper looked like that's way too many for the SATs offer to hold we anticipate one of the major outstanding pieces of work for this project is actually figuring out where that limit is but uh we do plan to do that and we're targeting a paper submission by the end of the month so hopefully we'll have answers for you for now let me talk about the other checks we wanted to do I told you we were talking about four different types of checks and we just went over the example

for under constrained circuits and um as you saw it it did work to some extent we don't know if it'll scale but another approach that might be sort of obvious and possibly better at scaling is something called abstract interpretation this is also another classic Concept in computer science it's been around for 40 50 years and we started to see if we could figure out uh ways to get some checks for this uh through this method sorry and essentially what we can do is we can evaluate the polynomials that we get from our rust library abstractly and just sort of say does it always evaluate to zero does it evaluate to something or is it definitely not zero like it always comes out with some non-zero value and

then when you do that you can compose these polynomials and these variables that are abstract and you can um see if you can figure out if anything is always zero all the time for example right and if that's the case then you get one of these checks right you can check that um you know various regions are are not constrained or that um some columns are not being used because they're only used in things that always evaluate to zero and so are never really important um so they're on the bottom there you can see an example of how you know evaluating a sum abstractly would work for a polynomial so basically you know so sum and multiplication you get it all multiplication is an analogous and so um

you know we don't evaluate the polynomials explicitly we don't have that information we do it um attractively over some regions and we can do this because within the Halo 2 system we know which gates are on and off we can sort of guess or we can get that information uh beforehand by sort of setting up the system but not running the system so we know which gates are on and we know which polynomials we need to abstract develop abstractly a value uh this comes for free from the rust library to The Layover and then as a result as I've already mentioned now we do get things that check for unused Gates so you know is there a gate that you wrote down in your file that you never actually referenced that's probably a bug people don't write things for nothing now could just be the selectors off so maybe you

know you're going to use it another time but uh go check it right this is why it's a linter not sort of a approver that you definitely have in here uh do you have unconstrained cells so is it possible that you know the values are not what you want them to be and unused columns this might be a bug or it might allow you to optimize your your proof system because the number of columns you have affects the runtime of your approver or your verifier or both and I can't remember which one it is but it may also be the case that you know we don't report anything particularly useful because uh it will return false negatives at times and say yeah I don't know and in which case um you know you might have some of these issues present but the technique just couldn't catch it but we think it's

still valuable to have this because you know there's probably going to be a couple of cases where where this does actually happen so um I think I might actually be almost done talking fairly fast my apologies um so um to conclude here quickly we've got lots of time I'll give you time for lunch um we we're still working on this uh if you saw this talk before Denver I apologize it's mostly the same there was a couple small changes uh but essentially we're trying to build up the proof of concept to see what we can catch for Halo 2 because we don't think that Halo 2 should be omitted from the class of proof systems that can have some level of automated detection and we're very interested to figure out how that is admittedly we're also spending a

lot of time on audits we're very busy so we're not prioritizing this project super high but if uh if you have ideas or suggestions or if you want to work on this please let me know or Motion in particular we also want to wrap it up and sort of Open Source it and submit it to a you know a nice Academic Place to validate the ideas that we're not crazy and missing things that are obvious uh that's coming soon as I've mentioned we're going to try to do that by the end of the month um and through that process we'll hopefully solve the rest of the big open questions for this approach which is you know when does it actually she stopped scaling because I sort of expect it won't work for a roll-up and it obviously works with a very contrived example but there's somewhere in between

where maybe this is very useful and maybe this is not so useful um we also just need to clean up the code base we don't have things like unit tests or whatever testing would you know be totally acceptable within the rest Community uh and we just want to see if we can catch anything else in this acne and practice actually class some catch a much larger class of bugs than we do so maybe we can take some of those techniques and apply them to our Halo 2 Checker I'm not sure how much of that is is sort of in the road map but it's definitely something we can consider so I think that's everything so if you have questions feel free to reach out to myself as I said my colleague motion is also here on Twitter or telegram same handle or just find me so thank you

[Applause] thank you very much I think there's a okay [Music] [Music] I'm sorry I'm I'm not having a great time hearing you can you can you say the first question I think you got two [Music] Ah that's a good question I don't know

um the engineer who would better answer that is unfortunately not here so uh I can follow up with you and let you know [Music] [Music] yeah so uh I believe that's also one of the parts that's sort of being fixed under the hood uh to really figure out how that system is being implemented the idea is to have a finite field solver and there are works in the literature that do this I think that's one where we're testing to make sure that we've done that correctly but it should be

something that's kind of custom [Music] um actually [Music] um okay so I think the question is how do I how do we look at rotations for like the next row and things like this also unfortunately a question that I can answer right now but I can find the answer from Fatima and we can get back to you on that

and effectively okay so maybe we can compare notes and then just see what works too right it's also possible we're just not doing it yet or can't do it so like that might be a limit we'll try he went to someone else I believe the current uh back end is Z3 and we had a suggestion in Denver to switch to cbc5 to see if it performs better I don't know if that work's been completed I believe it was being tried last night literally so

okay so yeah I mean I think we want to evaluate both of them before we submit or open source it to see what works but there also might be issues like the other question asked that are more pressing in the sense of like are we complete so much five consultant and sometimes yeah this was exactly the suggestion we had sorry the question was first what software reason and uh this next one was uh cbc5 might do a lot of the stuff we want to do for free and and that's that's sort of why we haven't made substantial feature upgrades in the past

couple of weeks is because we've been trying to swap out the Z3 for the cbc5 to see if we can do something not just for the sake of evaluating um like run times but to see if it's you know simpler and more elegant and uh I don't think that work has been completed just yet thank you um I'm sorry I didn't catch the question

how do I deal with forced I I don't I'm not sure I understand call something you have done it with friends and stuff but that's just a normal energy I'm still not catching it I'm sorry maybe we can ask this after I or can you speak a little louder I'm sorry I just I'm not yeah okay okay so uh I think I was hearing some of it how do we deal with false positives

or and or how do we deal with annotations to the Halo 2 code base is that yeah okay so the answer is we almost certainly haven't tested the annotations part and for dealing with false positives you could presumably just check to see if it's uh for the for the underconstrained case you'd be able to check by putting those values into it and seeing if it actually passes it would be nice to have that round trip done automatically right now you'd have to do that manually if that's you know entirely feasible which I don't think we've sort of tested explicitly so yeah you'd have to still inspect it right

so it really depends on how much resources we allocate to the project in the sense that you know it started off as sort of not quite a hackathon somewhere between a hackathon and a real product uh so I don't know the you know if there's demand and we fix all the other issues that may or may not be existing um and you know it's well received then then sure and if we open source that other people can certainly help with that right now um I don't know that we're going to spend a bunch of resources on supporting other planckish systems now if it's very trivial to do that if they have sort of the same implementation structure and rest where it doesn't take a lot of effort sure will we spend another two

years on it not that we spent two years on it now but like will we do that probably not so I don't know but probably no any other questions [Applause]