Formal methods for zero knowledge circuits with Isil Dillig | a16z crypto research talks

Transcript

very exciting to have Iselle today um so Iselle is a professor computer science UT atin and also co-founder of verise it's a blockchain security company and she's been a tremendous great work in the formal method and PR language and today she is going to talk about foral method of De knowledge circuit program thank you so much D for the kind introduction so uh as D mentioned I'm Isel dilig I'm a professor at UT Austin and also a co-founder of verise which is a uh blockchain security company and today it's my pleasure to tell you a little bit about our work on formal methods for zero knowledge circuits so first of all I think everyone in this

room probably I'm sure everyone uh knows about zero knowledge proofs but in a nutshell a zero knowledge proof basically all uh proving that some statement is true without revealing anything beyond the mere truth of that statement and you know because of this nice property of zero knowledge proofs they found many applications as you all know in the blockchain space for example in privacy preserving Financial transactions ZK rollups which are scalable layer to blockchain Solutions secure online voting as well as uh many other application domains but let's say you are a developer and you would like to incorporate a zero knowledge proof uh into your application how do you go about doing that typically zero

knowledge proofs are implemented using uh these arithmetic circuits so as you can see so you basically have some inputs you have these um you know Gates addition and multiplication and uh the circuit has some outputs but the important thing here is that addition and multiplication happens in some module or some prime number so you can essentially think of ZK circuits as far as this talk is concerned as a system of finite field equations right I'm going to represent the input variables of the circuit using X and output variables Y and in general uh as you probably know circuits also have some intermediate variables but uh you know just to simplify things I'm just going to write a circuit as C of XY

and kind of you know brush the intermediate variables under the rug to simplify things now zero knowledge circuits are very common and there have emerged many different domain specific languages that facilitate the implement ation of zero knowledge circuits so show hands how many of you are familiar with some of these languages okay yeah so there are bunch of languages in this talk I'll primarily focus on circum because our a lot of our work has focused on circum but there are variety of other languages like narc from consensus Halo 2 uh and a variety of others so now from the developers perspective here is how the general workflow uh occurs if you are trying to incorporate zero knowledge proofs in

into your application so first you pick your favorite domain specific language and you implement the ZK circuit in your dslo choice and then at that point the DSL compiler will do a lot of the heavy lifting it takes this high level circuit description and it compiles it down to some low-level constraint representation so for example R1 CS or uh plun and so on and then after that point that's where all the kind of the crypto uh Magic happens and then uh you know for what what I refer to as a crypto compiler this is not the main topic of the stock but for the purposes of this talk all we need to know is that after this low-level constraint uh we basically get aover and the verifier and

basically the prover takes your secret information and it will generate uh a proof of the statement uh that you would like to establish and then you can provide that proof to the verifier which will either say yes this is a valid proof or no uh this proof um looks in valid okay so that's the general workflow we have in mind well at this point you might say oh look this is great right all the hard work is already done for me the you know like all I need to do is Implement a ZK circuit this seems very easy to you know get zero knowledge proofs integrated into my application now that's true right the you know like all the uh cryptography system and the compiler does a lot of the hard work for you but uh you know

what I the point I want to make is that you shouldn't be lulled into this false sense of security even though a lot of the heavy lifting uh is being done for you because it's entirely possible that your circuit is wrong and as a result you get a wrong uh approver and a verifier and in particular if the circuit that you uh if the original circuit you implemented in your DSL has a bug then what's going to end up happening is that the prover is going to end up proving a different statement than the one you intended and similarly the verifier is going to be trying to verify a different statement than you wanted to verify but now at this point this begs the question okay I said you need to implement your circuit correctly

but what does it even mean for your circuit to be correct I'm a formal methods person and in formal methods whenever we talk about correctness it's always defined with respect to some specification right so ZK circuits is no different when we want to reason about the correctness of a circuit it's also defined with respect uh to some specification and in this context the specification you can think of it is it's the computation we want to certify so in particular I'm assuming that we're implementing a circuit that's intended to produce a proof that can certify that P of X is equal to Y that you know the secret such that P of X produces y basically we Define the correctness of

the circuit with respect to a computation p and the correctness of the circuit means that c of XY should evaluate to true if an only if P of X is equal to Y so it's saying this constraint evaluates to True only for those input output pairs that are feasible with respect to our computation right and if this Criterion is met then we say that uh the circuit is equivalent to our uh computation but unfortunately it turns out that many real world circuits violate this property because writing circuits turns out to be very uh non-trivial and in fact that my the startup I co-founded very guys we do audit a lot of um you know ZK circuits uh and we always find more bugs in ZK

circuits than other types of software like smart contracts or you know even blockchain implementations and this is the case uh you know even those ZK circuits are really developed by people who typically know what what they're doing and what they're talking about so based on this experience I really believe that it's crucial to develop formal methods techniques that can be used to improve the security of zero knowledge circuits and this is what this talk is going to be all about so I'm curious so previous on the previous slide is can you say anything about the types of bugs that you would so is it was it the case that you know you'd have CX y equal one for multiple y's with the same X was it that the Okay so Tim is asking a great question what are the

sources of bugs and you will learn all about that in you know in the in the next five 10 minutes yes yes so you're focusing entirely on like the the circuit layer not and not down not exactly there are many kinds of like bugs that are possible in different layers the circuit layer the integration layer the DSL layer the you know the crypto implementation of the uh the crypto system but what this to talk is focusing on is in the circuit layer itself exactly so here's kind of a little outline for the rest of the talk so I'm going to talk about two main projects so in the first part of the talk I'll tell you about a technique that allows us to verify an important property of ZK circuits namely that

they're deterministic in the second part of the talk um I'll talk about new uh constraint solver support uh targeting ZK circuits and finally I'll conclude with telling you about some of the other work and talking about uh future directions so let's start with the first part which is proving determinism of ZK circuits okay so to answer Tim's question it turns out that a common reason why uh circuits are often not equivalent to the computation that uh they're meant to certify is because they are under constraint so what do I mean by a circuit being under constraint well it basically means that for the same input X you can find two distinct outputs Y and Y Prime such that c of XY

and C of XY Prime both evaluate to True right so basically it's saying for the same inputs uh it evaluates the true for two distinct outputs now before we continue let's pause here a second and think about about why if a circuit is under constraint that's likely to be a bug so recall our definition of equivalence right so remember that equivalence says C should evaluate to True C of XY should evaluate to true if and only if P of X is equal to Y and this computation P that we're interested in is typically some deterministic computation right so basically that means on a given input x p can only produce a single y it shouldn't produce two distinct outputs Y and Y Prime but if the circuit is under constraint we

know that c of XY evaluates to true for two different values of Y so therefore if it's under constraint and assuming that P is a deterministic piece of computation if a circuit is under constraint it cannot be equivalent uh to whatever computation it's trying to certify so the moral of the story for us is that if a circuit is under constraint that means it cannot uh satisfy any uh equivalence for any deterministic computation so if we detect that the circuit is under constraint then you know there's very likely to uh to be a problem in your circuit now of course that said uh you know there are some you know this is not universally true in some cases the computation could be

non-deterministic but you know in many cases if a circuit is under constraint this is very likely to be a vulnerability and it's definitely something that uh you should uh give a second thought to and see if you really meant it to be uh non-determined istic okay so I bet a lot of people at this point say if there's a notion of under constraint well can a circuit can also be over constraint sure we can also you know come up with a definition of an over constraint circuit and intuitively uh an over constraint circuit says that for some input some input that perhaps satisfies some precondition there is no way to satisfy the circuit so there exists an X such that for all y c of XY

always evaluates to fall now are over constraint circuits buggy yes generally speaking over constraint circuits are also buggy but they're typically not as bad as under constrained ones so if basically a circuit is over constrained in some sense it's too conservative right so it's basically if you give it a valid proof it might reject the valid proof but if the circuit is under constraint then that's a soundness rather than completeness issue meaning that it may end up uh accepting proofs that it should not be accepting it accepts valid proof so therefore generally speaking under constrainted circuits are a lot more problematic uh than uh over constraint circuits yes so you we talked

about deterministic uh functions but often times if you add the Zer knowledge then things are definitely randomized the provs are randomized to to be able to hide the witness so that's typ a good question what about like um you know randomization that uh that's usually encoded as part of the input of the circuit yeah exactly and by the way I just want to make it clear that I'm not making this up this is not just an academic problem under constraint circuits are actually a real uh you know cause of vulnerabilities in practice and if you go and look there are you know like a bunch of vulnerabilities that are caused by circuits being under constrainted and they can cause a bunch of headaches and result in serious issues like draining tokens from an

account double spending and so on and to give further evidence to this there's actually a very nice empirical study paper that came out recently by stepanos chaloos at all where they basically did a largescale empirical study of a bunch of um you know known bugs in ZK circuits and what they found is that 95% of all known bugs are actually uh due to the Circuit being under constrained okay there was I think they looked that 99 problematic circuits in total and 94 of them were uh due to under constrainted one was over constrainted and the rest were like neither over constraint nor under neither over nor under constraint

but uh still not equivalent it's still hard to know how to interpret that right I mean it could be the under constrained ones are just much easier to find right over constrained ones sorry uh no it is true over constrainted ones are actually easier to test for in general all right yeah I was just wondering if there's like a sample bias in this statement at all yeah I'm not the author of the paper but uh I will one of them's in the room so I guess I could just ask one of them is in the room I could just ask him I guess so oh right s what was the question oh right okay now I just realized the author could that be sample bias could it be that the reason that 95% of all known bugs is ZK circuits who circuits just because those are the ones

that people happen to be able to find or have been looking for or something like that right I mean I think there's definitely a bias we we we debated for like a long time uh how how to even classify them right and there's definitely some cases where it's kind of like ambiguous so we try to outline as best as we can kind of like the methodology that we used objectively to kind of like classifying the circuits um and there's definitely also a sampling bias in the initial data set right so we kind of like went through all of the audit ports audit reports that we found and all of kind of like the the bug recollection uh GitHub repositories that we found which doesn't necessarily mean that this kind of like lists all the the the possibly observable bugs in general

right uh given that the space is also kind of like fairly nent right uh it's it's yeah it's it's fairly a fairly preliminary study of kind of like what's going to happen still in kind of like the next 5 to 10 years but it's I guess it raises a very important issue I guess what I'm curious to sort of close the like is there some puristic story you can say about how these circuits get specified where you'd actually kind of expect the common error would that be under constrain what do you mean could you repeat the question I think I think the question is like what is there a basic story for why you would expect this I think the classic story is like if your circuit is over constrained then it will fail basic testing like the exactly it's much easier to test for

yeah yeah because you give it a valid proof it's going to end up rejecting so that's what I meant by it's easier to detect but under constraint circuits are you know like by the time we get to look at the they go you know like they get released they're they have not been found through test so should be 95% of all known bugs that survived exactly yeah that's way of saying whether a circuit is under constraint is also kind of like debatable because it kind of like depends on the specification of kind of like the yeah what you actually want to prove right this is an all so is it okay if at this point I you know take back over because otherwise we'll never be able I'll never be able to get through my talk in the in the rest of the time okay so hopefully I've convinced Tim and

others in the audience that uh under constrained uh you know circuits are an issue in practice so based on this uh we recently developed a new technique for determining whether a circuit is under constraint or not and if you're interested in knowing more details this was published at last year's PDI and uh we also have a uh tool that we built uh that uh we uh use called pus so in the in the first part of the talk I'm going to tell you about how this tool actually works so before I tell you about how it works let's first kind of set up a straw man solution because there's an obvious way to solve the problem so recall that a circuit is under constraint the definition is very simple I can just write this one logical formula it says

you can find an X and two distinct outputs that both uh satisfy your circuit right now this immediately suggests and a very obvious way of solving the problem so you know as many of you who are formal methods uh you know who' talked to formal methods people know we love smt solvers right we love automated theorem provs so what we can do is you can take your circuit C you can encode it as an smt formula for example in the theory of integers or theory of uh finite fields and uh you give this formula to the smt solver and if it says this formula is set that means your circuit is under constraint if it says it's not set then that means

um you know it's properly constrained or it's means it's not under constraint well that's the obvious solution right and trust me that's the obviously the first thing that we tried but the um you know this this is not a very practical thing to do because it simply doesn't scale and why well you know real world ZK circuits tend to be pretty complicated things they have you know lots of you know constraints they have lots of you know intermediate signals there's lots of like nonlinearities uh you know everything is over finite field so if you you know in code everything as an smt formula and throw it at a solver it will just choke and not be able to you know even if you give it you know a very long amount of time it will not be able to terminate with an answer so what

we did uh instead is uh basically the idea underlying approach is to get a more scalable technique but that combines smt solving with a lighter weight static analysis technique and here's the key intuition uh underlying our approach so often you can look at you know parts of the circuit you can kind of eyeball uh your circuit and you can realize that some variable V Prime let's say can be expressed as a mathematical function of some other variables V in The Circuit by just doing kind of like a pattern matching approach and if this is the case if you can eyeball the circuit and realize that V Prime is f of v as as long as you know that all of these V's are deterministic

then you can also conclude that V Prime is also deterministic so let me give you an example to illustrate what I mean okay so here's a simple circuit that has an input X an output Y and an intermediate signal Z so if you look at the first constraint well da right clearly Z can be written as a mathematical function of X and if you look at the second constraint you also immediately see that y can be written as a function of x and z but since we already know that Z here is deterministic that means y can also be expressed as a function of X okay so therefore just doing this kind of very lightweight reasoning we can immediately conclude that the output variable is

indeed deterministic but in some cases well this is obvious in this case but in other cases it's not so obvious so let me give you another example so here we have an circuit with input X and three outputs y0 uh through Y2 and these three constraints here basically say each Yi is either zero or one and it says that the input X is basically uh the sum of the Yi scaled by 2 to the power I okay so in this case you can't just kind of look at the constraint and say yeah Yi can be written as a function of X or not actually let me ask you guys a question if you I'll give you a moment to kind of stare at the circuit let's look at it

for 30 seconds and let's do a show of hands who thinks this circuit is uh properly constrained or under constrained okay who thinks this circuit is looks good who says the circuit doesn't look good okay so the issue here whether the circuit is properly constrained or not it depends on what finite field we're working in it basically depends on kind of what the P value is so it turns out if p is less than or equal to seven then this circuit is going to be under constraint but as long as p is greater than seven then it is uh in fact properly constrained and um to see why that's the case let's let's consider what happens when p is 7 and X is zero well clearly

one uh possible satisfying assignment sets all of the outputs y i to zero right well clearly that's satisfied because they say Yi is either zero or one and clearly if you sum up a bunch of zeros you you get 0 equals z right if you look at the case where everything is one then again they uh the bit constraints are satisfied but now the key thing is that when we do the summation over integers get seven but remember that everything is happening mod P in this case p is seven so therefore the summation will uh in fact evaluate to zero so we get 0 equals 0 which is another satisfying assignment the moral of the story is that in some cases it's easy to kind of eyeball a

circuit and you know say yeah this signal can be written as a mathematical function of another signal but sometimes this is not so easy to do okay so our idea is basically to prove as many signals as possible to be deterministic by doing this lighter weight reasoning and we only want to resort to constraint solving only for the nonobvious cases where we run out of other possible solutions so this brings me to our technique which is uh basically at a high level you have this interactive Loop between two components namely the smt solver approach and the static analysis approach and these continuously exchange information with each other through a shared knowledge base and what does this shared knowledge base contain

well it contains two types of things so first it as deun was saying range information turns out to be useful so it will compute uh range information for all the signals but most importantly it basically has information about which signals have been proven to be deterministic and if at any point in this Loop we find that the output variables are a subset of the deterministic variables in our knowledge base that means the circuit is properly constrained otherwise uh we're going to First Resort to our static analysis because it's cheap and we're going to uh try to infer as much range information as possible and try to prove as many variables to be deterministic as possible and at some point we will no

longer be able to make progress using static analysis and when that happens we will hand things over to the smt solver and the smt solver will kind of continue the work started by this static analyzer and try to prove more signals to be deterministic but the good thing about this smt Sol is it can also potentially prove that an output signal is non-deterministic and if that's the case then uh if that happens we can conclude that uh the circuit is buggy but otherwise uh we keep uh repeating this until we can no longer make progress and if we didn't uh determine verified our uh buggy uh we can also return unknown and as you will see later the unknown

case will happens because of Sol solver timeouts right because when we make a query to to the smt solver it may not be able to provide an answer in some cases and the key point that I want to make here is that the smt solver and a static analyzer play a complementary role each other in the sense that partial results from one phase can be useful to the other as we will see shortly so let me talk about these two components in a bit more detail so the smt based reasoning takes as input our circuit c and a knowledge based KB and it will either say verified or buggy or if neither it's going to at least return an updated knowledge base that can be picked up by the static uh analyzer and what we do is

basically here is as you can imagine we first uh generate a logical encoding uh of the knowledge base everything that we know encode it as a logical formula and similarly encode the two copies of the circuit as a logical formula so we have one copy of the circuit over output variables Y and another copy over a different set of output variables y Prime and not that they all share the same X because we're trying to say we're trying to reason about what happens if they have the same input X can they have different outputs Y and Y Prime and then once we have this formula fee we're going to say for each signal s of C we're going to check whether our formula implies s is equal to S Prime and again s here is uh referring to the signal in

the first copy and S Prime in the other copy and if that's the case that means s is deterministic so it's going to be added to our knowledge base and similarly for each output not for the intermediate signals but for that just the outputs we're also going to see if Fe implies s is not equal to S Prime and if that's the case since s is an output we definitely know there's a problem and uh we're going to report the a counter example to the user and the important thing to note here is that the stronger the knowledge based in other words more information you have in your knowledge base in general the easier the query is going to be because you can use the information and the knowledge base to

essentially simplify your encoding of the circuit so I didn't make it very explicit here but you know when you know that some of the signals in the uh in the circuit are deterministic you can use that information to basically eliminate some of those y primes in your second copy of the circuit essentially okay so I think of X here is fixed or there's a for all x uh so it's an existential so it's we're saying does there exist a value of x yeah so let's turn our attention to the static analysis and as I mentioned earlier the uh what we're trying to do is for each signal s in the circuit we're trying to see if s can be expressed as a function of some other signals S1 through SN and if according to our knowledge base if we

know that each of if we know that all of the SI are deterministic that means s must also be deterministic so therefore s can also be added to the knowledge base now here's the thing that I want to emphasize again which is to note that the uh smt solver and the static uh analyzer play a complimentary role and that is because we may not be able to prove these some of these SI to be deterministic using the static analysis alone but we may be able to prove them using the smt solver so therefore they kind of support each other in the in the process and to give you more of an idea of how this static analysis works I'm not going to you know talk about the rules but just to give you some idea so be we have inference rules that are

written like this and basically whatever is on like this side of the Turn Style basically says we can prove that variable to be deterministic and whatever is on the right side uh the right hand side is the information we have available so for example Delta is our range information K are the signals uh that are known to be deterministic and C is our circuit and just to give you kind of like a sense for example we have this assign rule which says that let's say our your constraint has an equation of the form C * X is equal to e right so this is one of the syntactically one of the constraints in your circuit and you know that c is a nonzero constant and you've also proven e to be deterministic from that you can

conclude that X is also deterministic and if you're wondering you know where are these coming from well they basically reflect common patterns that we found in ZK circuits and they're based on rules that are manually proven to be sound so you can think of the static analysis here as essentially doing like pattern matching over uh a bunch of rules that have manually proven to be correct and if you take our implementation and run it uh on a circuit uh here is kind of to give you an idea of what uh it will look like so how many of you here are familiar with circum the one of the uh circuit languages okay anyway for the purposes of the talk you don't need to you know be able to read sarom code but uh the so basically as you can see there's an

input signal there's an output signal and there's some intermediate variables here and as I highlighted um here the problem is the loop termination condition essentially very classical error right there's an off by one error here and because the uh developer forgot to it basically because it says I less than n minus one instead of I less than n it happens that out of n minus one ends up being uh unconstrained here even though it's supposed to be constrained and if you take our tool and run it uh on this piece of code the output will look something like this so as you can see it's saying a bunch of propagation and this is where it's doing this kind of like pattern matching based static

analysis and it's able to prove some variables to be deterministic and at some point it invokes the smt solver and the smt solver returns a counter example and as you can see uh it says if you take in to be2 and if you look at the last variables I can you know like make them different so it's essentially giving us two different outputs that will satisfy the circuit and of course that's just one example so uh to evaluate our approach we did um a larger uh scale study so we gathered a a benchmark Suite from circum lip so this is the standard library of the circum language we looked at a total of 163 circuits and these contain on average

like 4,500 constraints and uh about 24 output signals and the key result here is that we were able to provide the definitive uh answer for 70% of these circuits so for 70% we were either able to say verified or uh under constraint and as expected because circum lib is very widely used and uh uh you would expect most of these benchmarks to be verified so out of those 101 circuits were verified and eight of them were reported to be under constraint and they were in fact under constraint this tool doesn't have uh false positives so to speak and if you're wondering where all of those buggy yes some of those correspondent to bugs but in other cases

we uh talked to developers and I I believe that in some cases they said we expected you know the circuit to be constrained at the call site uh for efficiency reasons for some of them that was some some of them were bugs and in some cases they were not okay so that concludes the first part of the talk uh if you have any quick questions I'm going to take uh a question or two oh any quick insights they failed the the the circuit that failed but uh by this tool and ins such Why Oh that's because of the uh so to repeat Dent's question why so in the cases there 30% of benchmarks where it can't produce an answer smt solar

timeout you basically we ran it with I forgot the exact time limit but I think it was like 1 minute or something like that but it was not able to say you know it wasn't able to decide sat or unsat with in that time frame so I I think you said both the static analyzer and the smt side they both contribute to the the knowledge base is that right correct yes yeah exactly yep um do you have plans to include more operations like lookups say to to this procedure oh like the lookup tables in the Halo 2 sense uh so this so when we if you look at the PDI paper that that I talked about it doesn't talk about that but we did some later work where we did where we working on like

Halo 2 support there's some basic support for lookup tables as well all right so in the second part of the talk I'm going to change gears and try to address the question that Dean was asking about like I said there are 30% of these circuits you know and even when we use a state-of-the-art smt solver for finite fields we get you know we're not able to solve 30% of the benchmarks and this is because of smt solare timeouts so the obvious question we asked is can we do better can we develop a decision procedure for finite fields that works better than the state of art at least for the types of practical queries that we care about and that brings me to um our new calf paper which uh talks about

a new uh solver for finite Fields based on the idea of split grubner bases and the key thing I'm going to tell you more about how this works but the key thing is that using our technique you can actually do much better when you're trying to answer determinism queries and in particular compared to the prior state of the art smt solver we can decide uh we can decide the satisfiability of three times as many queries within the same timeout compared to the previous state-of the art tool so the rest of the talk is going to be how did we uh get this kind of improvement what's the new decision procedure so uh first let me kind of you know recap the problem that we're trying to solve so

remember when we talk about smt solvers we're trying to decide some uh we're trying to decide satisfiability in some first order Theory and in our case the uh first order theory that we're working with is uh Prime order finite Fields right so in other words we have constants 0 through P minus one we only have two operators plus and times and these are addition and multiplication modulo R Prime p and we only have a single predicate equality and at this point I do want to make a little remark so if you remember the formulas that I I was showing you for determinism in general they can contain dise equalities like when I wrote Y is not equal to Y

Prime but for the uh we can actually ignore dise equalities because there's a you know way to get rid of dise equalities and turn them into equalities by introducing more variables and but it won't in a way that won't change the satisfiability of the formula so we can pretend that we only have uh equality and ignore dise equalities and so the problem we have is given a form uh in a prim order finite field is it satisfiable and I'm going to uh assume that the formula only has conjunctions because uh basically there's all this Machinery around smt solvers where you have the integration between the SAT solver and the first uh order Theory solver where all the Boolean structure

like the disjunctions and so on those are going to be handled by assat solver so the theory solver can only focus on formulas that only have conjunctions should I of the SATs piece it's just kind of easy basically like that the hard part is the smt part or it depends on the uh problem that you're working with there are formulas where the SAT the Boolean structure can be challenging but generally in this domain it turns out to be the finite field arithmetic that's very challenging so another thing I do want to point out here is because the only predicate we have equality is equality all of the formulas we have are of the form e is equal to e Prime and clearly we can write that as e minus E Prime is equal to zero and we have a

conjunction of those so that means we're basically interested in asking the question given a set of pols do these pols have common roots or not right does that make sense to everyone this reformulation so basically if I give you the upshot here is that if you take the uh problem of determining satisfiability you can have an alternative characterization of it which is that you're given a set of pols in FP let's say over variables X do these polinomial have common zeros or not so that's uh those are two equivalent characterizations of the problem so this is kind of the alternative uh problem statement is how we're going to view things but in order to kind of answer

this question we're going to need a little bit of background on algebraic geometry that's going to be very useful for answering this question so the first uh important background is uh the notion of an ideal just to recap basically if I give you a set of polinomial s the ideal that's generated by S is denoted using these brackets and basically it includes all polinomial that you can obtain by taking the pols in set s and multiplying them by arbitrary polinomial pi and then adding them up right so basically any polinomial that can be written in this form is in our ideal and uh the important thing for answering or for solving our problem is uh the following

important fact which is that if it turns out that one is in the ideal that's generated by S then polinomial and S do not have common zeros or in other words that means the formula is unsatisfiable so that's uh the basic thing that we're going to make use of so kind of to recap what that means is that if we have a way of proving that one isn't the ideal then that's uh one is in the ideal generated by S that's great then we have a proof that the formula is unsatisfiable but then that begs the question well how do you check if one is in the ideal that's generated by us or not so that's the ideal membership problem right for those of you who have uh who don't have background well it turns out that

there's a nice way of doing this using the concept of a grubner basis so basically if you have a given a set of polinomial you can compute something called a grubner basis and that's a very nice representation of the ideal that simplifies a bunch of computational problems and it turns out that if you have if you can compute a grubner basis for which there's an algorithm then you can also answer this ideal membership problem and this is exactly what the state ofth art the prior state-ofthe-art decision procedure does right so it first starts by Computing a grubner basis so given our set of polinomial s it goes ahead and uses this well-known algorithm or one of its many variants called B bers technique and it computes

a grubner basis of s then it does the ideal membership test which can can be done in linear time so if uh one is in the ideal it returns onset but here is the catch if one is not in the ideal generated by B this doesn't necessarily mean that the formula is set this result only holds for algebraically closed Fields but finite fields are not algebraically closed so therefore in that case if we cannot show that one is in the ideal we do need to resort to backtracking search in order to try to explicitly construct a model but even then having a grubar basis uh you can utilize various nice properties of the grubar basis to make backtracking search more tractable so you can make it um uh

you can basically use properties of the grubner bases to prune the search space okay but here's the problem right so when I you know when I was talking about the previous algorithm we said hey we can do the ideal membership thing in linear time I was expecting one of you like to ask but what about Computing the grubner bases well that's the bit that's sticky right well basically in the worst case grubner basis computation can be doubly exponential in the number of variables and unfortunately so you know like if you're doing verification usually if things are MP complete we've learned to deal with them right because like sat solvers are you know that's like the easiest problem for us right so we just basically say okay that's MP

complete not too bad how does it work in practice well unfortunately in this context for many problems of practical interest Computing a grer basis does end up being intractable so in this work what we ask is well can we at least avoid Computing the full grab ner basis can you kind of like computed partially do something so it doesn't like blow up in our face the answer turns out to be yes at least for answering determinism you can kind of get around Computing the full grubner basis and here's the key observation that we made that kind of drove the entire technique so if you look at the benchmarks where grubner bases computation really blows up these have a common pattern right they all turn out uh to require emulating bitwise

reasoning using finite field equations okay now I know what you guys are asking why the heck would you want to emulate bitwise reasoning using finite field equations well we're stuck with them right if you're writing a ZK circuits everything has to be expressed in terms of finite field so we don't have a choice if you want to do bitwise reasoning you somehow need to find a way of you know emulating it using finite Fields right right and to kind of give you intuition about uh what I mean so here is the constraint that we generate in fact it's uh very similar to the Circuit that we looked at earlier that you guys might have deu to that second example I was showing you earlier so as you can see here basically here we have

a bunch of bit constraints that says Yi is either zero or one and we have what I call these bits some constraints that say some variable can be written as the summation of Yi 2 to the power oi essentially you know you're doing bit splitting in order to emulate bitwise reasoning using finite field equations this is a very common pattern at least uh you know as I mentioned earlier we were our primary uh language that we were looking at was circum so we mined a bunch of circum projects and we found that 98% of circum projects have circuits that uh that exhibit this pattern now here's the important part so it turns out that if I give you the entire constraint system system it turns out to be difficult to compute a full

grubner basis for the whole system but you can compute it efficiently if you separate some parts of the constraint from the other so in particular if you isolate these bit sums from all the rest along with you know the bit sums plus all the linear stuff versus all the other nonlinear stuff then Computing a grubner basis for each of those in isolation turns out to be uh very uh practical so that's kind of the intuition behind our approach so we want to basically split the constraint system into multiple parts and uh compute grubner bases for those separately and then somehow iteratively refine them by exchanging relevant information so that brings me to kind of the contribution of

uh this Cal work which is the idea of a split grubner basis and basically um so given a set of pols in our finite field we say a split grubner basis is is a sequence of bases B1 through BN such that each bi needs to be a grer basis for some subset SI of s so we split s into S1 through SN we compute a grer basis bi for each of them separately and we also require that if you look at uh the ideal uh generated by S that needs to be equal to the ideal that's generated by the union of all of these bases right so you know in other words they kind of like Union up to our

original basis or our original ideal and there's a tradeoff here right uh so in general if you can compute a full grubner basis as we will see that contains more information that's more useful but it's harder to compute there are problems where you know it will just the computation will blow up on the other hand the split grubner basis is not as informative as the full grab ner basis but hopefully we can split it up in such a way that we'll be easier to compute so how do we use the split grer basis in our decision procedure so the first obvious fact is that if we can prove that one isn't the ideal generated by any of those bis then that means some subset of the polinomial don't have

common zero so therefore the full set of polinomial will clearly also not have common zeros right because we're looking at a subset of those right so basically by doing this uh by having a split grabner basis we can still determine in some cases whether the constraint system is satisfiable or not or whether it's unsatisfiable however as I mentioned it's not as informative because it could still be that even though one is not in the ideal generated by any bi it could still be that one is in the ideal that's generated by S so in this sense it's not as informative so what do we do so it seems like this part seems a bit problematic right because it seems like we're losing completeness so how do we recover completeness so recall what I

said earlier so even in the case where we compute the full grubner basis this doesn't give us a full decision procedure right because we don't have that nice if and only of property so even if we computed a full grubner basis we would still need to do some kind of backtracking search for uh for model construction so what if we have a split grubner basis we do the same we basically if we cannot prove unsatisfiability using any individual basis we're going to rely on backtracking search and furthermore we can still leverage the nice proper properties of each individual grubner basis to help us uh to do the search but as you can also Imagine when you have a split grubner basis the search algorithm itself gets more complicated and it also

in general can require more backtracking than if you had a full grubner basis so there's that trade-off now in addition what uh our technique does uh additionally to reduce the Reliance on search uh it relies on information exchange between different bases so it might give you this de feeling like the first part of the talk where you were doing information exchange between the smt solver and the static analyzer and here we do something similar right so in this split grubner basis approach we break our system into end different subparts we compute a grubner basis for each of them separately but after we compute a grubner basis we have this thing called the propagation module

which is going to kind of inspect each of the bases and it's going to try to do some reasoning you know if you added this it probably you know wouldn't make grubner basis computation much harder but it's potentially very useful so it basically propagates uh these polinomial back and forth uh and uh you can recompute the grubner bases with those added polinomial and the overall goal here is to construct a split grubner basis that's almost as useful as the full grubner basis but that is hopefully much much easier to compute uh than the full thing so one thing you might notice is that this what I described is kind of a decision procedure but at the same time not because it doesn't specify you

know many kinds of details for example how do you split these polinomial how does this propagation module work and you know you can instantiate it in many ways and it will still be sound and complete as we uh show in the paper but the particular way in which we instantiate it is motivated by the observation I made earlier which is that grubner basis Compu computation blows up when you do when you have these bit splitting constraints so in our specific instantiation of this algorithm we have we separate the constraint into two parts so we have the linear part which does include the bit sums because those are linear and we have everything else and then the propagation module

essentially focuses on inferring equalities based on bits some congruence so the very tailored towards that observation I made at the beginning and the key result is what I showed you at the very beginning if you look at satisfiability queries about determinism this technique you know makes a huge Improvement you can answer three times as many satisfiability queries as compared to the prior state of the art but now you might ask what about other types of benchmarks what about those that don't involve determinism and there the answer is mixed it depends on whether you're an optimist or pessimist whether you'll be happy about what I say so if you're an optimist it's good because it doesn't hurt anything but if you're a pessimist you know it doesn't

also doesn't make a big difference so this technique is primarily good at you know uh answering satisfiability queries that arise in the context of proving determinism but it doesn't hurt anything else so you might as well use it right so in the last few minutes that I have I also wanted to tell you about some of the other stuff that we've been thinking about and maybe some of you may be interested in uh collaborations so when I think of formal methods for for me the different tools we have come in a stack and the most foundational tools and formal methods are solvers like smt solvers sat solvers so those those for like the layer one of the formal method stack so once you have smt solvers uh uh then on top of those you can build

useful tools like verifiers and Bug finders and symbolic execution tools and then once you have verification tools you can also do more advanced stuff like you know synthesis can you you know synthesize software that's correct by Construction or synthesized circuits that are correct by construction and so on I would say that this whole area of formal methods for ZK circuits it's a pretty nent field so unsurprisingly a lot of the work so far has focused on the bottom two layers and I told you about some of the work that we did on solvers and verification but we also have some additional work in uh in the second layer that I also wanted to tell you a little bit about so generally speaking if I think of program analysis or you know verification techniques like

everything there's always a trade-off right everything comes in a big Spectrum so on one end of the spectrum you have full-fledged verification techniques that come with very strong guarantees right you can say I proved full functional correctness but they tend to be pretty heavyweight on the other end of the spectrum you have things like bug finding tools that give very weak guarantees so maybe they you know say oh they they can have both false positives they can also have false negatives but their advantage often is that they're much lighter weight right so there's a always a trade-off uh between different techniques and the technique that I told you about in the first part of the talk uh so I would say that falls somewhere in the middle it focuses on a specific

properties in particular proving determinism uh but it can at least you know say at least for the determinism property it's verified so it can give you some guarantees so you might ask well what about other kind of Alternatives in this design space so we also like buildt other tools that fall on different parts of the spectrum so for example in our recent YX 24 paper uh we described a technique that constructs this graph abstraction of ZK circuits and does you know analysis at the graph level and uh that's a much faster technique it doesn't require any smt solver support but it doesn't have any guarantees it can have false positives it can have false negatives we also

looked at the technique on the all the way on the other side of the spectrum so we actually have this uh programming language for ZK circuits called Koda and it's uses a refinement type system and then it basically uh you know when it does type checking it will output a bunch of uh Lemma so this technique is actually not fully automated it can verify full functional correctness but in the case where you know uh the built-in tactics fail a person needs to go and prove those lmas by hand so this is not fully automated and there are bunch of f future directions that we're interested in exploring that we some of them we uh already started on uh someone was asking about those so one

thing I'm very excited about is like I said a lot of our work has been focused on circum and R1 CS at the law Lev representation but you know they're constantly emerging dsls for um you know ZK for implementing ZK circuits who we're interested in building a verific verification friendly intermediate representation for ZK circuits that can support many different languages like narc Halo to uh sarum and others another thing that I'm very excited about is uh specialized solvers for integers plus finite fields and why am I excited about that because if you want to prove equivalence between computation and the circuit all the circuit constraints are

in finite Fields but all the computation use integers so if you want to you know reason in an automated way about uh about equivalence then you definitely need uh good smt solware support for theory of integers plus finite fields and currently uh we're also looking at more automated techniques that uh use smt solvers for verifying equivalence between ZK circuits and the computation they encode that don't rely on manual proofs using or lean or some other interactive theorem improver I wanted to acknowledge my collaborator so you guys invited me to give the talk but a lot of the work was actually done by others not me one of them is my PhD student Shankar pyure who's supposed to defend in a week

uh I'm trying to convince him very heart to defend as soon as possible Alex oir from Stanford is a PhD student that uh who's been collaborating with us so he was the lead person on this finite field solver and Al Pier who is a uh mathematician who was also one of the uh the big brains behind the um the second part of the talk that I mentioned so that's all I have thank you very much for inviting me [Applause]