Quantstamp: Linting Halo2 Circuits

more to come from this work but we'll get into that so first what are we talking about well we're going to be talking about bugs on Halo 2. you may have seen Halo 2 a bunch of places I think Scrolls using it for a roll up probably a bunch of people are using it for a bunch of different libraries uh and it's essentially a zero knowledge proof system that is written in Rust it uses uh plunkish arithmetic so it's based somehow on the plank crypto system that's been around and essentially what happens is you take some code you do some magic and you get a table and some constraints and that is somehow equivalent to your piece of code I could go probably for 20 minutes about what that actually is and what that works like but I only have 20 minutes so I can't do that so I'm going to assume you kind of have a rough idea of how this works and if not please come ask me or someone else is working on this project but essentially you get some table and some constraints out of some code and you do this in rest and so essentially you get a table and some columns are known only to the prover in your zero knowledge system some are known to both the proofer and the verifier select the fixed ones or the instance ones um and then uh some things are also set up at different times so it's not always clear that you have all the information at once ultimately it doesn't matter too too much about what those columns are or where they are for the purposes of this talk just note that we're going to be talking about tables and constraints over those tables so that we can see if we can find bugs in how these tables are developed uh inside the rust Halo 2 library system so I said at the table we've got some columns we also put some values in the table no surprise these are the things that actually get executed on and evaluated during your process so you know the specific numbers don't matter what for this slide for what really matters is the fact that we have polynomial constraints over these table entries now I'm not going to give you a very precise definition of what these constraints can look like but you know they can be combinations of various things inside the table so you could you know talk about a constraint on a singular row typically you'll always assume it equals the zero or the proof system will let you do this sort of by default um but you can also do things like talk about entries in the previous row or the next row or different columns or however it works but essentially you get this this great table and this great system of of constraints that are polynomials and ideally this capture is exactly what you want to do correctly and everything works out right that's the ideal situation in every piece of code that you do something and it works in this case we know that bugs are everywhere and what a surprise bugs happen in the zero knowledge world just as often right so here Xerox park has a nice GitHub uh list of known bugs that people have seen so far in zero knowledge settings so these are probably you know more subtle in some cases so the frozen heart bug that's somewhere down there uh really subtle not exactly you know something most developers would probably catch I don't know exactly the details but it feels like you had to have read the paper to really figure that one out other ones a little bit you know more obvious to the end user and something you can catch automatically not everything here is going to be automatically checkable and we started to look around and we saw that there were various tools that were trying to catch some of the stuff automatically or prove that these bugs weren't in these systems we're like that's really cool like we love that Tech I got some background informal methods a bunch of us do we wanted to see what was out there and we started looking at this in the context of Halo 2 and we didn't find anything now it could be wrong they could be out there but we didn't find anything and it's been going on for about a month now and we still haven't found anything so I think this Talk's actually still on point and what we're going to try to do is see which one of these common bugs mostly on the right but not necessarily so in fact on the left the bottom we can find in Halo 2. and the caveat is um this work is very much a work in progress slash proof of concept it's almost certainly not going to work on a production level system tomorrow next week or even next month right so this was just can we do it and should we see if we should invest more time to do it or can I get up here and talk and then someone else can do it better for me because that's also useful to me as someone who likes to use these tools but essentially what we're going to be doing is sharing or describing at a really high level this piece of code that's going to look for just a small subset of these bugs there's obviously a lot of bugs there on that last slide but the ones we really were concerned about are things like under constrained circuits how can we detect those because if that's the case you might be able to get approver to submit some vacuous proofs into your zero knowledge proof system or things that are are more akin to linting so something like unused Gates or unused constraints or um sorry unused columns or assigned but unconstrained cells so things that you know if you were doing everything right and sort of efficiency efficiently as a developer you wouldn't necessarily want to write Gates take time to write you know they could affect how your proof system is run um and if they're unused either you meant to reference them and you didn't and that's a bug or maybe you just wasted some time and so what we're going to find is some analysis that doesn't necessarily point out that you've made an error in some cases it might uh but it's sort of like something you can run at the end of the day and say okay maybe I gotta look at this or maybe everything looks fine and I don't need to worry about this just yet it's also the case that the tool will probably come up with some false negatives so we're not proving it's going to catch everything we're not claiming that but it might catch some obvious cases it might save you a headache down the road and we kind of envisioned that anyone who would have run this tool runs it you know if they did their job well they gain almost no information from this so it's almost like a useless step but we think it's a very important thing to start thinking about now before these Halo 2 systems really become live and big and people have lots of money in it because preventing issues is better than reacting to issues especially in the blockchain world so if all I you know tell you on this work is we have something that kind of works and you want to do better by all means do it but otherwise we at least have a starting point and we can launch off of it so as I've said we looked around for tools we didn't find anything for Halo 2. doesn't mean we didn't find anything um there's a bunch of projects out there that claim to do something similar acne and pikis are two that I present on this uh page they've been sort of competing against each other in some sense as far as I know uh and they do sort of the same thing they have different tactics spicus uses symbolic execution acne is a little bit more fixed Point algorithm based but they don't importantly Target Halo 2 circuits now that's not to say the ideas in those systems cannot Target Halo 2 systems but they currently don't right they just work on r1cs files and they do similar things probably even more than what we're claiming to do and probably better on those things and so we just thought well can we do something that's like this or start doing something like this for Halo 2 and see what comes so I'll take you through an example of how the system works at the very low level on on one class of problems which is under constrained circuits and then we'll talk about some of the other analysis it can do namely assign but unconstrained cells and unused columns and then I you know we'll probably be out of time and so you're going to have questions if you're interested in this field come ask me and I'm happy to talk to you all about it but let's go through the simple example to start so the first one we care about is an under constrained table so I've removed look at the values from the column but you still get a table in Halo 2 at some point and we're going to say that a Halo 2 circuit is under constrained if there's two valid assignments to uh the advice column that hidden column for the prover that you know when paired with the same input instance public variables whatever you call them also satisfy the system right so in this case what could go wrong is uh you know approve or prove something but then there's another proof that proves something that's possibly vacuous and you know it could be with low over low probability also something that's not vacuous and problematic that's probably not going to happen but it still probably means you wanted your system to be constrained more than it was and so you know there are real examples of this happening at least toy real examples I don't know if this happens actually you know in the real world to scroll or anyone using Halo 2 but we can come up with 20 examples to drive home this methodology and the first one I'm going to say is well let's give me a program that I want to write in Halo 2. which it just checks if a number is in zero or three namely can you decompose it into precisely two bits that are binary that um you know when combined in the appropriate way add up to a number and that number is less than four and so we can encode this very simply we can say well we need two bits B1 and b0 they've got to be binary so we have two constraints that we're going to need to put I've omitted the table because it's a little bit sort of small in this case there's not too many rows in fact you can do it with one row I think and then you need the other constraint that just says how to compose uh this bit information into the number you care about and check if it's between zero and four or zero and three sorry inclusively and so we'll have two advice and uh variables b0 and B1 those will be secret and if we can find two two inputs to those that differ for the same input whichever input that is X um we're going to have an under constrained circuit and if you do this correctly it's um it's not going to be an issue right this this won't be an issue someone will have so let's let's try to code this well this is actual Halo 2 code um so what we're going to do is we're going to create a custom gate that checks if a number is binary in this case B1 because we have two bits we need to do this so I'll take the B1 column from the advice you know I'll do some stuff with selectors that I've already omitted anyways if you're here and you're an expert on Halo 2 you know I've skipped a lot of stuff um which is fine I only have 20 minutes and then we're going to make this compress this expression which is that that Vector thing that sort of says a times one minus a and and it the proof system will assume it's equal to zero and essentially this means uh this is a binary variable so we do that all is good then we need to do this for b0 and really quick so we copy and paste it it all works out and then we add a final constraint here uh that says okay actually I need to be able to say uh you know B 0 plus 2b1 minus the input variable C or X um is actually the number we care about right that is it's not just some input and we're emitting a little bit here uh because we're using the advice column to copy stuff in from the public inputs which is maybe not how you would do it but um from what we've seen is how some people do it so it's not a totally contrived example aside from the fact that it's small and probably too small and then what we're going to do is we're going to do the most naive thing a computer scientists can do in this approach we're going to plug this into a SAT model and hope it doesn't time out and for this example there won't time out because it's really really small but um maybe in the future someone can do it better or maybe we can optimize what the model looks like or maybe we can uh you know break symmetry in some way that makes sense and so what we'll do inside the Halo library is every time you give me one of these Gates that you just built there's that constraint that is there convert that into some equivalent phrase in a valid sat model or smt model in this case we're going to use the Z3 solver because in our personal experience it works fairly well but you know it doesn't have to be the case that you use that one and then we'll just say is it set and the answer probably should be yes otherwise your system's overconstrained and that's a whole nother class of bugs which we're not going to talk about and if it's yes we'll just say can we find another satisfying model and we're going to do this as the most naive way possible we're just going to add another constraint to the set model that says you know change one of the variables either the B1 was Zero at this time or B zero was different this time and you just see if you can find another model and if you can do that the system is definitely under constrained because you've changed the assignments and you know you found two different variables or two different models that satisfy the set and so you know you definitely have an under constraint itself system of equations now if it returns no uh you're probably in good shape but I would guess at scale most of the time it's just going to time out you're going to learn nothing but you know it's the most naive thing you can do and like I said we did it over a week to see if it was possible and in this case it does work right so the novelty here isn't necessarily the quality of the work but the fact that we're trying to look at this in the rust in this case we did find two things and why did we find two things actually I thought I presented a good model well I'll tell you why in the next one but essentially there was a copy and paste error if you were paying attention you saw it if you weren't congratulations you know it's why you need Auditors um and so we do find one in this case essentially we thought we forgot to constrain b0 as binary and so you can just say b0 is three if your input is three and it's all good just set the rest of zero in this case naturally it takes almost no time to run right it's it's a tiny model it should not take hours you got a problem if it does in this case it's also push button we've hard-coded what it means to be um under constrained in a rust system but the advantage is you could write additional properties in z3's language to try to see if they hold uh given that we don't really expect Z3 to scale I don't know if there's a lot of value in that but it is something you could do uh and the key point is it's sort of automatic if you implement this trait in your rest two circuits you get this for free and so maybe at times out maybe it's not particularly you know valuable but at least it didn't cost you a whole lot of development time either so uh let's find out why it actually went wrong well when I copied gate B1 over to gate B zero I changed the name of the gate but not actually which variable it's referring to so I actually only constrained B1 and I just happened to constrain it twice with the same constraint which means you know it doesn't really matter what b0 is and uh the smt solver was you know was happy to find this issue for me and now I can go back and fix this and it would totally work so only got four minutes left I'll talk very quickly about how the other checks work which are probably more sophisticated um essentially we're going to go away from uh smt solving and sound solving and use sort of the next most naive thing in computer science which is abstract interpretation and we'll just start replacing variables in these constraints with abstract variables which are either zero something or definitely not zero right uh sorry definitely not zero definitely zero or just something and you can use that to then evaluate all of these constraints in the sense that you know if you're adding two things that are definitely zero well the result is definitely zero right zero plus zero zero uh if you're adding something that is zero with something that is not zero you're getting something that's not zero and so you can evaluate these uh polynomial constraints that you get from this library for free anyways and in some cases you know that they're always zero probably not many cases we haven't done a real world study to confirm it but in the case that you do have something that is always zero you can probably claim something about it and it's not perfect you have to do a little bit of work um some things you don't know which gates are being used or which constraints are totally applicable but uh in some cases you get some things I've omitted discussions about things like selector variables which would turn on Gates and turn off Gates but you know if you give me a concrete assignment of what that selector variable set should be I can start to do this and when you do this in a careful way and you think about it which I don't have time to explain we can get checks for unused Gates under constrained cells and assign button unused cells right so we get a little bit more and this has the advantage of actually being a lot faster than an smt solver because you don't have to any of the stat solving the downside is you might get some false negatives you know some polynomials might always go to zero and you just can't show that and that may not be you know ideal but it is a good start for this type of work in my opinion and you know maybe the real answer is just take the ideas from acne and practice and put into rest but I suspect other people are doing that anyways so what I'll just end with is a couple things there's a lot of challenges here I've tried to be open with you and say this is not a final product this is not something that's complete we don't know how it'll scale that question is a gonna really slow the system down in almost every way right can we do better um so specific implementation stuff like how do we actually do this in the rust libraries there a nice way to do it we sort of have to Fork our own and make a trait is that the right way to do it uh it seems decent enough but maybe we can do better we haven't tested it you know we haven't evaluated it uh when it will crap out if it craps out which we sort of expect it would and maybe we just have to review the code again as well so for those reasons in part um we haven't published this code open it I'm not sure what we're when we're going to do that um but we also want to write a paper on the idea of very you know it I don't think it's like massively novel but I think there is still a write-up that's worth doing there and see if there's any intricacies for um for this type of uh zero knowledge proof system in this library with these tools and maybe that will be where we evaluate exactly when this fails and that alone is something right um in which case then we can probably also you know publish a very decent version of the code and um and because it's very much a work in progress and we've only been working on it for a little bit um there's going to be future updates and one of those future updates will definitely be at ZK Summit nine so we're gonna give a talk there it's probably going to be starting to look a lot like this but hopefully we'll have a lot more work done and we'll have fewer open questions or you know more explicit responses to things like will it scale um but stay tuned and you know find us at in Lisbon uh in April uh to learn more or just shoot me a question so thank you if you have questions feel free to find me on Twitter I don't tweet but I do respond it's also my telegram handle and um ask me about this anything in Halo 2 anything about auditing we also got three EF granted Quantum so we're very grateful if you're on the roll up we definitely want to talk to you about that and um yeah thank you [Music]