Training for Constraining: How to Prevent Circuit-Level Bugs

Transcript

Hi. Um, I'm Levi Katy Sled. My colleague is VJ Singh. We work at Open Zeppelin. Um, in some ways I'm glad that uh I don't know how many of you were around for the previous workshop, but I'm glad that Alexander and Andre went before us because uh they talked about a uh kind of below the the the proof level at the information theory level of read Solomon codes. Now we're going to be talking about one level above the the zero knowledge proofs um in the form of uh arithmetic circuits and um and it's interesting uh the the levels kind of mix a little bit as well because sometimes you encode you know lower

level cryptographic things and into aic circuits but anyway I'll get to all that later I'm getting ahead of myself. So um ah okay so uh here's the outline. Uh first we're going to go through some motivation why this is an interesting problem. Um we're going to talk about uh the foundational topics of circuits and constraints. Um different kinds of under constraint bugs that can occur. Um then we're going to go into a little bit more detail into um a real um under constraint bug in the wild. Um and uh we're going to talk later about that uh how to find under constraint bugs and uh

address them and um as part of that we'll discuss uh our verification structure and AI and then we'll wrap up with some questions. So um motivation so um kind of um why do we care uh you know what is um what is the reason for talking about under constraint bugs under constraint circuits um so a lot of uh circuits have sort of been abstracted away there's a lot of libraries out there there's CKVMs so um may seem like a sort of solved problem but there are some uh vulnerabilities that occurred even in the past year on under constrained circuits. Um for example uh

we have you know this table up here um uh Zcash orchard there was a um missing binding of an ECC baseoint cell uh which you know allowed a counterfeit orchard value. Um not disclaimer none of this means that any of these were actually exploited just that the vulnerability was found. It was patched. Um, in the case of Zcash Orchard, it's um, impossible to really tell if there was ever an exploit of it, but um, you know, we think that it was not exploited. Um, uh, OpenVM pairing for example. Um, so uh, it's an example of um, missing hint validation, missing um, kind of sub

field check. Uh so uh allowed uh someone to forge uh potentially forge pairings. Um scroll EC pairing. Uh there's missing G2 subgroup membership check. Um if you don't know what G2 is, it's uh one of an one of two a billion groups in a pairing. Um and if you don't know what that is, don't worry about it. Uh it's a little outside the scope of this talk, but um just there was a missing check there. Um and uh so there's a possibility of sequence or improver disagreement and failure to finalize uh one of those proofs. And then uh another example was zkync air bender. Um so uh this sort of effective deferred

constraints and verifier composition and um basically is kind of um uh missing uh continuity check between two different steps in a larger proof uh larger circuit. And so this ended up uh uh appearing as three criticals in the in a report. Um and uh yeah so um we won't uh you know say so in the presentation but you know uh in the slides which you'll find on the repo you'll find uh appendices where we discussed and we link to the um to the reports.

Um okay sorry I'm going in the wrong direction. Uh okay. So circuits and constraints. Um so we're going to back up a little bit and we're going to discuss like um you know build up to to this stage how we get here. So um so uh let's talk about relations and witnesses. So uh complex claims like a ZKVM execution or a blockchain state transition. It can be expressed as knowing a secret witness uh that relates to some public information. Um so here's a really simple version of this kind of thing. Um you can say I know uh w contained in uh f11 the field with uh 11 elements. So 0 through 10 with uh

addition and multiplication such that um x= w 4 + 5 uh where w is a secret witness. X is a public witness. So everyone knows x only the provers w. And then you define that this relation r of wx holds if uh x is actually equal to w 4 plus 5 concretely. Um so usually what happens is that the private witness and public are vectors. So instead of in that simple example instead of like uh I feel like we're missing one subs slide here but okay. Um usually we have uh vectors of of uh private witness and public witness

elements. So not just one element but uh um and the public witness can be expected public inputs, outputs or both. Um so there may be a lot of these public lot of public information to check against. Uh so here's an applied example. Okay, this isn't slide good. So um uh suppose that we have uh W and that's just W not through W3 and that's those are secret witnesses. they're leaves of a oracle tree and then um x is uh just one element x knot and that's the public root and then we can define rwx as um if these secret witnesses um hash up to the uh to the root then that relation holds.

Um and then we didn't specify the hash function in here but it could be anything. um maybe a field friendly hash one like Poseidon or something. Um so another thing is that uh just for the rest of the presentation just so you know um we might use like letters instead of uh subscripts to denote different parts of the witness. Uh if it's clear which information is uh public and which is private. So we may use stuvw for witnesses secret witnesses and maybe xyz for public witnesses. Um okay so uh let's talk about arithmetic circuits a little bit. So an arithmetic circuit is uh like a boolean circuit. So you have wires, you have gates uh but

instead of um and or not gates stuff like that you have uh wires that carry values in um in a finite field uh and it could be other finite fields but we're just going to focus on prime fields. Um so FP and then the gates are addition and multiplication modulo P uh instead of and or not etc. And the right so the um calculation is just in addition to modul multiplication um and uh by the way just as an aside um why would we want to do this? Uh so an arithmetic circuit uh can model any bounded computation. Um and you think

okay well maybe I don't want just bounded computation I want four loops and while loops and things like that um but it's actually sufficient most of the time because every run through an unbounded computation uh is equivalent to some bounded computation. So if a computation already happened you can sort of model that as a bounded computation. Um so this is kind of an a little motivation there. So um the thing is that you can uh take an arithmetic circuit and you can you know make it equivalent to a system of constraints. So one for each gate you have a plus or times operation. Um and then there are also other kinds of constraint systems that are a little bit

more complicated than just plus and times. But the point is that they're all equivalent in what they can express. Um so here's a an example. So um let's take this constraint system C which is C not K through C3. Um and uh C kn says that W1 = W KN 2 W2= W1 2. Notice that putting these two together that means that W2= WN 4th W3= W2 + 5 and then W3= X0 or X0 is some public thing. Um so again here X knot is the public witness. Uh W knot is the secret witness. Um

and W1 through W3 are intermediate witnesses. Uh so in one sense they're all the same. The input W knot and the intermediate witnesses uh W1 through W3. But it just helps us distinguish you know what is an input to the circuit versus what are some intermediate values that we might want to compute uh to get the output. Um and the combination of both of these is W bar. I mean we're calling it W bar. It's the extended witness. Uh so your inputs plus whatever you calculate along the way. uh and then we write that w bar x satisfies c if for that concrete w bar and x all those

constraints c1 c through c3 all of them hold simultaneously. Um and as we mentioned before, if you think about this calculation, what this is saying for this particular C is that wx satisfies the implies that x= w kn 4 + 5. Uh and also if we have um an x knot which is w 4 + 5, we can choose these intermediate values satisfying c. This just kind of means that we have modeled our relation of uh taking something to the fourth and then adding five um as uh a system of constraints.

Um so here's the kind of like chain of steps or you can also think of it as a little bit like a ladder of abstraction um for snarks. So basically um you have this intended specification or intended relation R um which kind of tells you like what am I trying to do? What what am I trying to prove about the inputs and the outputs? What am I trying to compute? Um then you compile them to constraint C uh just as we did in the last slide. Uh then the prover takes uh their input the public output and then they uh calculate

uh honestly or dishonestly um but they calculate a w bar uh so some extension of this input um and then this uh uh x um and then from this they generate a proof pi. So this step here from W to W bar is called witness generation and this step over here is called proof generation. Then this is verification. So the verifier takes uh pi and x and then it outputs a boolean saying do I accept or do I reject this proof? Is this a good proof? Is this a bad proof?

So ideally what we want is that um this wx satisfies C if and only if this relation holds between the input and the um x here. So uh if and only if rwx um and then also this is another sort of flavor of this is for public statement specification we might want to prove that there exists some witness that satisfies the constraints if and only if this relation holds or there exists a w where this relation holds.

Um and an application can fail when one of the implication fails even if the proof system works. So we're not talking about proof systems at all in this talk. it's all about the arithmetic circuits which kind of sit above them. Um so we're assuming that the proof system works totally fine. Uh everything's you know everything's good with that. But uh still if the if this intended implication doesn't really hold then you can still get cheating provers. Um so another thing I'd like to discuss is hints. Um so there's a honest computation where you take say for

example you want to calculate t and you set it to w ^2 u and the prover is computing a hint which is outside the circuit um and if it's if the prover is honest they'll use some witness generation which is like you know supplied by uh whoever writes the circuit or the verifier um and uh the answer that's provided by this generator is called advice but The prover can ignore advice. They don't have to do this. They don't have to assign t to w ^2. On the other hand, if the constraints have this enforced equation tus w ^2= 0, then they have to set t to w ^2. Otherwise, this will never hold and then they won't be able to to pass proof. Um,

so uh the thing that you want to keep in mind with these is the adversarial model. So the reprover can replace a witness generator, ignore advice, substitute their own hints. Hints are unless you constrain them some other way, they're kind of unconstrained. Um, and only the enforced constraints bind these choices. Okay, so what kinds of under constraint bugs tend to happen? Uh, so here are some common failure patterns. So one is that there's um a missing copy constraint. uh and so wires can disconnect, values can disagree. Um you want to port the uh output from one submputation to another computation and

that doesn't work. Those don't match up. Uh that can be a bad thing. Um you can miss a range check. So you can get an over or underflow value depending on what you intended or some other unexpected value. Um hint validation. This is the big one. Um, and uh, by the way, like why um, why do we kind of allow hints at all? Um, might be best to see with this with an example, but sometimes having a hint and then verifying that hint and some kind of you have to kind of think backwards from the verifier's point of view.

Sometimes that's the only good option that you have. Um, otherwise the you get some very prohibitively expensive. Um but if you don't validate correctly then the prover controls the computation and then they can sort of forge whatever they like for that computation or something similar. Um another thing that can happen is that you miss a field or subgroup membership check uh and your algebraic properties that you want or they're guaranteed inside the subgroup or the sub field don't actually hold in the in the greater uh domain. Um and then there's um public witness binding.

It's kind of like the same as a missing copy constraint, but it's different type of it. It's like you do some computation and then the output might not uh might not be bound correctly to what you want it to be bound to. So it's a little vague, but we'll get into some examples. Um so uh let's do first example zero missing public output binding. Um so suppose that we have uh you remember our set of constraints C the constraint that X= W 4 + 5. Uh suppose that we just eliminate the last constraint from it which is W3= X KN. Um so we still compute W3= um W to 4 + 5 but then we just leave the the

last part out. So then maybe you can make this false claim. You say I know a w knot with w to kn 4th + 5= 7. Uh that would mean that w to the 4th equals 2. Uh and I just printed out this table so that you don't have to like take everything to the fourth yourself. But everything in f11 if you take it to the fourth it does not equal to. So this cannot be this cannot happen. Um but if you if you just put something in for w knot then you can have um you know w bar is equal to 1 and then you square that get one square that again get one

at five get six uh x not equ= 7 but they're not bound so it still passes. Um so the repair of this is obviously just restore the the binding from your uh computation to the output. Um and that's the only link between what the circuit computes and what the verifier sees. Okay. Um so example one like unvalidated hints. Uh so let's take this um uh W in F11 a secret witness and X in F11 a public witness and we want to constrain this relation r of wx holds if x is is zero of w meaning x is one if w is zero and x is zero of w is non zero.

Okay. Um so the thing is that uh you know you can you can try to do inverses using like extended uklitian algorithm and then try to model like the integers inside your circuit and like do all that and compute it in the forward direction. But the best thing to do is to comput it in the backward direction and say give me something that's the inverse and then if it multiplies to the other thing and it equals one then we're good. So this is the idea. So let h be a secret hint. And then a witness generator advises that h should be w inverse if w is non zero and it should be zero w is z.

Um and let's suppose that we just have this constraint that x= 1 - w. Um so you can see that this kind of models what we're going for here because if uh h is w okay so if w is non zero then h is w inverse then you have one here then x is zero. So if uh w is um non zero then x is zero and then if w is zero then you have 1 minus 0 and then x is uh one. So looks like that should work. Uh unfortunately it doesn't. So um if you take w= 3, h= 0 and x= 1 um so this holds because then you have

um 1 = 1 - 3 * 0 uh but is 0 of 3 = 1. So is 3 equal to 0 uh equals true? No, that's not the case. Um so something went wrong. Okay, so what the repair is for this is you want to constrain the hints effect. So basically you add this extra constraint um wx equals 0. And why would you do that? Well okay um if uh w is non zero then x is zero um because the reason we're using fields is that they have the zero product property. So then we have um cot forces that h is w inverse. Um and before we could sort of do whatever

we wanted with h but now we can't. We have to make it w inverse for this to hold. Um now if w equals 0 then uh you have x= 1 and then the value of h doesn't matter at all. Um so uh you notice that if w equals z you can put anything you want in for h which means that there are many different extended witnesses that correspond that you can still use and constrain the same relation. So um a hint may not have a unique representation. There may be multiple W bar for a given W but the public behavior must be pinned down by the constraints.

Okay. Uh so I'm going to give you all an exercise. Um so uh the intended behavior is that we have S in 01 and it selects S or Y. So we're just making a selector circuit. Z is uh X if S is one and Y if S is zero. So that's what we want to achieve. Um and we have uh a constraint over F11 which says this that uh Z is sx + 1 - s y. Um so here let's say that x and y are secret inputs and fix a public output z

equals 5. Um okay. And then the selector S is also secret. Um so uh I want you to take two minutes with your neighbor and try to find um an S so that uh even with x= 3 and y= 7. So neither of them equaling five. Can you choose s so that the equation accepts? And then in that case which constraint is missing? So, I'll give you a couple minutes and then we'll move Okay. Uh, does anyone have a value of s

that they wanted to shout out? Yes, two. Uh, I got six, but okay. Um, but the point is there is one, right? So um if x is 6 and f11 then you have uh 6 * 3 + 1 - 6 * 7. Um so that's going to be 18 - 35 and then that's - 17 which is 5 mod 11. Um and uh you know the thing that you notice which is that s doesn't have to be zero or one. We never constrained that. So uh so this is like one example where you can get five um and uh so so what do we do? We have to actually

constrain that s is equal to 0 or 1. And one way we can do that with polinomials is to say s * s - 1 equals z. Uh and that forces that s is equal to 0 or s is equal to one. Then everything holds that we want to hold. And this is actually a selector. Okay. Um and uh I'll go through a little quickly um some uh examples on uh range checks and foreign field arithmetic because it's a little um helpful to understand the the the bugs that we're going to be talking about in a minute.

So um so what we did uh in the last slide was we took s and we forced it to be either zero or one. You can think of that as s is in the range of zero uh up to two not including two something like that. So that's a range check on a single value which uh makes it a single bit. Um and uh one thing is that you can't really talk about field elements being greater than or less known one another uh in general. Um so that's kind of disappointing, right? Like in in F11 you

have uh min -2= 9. So how do you say that you know there are no real negative numbers. So how do you compare two different numbers? Um and this might be a problem because you want to say something like balance greater than equal to withdrawal or something like that uh in your circuit. Um but you can do this. It's just requires a little extra effort. you use a range check um and you can read uh like x for example as a as an integer in 0 to p minus one and then uh show that x is less than 2 to the n um n has to be small enough for this to work though. So um so for example like if you have uh x

you want to say that x is less than 4 in f11 then you uh decompose it into bits you say x= w + 2 * w1 and then you have to constrain both w9 and w1 to be bits. So there's bit decomposition that's a kind of range check. Um and then uh yes this holds. So uh x has to be 0 1 2 or 3. So x is less than four. Um but you have to make sure that uh when you're doing these bit decompositions that you don't try to do too much and try to bit decompose numbers that are too large. Uh if they overflow the field modulus then you're going to have a problem. So um if you want to say that uh say x is less

than 8 then you have a bit of a problem because then uh you have nonunique bit representations of the same x. Um so uh and there's another concept which is kind of important uh in general with circuits which is like uh some people call it non-native field arithmetic. I call it foreign field arithmetic just to eliminate a double negative. Um but anyway uh you might want to like uh check um arithmetic modulo some other field or modulo you know some other modulus um which is not equal to your native field um which is the the p that

all these um belong to. uh so that is um uh especially important in elliptic curve scalar computations like inside um inside a circuit. So what you can do is you can do this trick. You can take a uh express it in base B where B is small enough uh and then you can kind of decompose it into limbs and then you range check every limb uh so that you have this decomposition. Uh so just like with bits but you can be in different bases other than binary. Um and you need to choose B small enough so the limb products and carry stable OP and then you you know you have to reduce after a

certain number of steps um you know depending on uh how small your uh field is compared to the native field. So etc. Um so uh for example to show that ab equals c mod l um then the prover has to hint a quotient k uh and the circuit checks that ab= kl + c. So you see that this uh kl term drops out if you consider the equation mod l and then you get a= c mod l. Uh but you need to range check k and c. So um so just a very small example like uh if you have um foreign field f3 so l= 3 and public x y and z uh in 012 then

you check xy= z mod 3 with uh c 0 = xy - z = 3 k but um you have a problem here. If k is not range checked then you can just set it to 3 inverse which is four and then you get uh k= 4 * uh x yus z and then whatever your x y and z are you can satisfy this uh so so then it's kind of under constrained so then what you need to do is you need to uh range check k and in this case it's sufficient to uh say that k is zero or one. So k * k - 1 equals 0.

Um and so what's the lesson here? Um so you have to range check the quotient and every other term so that the negative equation can't wrap. So, uh, and this is kind of I mean it's a little bit more complicated than this, but this is kind of what happened with the Garch fake GLV bug, which is a bug that we found in the wild. And it's it's um I mean uh it's a good example to learn from uh um and how uh these can go wrong. So um let me look at time for a second.

Okay. Um, so yeah, uh, the fake GLV bug. What is that? So, uh, what is, uh, fake GLV anyway? Um, so basically you're trying to, um, do an elliptic curve, uh, scalar multiplication. You have a point uh, P, you want to multiply by a scalar X, and then prover tells you the output is Q, this other curve point. And then um instead of just calculating uh s uh scalar time p which is a lot of doubling and adding you can save some time by decomposing it this way. Um if u p= vq and this scalar relation

holds so u is congruent to sv mod l and p and q belong to this prime order subgroup. Um and this is the situation that we hope to be in. uh P and Q belong into that uh subgroup then um V * Q - S * P equals the identity point O and then that means that uh Q equals uh S * P. Okay, so if you didn't understand all that that's fine. Um but the thing is that this has kind of some assumptions here and every one of them needs enforcement which is what we're going to talk about. So um so we have two fields to think about.

We have the native circuit field modulus uh FR um and then we have a prime subgroup which we're talking about P and Q being in and those are scalers modulo L. Okay, so our scalers are coming from L but our uh arithmetic circuit elements are all FR. Um so like uh for baby jub jub in a bn 254 circuit r does not equal l. I mean these are just um you know uh fields and and and so forth. So doesn't uh if you don't know about baby jab and bn 254 no problem. It's just they're different. That's the only uh thing you

need to know. Um so u congrent to sv l is a relation in the scalar domain. But this equation is evaluated in FR. So um so the the simplified form of the vulnerable binding check here was just that uh u minus SV= KL in in FR. So this is there I'm trying to constrain that U is congruent to uh to SV mod L. Um however uh the problem is that K is prover supplied and the prover can do whatever they want. So um uh they can just set um this to be U -

SV * L inverse mod R. And so um since K isn't constrained by something else uh you can just solve for it and then you can get a K that works. Um, and so there's no real binding between US and V there. Uh, so here's the the code before the fix. Um, and uh, and so, uh, the plus or minus is uh, not too important, but um, but basically uh, it's just letting u both branches kind of are left free to um, uh, absorb K. So the balance on S and Y and S2 don't bind

K. Um and okay. So what does this actually imply? Um you know what does this bug mean? What can we do with it? If we're a cheating prover um if we're a cheating prover we can choose u= 0als 1 and q is the identity point. We get up= vq which is the identity point. Um and uh we can you know the free quotient satisfies this native field equation for any s. So basically uh the gadget accepts q equals z even when sp doesn't equal z. Um okay why is that bad? Because um if this is used in a signature verification algorithm for example, uh then you have this equation which can

only is only supposed to hold if um the prover has a um a assigning key. Okay. But then um this H A uh is uh if it's replaced by O, then you're not bound to the private key at all. So you can just sort of um uh assert any kind of private key you want and it's not adequately bound to the public key and then you can forge messages. So um that's really bad. Uh so um so what do you actually have to enforce?

So um in this example and then we'll move on after um after we're done talking about this but uh you have to have this you have to enforce this congruence properly. So you need to um implement this foreign field arithmetic simulate this other field inside this uh the native field. Um you need to ensure that P and Q are indeed part of this prime order subgroup. Uh you need to ensure that V is not equal to zero mod L. And then you need to um you know have your constraints on signs decomposition bound and selected branches. Okay, so that's kind of a lot that you need to constrain just to just to optimize one scalar uh multiplication.

Um and as an aside um you know why do we keep getting um you know under constraint bugs? uh one place to look for them is in optimizations cuz a lot of times you'll say okay uh I have this big long computation it costs a lot to do to put it in an arithmetic circuit and then prove it in our proving system but if I do some uh optimization of it I have much fewer uh constraints to prove the the prover can throw some hints in there but I'll verify all of them in some clever way but if the verification is a little bit off in that optimization That's where a lot of bugs occur. Um, so,

uh, I'm going to hand it to, uh, VJ for the rest of the, uh, talk and he's going to, um, talk about, uh, how we can, uh, spot these, um, vulnerabilities and and prevent them. >> Thanks, Eva. Yeah, cool. This goes down. >> Okay. All righty. So, how do we find the, right? So, >> Oh, yeah. Okay. All right. Not used to it. But let's see. So yeah. So first um so this is how we start generally you know if you're an auditor you want to audit this. So well first step would be to write down the you know uh the intended domain. Uh a good example to keep in mind is a selector right you want selector generally the selector is

between zero and one. I mean you know uh the different kind of selectors but then essentially you mark public witness secret witness hints and selectors. Um again uh you'll see that in a moment. Uh uh there's some flexibility on how you you go about uh checking them. Then you you basically look at the constraints which bind you know uh in the individual ones right okay and then you try a value outside the intended domain and see whether you know it still satisfies. If it still satisfies, then you're in trouble because that means you have an under constraint circuit.

And uh then what you do is if you find the under constraint or if you find a missing constraint, you you throw in the missing constraint again and then you know keep doing this uh until you get a complete picture of what's uh what the bugs are. Okay. So um all right. So um so what are we doing here? So uh recall uh you have basically you have uh honest witness uh essentially um uh is uh W bar from the you know from the introduction.

So you are having what you have is you have a honest witness uh uh satisfying the constraint. Um so suppose now you're trying to see what uh what basically fails right so if you're just checking the honest witness you're not going to get anything out of it right because honest witness must satisfy I mean that's the basic completeness property what you really want is something which is not an honest witness and satisfying it so essentially what you're looking at is something a witness such that it satisfies the constraint but does not satisfy the relation Right? So you can see that that's an ant there. Right? So you have this uh system for which you want to

basically uh you know find find solution. Right. So all right. So now how do you find such a witness uh which what which satisfy the constraint but it's not in the relation. So it's it's a bad bad or counter example. So well one way is essentially uh you can do randomly. a lot of people I mean there's a there's a whole uh setup where you do fuzzing right so you you throw in and check >> there are some more systematic way of fuzzing as well you just don't randomly do it but you have some idea where your uh bad counter examples may come from but again it's it's still uh still a

still a problem okay so question is is there a systematic way of uh of uh of going about it I I'll move forward because I just want you to give quickly you know the the nice kid in the candy store kind of a experience uh with the problem. So I'll I'll skip this slide actually and move ahead. So uh and I'll first talk about the formal verification. Uh so what are we trying to do again? uh we are trying to find out a a witness uh a a bad witness in the sense that something which is uh you know satisfying the constraint but not in the uh what do you say not in the in the not satisfying the relation so what you can do is you can convert this into

a sad problem all right so it's a satisfiability problem uh and then you check right so if you if you get a solution to this that means you have found a counter example so if sat basically passes you get a witness uh you get counter example to this uh setup. If you have an unsat that means what that means you do not have a bad example in this model right whatever you have modeled as as for your formal verification and if it is unknown then that means you know you ran a program it did not converge did not stop you know kept on going forever right so for example uh if you see uh quickly for the selectors you had z equals to this what will be the

what will be the setup that you have z equals to sx + 1 - sy that is your constraint Right? And then you have what? What will be the negative of the relation? Uh it's instead of zed belonging to XY, it's negative of that. That means does Zed does not belongs to XY. Right? So so this is a setup and uh you you basically add this to it because you want to enforce the booleanness of S and then you'll see that uh it basically is unsat, right? So so it basically says that you have a proof that you know there's no counter example to this. So it's it's verified and it's quite fast actually you know. Okay. Now what next? Well I mean imagine so when you're doing the

SAD problem for each of those witness or intermediate witness you have a variable associated to them. Then you can think about a huge I mean if there's something called as ring or and over the ring you're trying to basically uh you have this big ideal membership problem you know and then to solve that it's actually crazy. I mean the number of variables if they keep increasing uh then then you know it's unsolvable essentially even with the formalism. Okay. So uh but but at this moment what are the formal verification scenario available. So part of it is here. So you basically take all these you know circom hello2 plonkey and all these things and convert it into one

uh you know mechanism or representation which your which your you know computer can read. Uh so LLCK is one uh of the uh interesting um open-source project uh developed by Veradise funded by Ethereum Foundation. It's a uh uh so you can convert it into some uh uh representation and then you can have different hammer to solve that problem. For example, you can run an SMT solver, right? But it could be that you have too many variables and then you can't solve it. So well, you can try some lean proofs right?

uh you have basically you know some some some other mechanisms to to to go about it right so so so this is a scenario of the formal verification but let me just tell you a few things so the the lacking part is for example you know something may not be solvable you know you don't have enough resources to solve again the example of empty solver if you have a bit some decomposition then the sat can only do so much there are some advant sciences in that area. Uh but uh like split groer bases and stuff like that but uh still there are interesting problems to look at. It's a good research problem to to have. Um yeah so next uh is well formal verification is

not enough as we see um and also for other reasons too. Uh the other reasons are suppose you have a dependency. Yeah. uh so uh if you're running say something on top of narc you either check the whole of the narc as well right I mean the proper formal verification would be going all the way to the basic step right you cannot do that all the time I mean why the program will not converge essentially so what you do is then then you start using some AI infrastructure on top of so AI infrastructure can help you basically with some advisories like imagine this narciss issue actually came out like in August sometime time you know I mean we know finite field elliptic curve for such a long time we have complete I mean almost complete

understanding of this mechanism but still these bugs actually go unnoticed so you could have some kind of an uh relevant advisory like you know tells you what are the bugs uh which come out for example secondly um yeah so it it helps you um prototype your stuff first right um and then uh yeah and helps you with the you crafting your your stuff, right? So, pretty fast. All right. So, how do we go about it at at open zeppelin? Just quick so we have a AI auditor which basically does this tracing and hypothesis. I'm specifically talking about ZK stuff, right? Not outside. Yeah. Then uh essentially we we have a mechanism uh we

have a we go with the LLZK route uh which is open source and we have built something on top of that as well. Um then we have lean proofs. So for example, if you have a elliptic curve uh you know uh operation like doubling or signatures, right? So you could just like you know uh get the the mathematical um what do you say representation out of it and check in lean if that that operation is done correctly, right? So checking formulas, right? Okay. And then of course we need human auditors precisely, you know, because well I mean these none of these mechanisms on their own are complete.

Yeah, it's getting there but but but not not there yet, right? So, yeah. So, well, uh this is uh the whole setup uh I mean at least uh the most of the setup for for trying to find out the bugs in ZK mostly in the under constraint but also outside too but uh all right so am I going in the other direction? All right. So questions. Uh you can run some of these by yourself. Uh that's a link for the u you know the repo. Have a look. Uh u there are some demos we have for you. And yeah I mean um just to end I mean this is a very exciting uh area.

I think Derek talked about it yesterday right like so you know yeah if you if you have any questions or anything in particular please feel free to reach out to us. Yeah. Cool. Thanks. We have 2 minutes. So one question maybe. Do you think there will eventually be integrated into Ethereum? Because for example if something like uh uh is stored on chain and could be no without revealing the secrets. Yeah.

Um I I think ideally do you have any? Yeah. Yeah. I think ideally it should be at at some point right I mean it depends on how uh how things are built right like so for example now we have these many uh other things built on top of Ethereums like you know where you have privacy solutions right so you know you have sama you have other things so I I'm not 100% sure that should ethereum itself do it I don't know I mean but uh yeah but there are layer two solutions or you can call it some solutions on top which actually already do this.

>> Okay, thank you. >> Thanks. >> Uh my question is specifically about witnesses. Is there such thing as a private and public witnesses or are private witnesses um a kind of like a specific witness with like a blinding factor or something? Um yeah, so there uh um it eventually uh comes down to the verification algorithm and then the verifier takes in the public witnesses

but does not take in the private witnesses just takes in the proof that was generated by the prover based on their private witnesses. So only the prover gets to see the private witnesses. Um and uh but the verifier learns something about them if the circuit is journaled correctly uh but not too much uh because it's you know uh you may you want preserve some privacy with ZK um yeah uh but does not see the private witnesses. >> Yeah. So so witness is essentially the solution to the equation right. So you know for example hints could be public some of it right. So um I think yeah so there's a mix of public and private

right. >> Yes. >> How did you uh I mean so you created the lean models automatically. I will were they syn synthesized automatically? >> Sorry which model >> the lean models. Uh yeah. Uh so yeah we basically say for example um we run say there is a there is a repo which is implementing elliptic curve edition right so we try to extract it using AI right I mean like you know we are not going to code it right sure yeah and then we check it in our lean that oh does it really satisfies that equation or not >> sure sure so one thing that's been cropping up um cropping up quite a few

places is that lean models uh may prove something which may not be strong enough what you would I mean basically the lean model may not capture the intent the user intent >> so it may end up proving something >> um and it may give a false indication that well the circuit is correct um so I just wanted to understand uh have you guys been looking at what these models are um in do review >> so sure okay so first of all yeah so lean model we are using leans mostly to verify the formulas right so Yeah, there are two problems. Formula is correct but the input is not like you know you can still have a good formula but as you say I mean if you don't bound your inputs then there's a issue right so uh yeah so

we are using these kind of setup to to solve the problem right so uh and if you look at zk stuff uh it's actually I mean I would dare to say that most of the problems are mathematically simple right you look at the selector or or those problems are actually pretty pretty simple to understand right they're not deep math mathematical like you know you're not we are not solving Navia Stokes or something at least not as so so um the the math equations are simple it is just that the you know because we don't constrain them properly they tend to go all all all crazy right so so look at snark for example I mean you know I mean what are the prototypes they are very well understood uh things you know ashes elliptic curve elliptic curve has

been studied since I don't know time immemorial I don't you know so so so So we are just in time. Uh speakers will be here for additional questions. Please