ZK10: Pushing the limits in the automated detection of vulnerabilities in ZKP circuits

Transcript

foreign [Music] our next Workshop is going to be from the folks at verdice I'm looking at pushing the limits of automated detection of vulnerabilities in ZK circuits we'll have John Daniel and Alf presenting various parts of the presentation to start it off I'll hand over to John hello uh it's been a bit of a a bit of an adventure getting everything working here and so luckily we've managed to record some things just in case this eventuality came uh but yeah

so we're going to be talking about a couple of different things uh we're going to be talking about some common bugs in ZK circuits so I want to give a little bit of a disclaimer here this is mainly going to focus on bugs within the circuit logic rather than in applications in general so there's going to be certain types of bugs that we aren't going to cover like uh application Level bugs like not checking nullifiers in your application or issues and hashing functions that can reduce the security guarantees that hashing functions can give you and stuff like that instead we're just going to be looking at logical errors within bugs themselves or within circuits themselves then we're going to be looking at some ways that veridice has been developing

in order to identify these bugs automatically and so I'll be in the first part of the talk then Daniel will be starting to talk about static analysis and how to identify bugs in ZK circuits and then finally Alp we'll be talking about how to use some graph theoretical Notions in order to simplify the process of solving some of these problems and so uh mainly I am just here to give the introduction and so uh we're going to start with kind of the classical notion what is a ZK circuit I assume that most of the people in this audience are going to be aware of how a ZK circuit actually works but just in case

I'll quickly go through this so basically uh the way a ZK circuit is going to work is you're going to have a circuit written in some language that could be a circom Halo 2 Arc Works uh snarky 2 doesn't really matter the the DSL or the language but basically what you're going to get out of that is you're going to get a witness generator which will generate your witness that witness is going to include an assignment to all of your signals and then you're also going to get a set of polynomial field equations and so this could be in a couple of different formats depending on the proving system that you're using so this could be r1cs like a plonk table it doesn't really matter there are still equations that are going to have to be satisfied by your circuit and then those equations are going to be

used by the prover and the verifier in order to prove that you know you have actually run this computation and then verify that the computation has been run at the end and so the important thing is unlike in traditional programming languages now your source code is going to contain two things it's going to contain computation and constraints and so traditionally in programming you're just expressing a program and so we are going this notion is important because we're going to take advantage of it in several of the future parts of our work so we are going to be showing most of our examples in circom the concepts that we're going to introduce here are not

specific to circon but when it comes to showing circuits it's just a little bit easier to show in circum just because we can kind of directly show the computation without having to worry about whether or not you know rust or a particular API and so I'm going to quickly go over some of the circon basics and if you have any questions let me know also throughout the presentation if you have questions just raise your hand shout them out doesn't really matter we're not going to be very formal about this but basically if we look at the circon program we can separate the components that we just talked about so and the circum component you can take this circuit and you can separate it into the computation component and so that's going to be this right here you can tell

what this is because in circum there's basically going to be three different types of operators in order to perform assignments and equality checking so your first one which is that arrow with the two dashes is only going to express something in your computation so you can see right here that division ends up going in here and then also the arrow with the double equal sign will also Place something in your computation however it will also generate constraints as we talked about previously and so constraints and circle are expressed using this triple equal sign and so you can see here in our original circuit you had that operation with the triple equals which uh ends up being

encoded in your computation and also the arrow with the double equals also encodes a constraint and so one thing that you'll notice is it's always safest to use the arrow with the double equals but there are some times when you can't express something as a constraint and so you might have to mix and match these operations so specifically just because of the form that equations are allowed to take in ZK circuits some operations like division can't be expressed in your constraints and so you have to use this single Arrow rather than the Double Arrow and so part of circom is going to require you to express things in either

your computation or in constraints and this is what we're going to be talking about quite a bit because as we have found that this leads to a lot of programming errors where people do not recognize what goes into either side of this problem and that leads to programming bugs because at some point you might have some computation that is not actually going to be checked in your constraints so putting this all together uh I already kind of showed you how this works previously but the computation component is going to encode your computation into a witness and then those are going to be con checked by your constraints and this is why it's important to make sure that there is some sort of equivalence between the computation component and the constraint

component and so the goal is in a lot of cases not all cases but you want to make sure that these two things are equivalent and so I'm going to tell you what equivalence means and that will be an a slide apparently so first let's talk about why we care about this so ZK is still relatively new and so traditionally what I would do is I would show you oh look at all these bugs we don't have a whole lot of that but we still have had a couple of bugs so specifically uh tornado cash had an under constrained circuit in their circuits and they were actually able to find it before anyone else did

but the important thing here is uh had an attacker found it they were able to show that their vaults could have been drained by an attacker very slowly and the important part is because this is ZK no one would have known about it in addition to that there have been a number of other ZK bugs that have been found before they were actually hacked so varadise actually found a bug in a circumlib which corresponds to that first one and then there have been a number of other disclosures that could have caused things like double spins in the past so let me talk about equivalence really quick so I I mentioned that it's very important to make sure that your

computation and constraints are equivalent so let me Define what that means exactly so basically uh I I talked about the witness generator and your constraints previously so your witness generator is basically a program and the reason why that's important is because your witness generator is going to take in some inputs and it's going to Output some values and so that value that's going to Output is essentially the outputs defined by your circuit but also the entire witness that you're generating your constraints then are going to take in both your inputs and your outputs and it's going to return Yes this was verified or no it wasn't basically or yes this is able to be proven or no it's not and so in a lot of cases you're trying to or the the program that you're

encoding is deterministic and so basically what you want to ensure is that because your program is deterministic you want your constraints to be deterministic as well in that your constraints are only going to accept a witness that was generated by your witness generator if it's not that means that there's some behavior that is outside the scope of your program and that would still be accepted by your constraints in a lot of cases this is not intended by the developer of the you know circuit and we'll show some cases where this can lead to some buggy Behavior where someone can manipulate a

witness in order to generate an attack and so we'll be taking a look at that in a little bit but essentially here what I mean by equivalence is we want to ensure that given some program that takes in some input and generates an output the constraints will only accept that input output pair and so that's what this is saying so um yeah one thing that we'll be looking at in or throughout this talk and through the tools that we're going to look at though is how this can be violated and how we can use tools in order to look for these violations because they often occur in you know kind of patterns but also we

can use very formal reasoning in order to identify these cases let's go ahead and first take a look at a taxonomy of bugs so the transitions got screwed up here when exporting this to this laptop but we'll just go past that so we're going to just look at a couple of particular classes of bugs in this talk and so specifically we're going to look at under constrained signals so these are signals with that can accept more than one possible value constraint computation discrepancies so basically that's looking at cases where your witness generator and your constraints differ uh unsafe component usage so in this case we're going to be looking at cases

where someone declares a sub-circuit and they don't use that quite correctly and then finally logical errors and so this is going to correspond to cases where the user doesn't correctly understand like the semantics of the programming language that they're using and they introduce something like field overflows and stuff like that but we'll go through each of these in a little bit more specifics and also I'll show a couple of examples and they're pretty easy I'll ask you guys if you can find the bugs it'll be great um so first let's talk about unconstrained signals so basically an unconstrained signal is going to correspond to one whose constraint is always true and so

what that means is it doesn't have any constraints on it that signal is always going to be satisfied no matter what the value that it's assigned to is so because it's accepting everything this can obviously lead to programming errors if you intend for it to only accept a particular value and so there are certain cases where this occurs so this can occur where you have an output signal that's unconstrained so that means that it doesn't matter the assignment of your input signals your output signal will accept everything or you can have unconstrained public signals where uh you know you take in a public signal but you aren't actually constraining that public signal in any way so we can take a look at an example here and so I've already given you a hint

about you know there's an unconstrained output signal it's a fairly contrived example just to make it easy to look at uh there's also apparently a typo that I didn't see but let's ignore the the Sig a and assume that that actually defined a signal but looking at this can anyone spot the the programming error I'll give you a couple seconds anyone got it it's right here so basically what's happened in this case is uh you're just looping over the structure you have defined that you have

a arrays of size n but you aren't looping over the entire array and so in this case the N minus oneth entry is going to be completely unconstrained because someone didn't Loop over to actually constrain n minus one so this is just a basic programming error where the problem that we have here is this particular output signal is completely unconstrained most likely the user want to constrain it to a plus b but it basically means that out of n minus 1 will accept anything the reason why this can be really bad is because yes so yeah so right so this is constraining

output of n minus 1 equal to a the reason why that's bad is because basically what this should be checking is it should be checking to make sure that um and this is where the the typo ends up coming in I guess technically a is overloaded in this case that should be something like n and so really what this is trying to constrain is that um like out of n minus 1 should be equal to an a of I plus b of I or a of n minus 1 plus b of n minus one uh and that should be equal to n and so really it's just because those constraints are concluded it it doesn't matter you can pass in in

for the output signal but it's not actually correlating that to A and B which should be the intention here because you should have a correlation between a a by and B of I like I said uh I don't know when that error got introduced but uh either way so basically you have a logical error because um out of n minus 1 is unconstrained and so the relationship that you're expecting to hold here might not necessarily hold um yeah so the reason why this is important is because uh values that you expect might

or the relationship that you expect might hold won't and then on top of that if you have an unconstrained value like this through traditional testing you might not catch it because essentially you would have to start manipulating the witness generator in order to actually or the witness to reveal cases where a value is unconstrained okay so now we're going to look at uh some examples where sub-circuits are incorrect and so basically what we found is in a lot of cases sub-circuits often assume that constraints are going to be placed on either the inputs or the outputs but this does not always occur and so this corresponds to cases where

sub-circuits do not follow certain assumptions so if you're familiar with circumlib for example there are assumptions that are placed on certain circuits so for example less than and greater than assume that you've performed num to bits to check that the inputs are of a particular size so it can do the comparison efficiently and so this is going to correspond to cases where those sub-circuits aren't used correctly and so if we look at an example of this this one does not have a bug so apologies for that but uh can anyone spot where the bug might be here I'll give you a couple more seconds

all right does anyone think that they have it all right I'm gonna show it so basically you have a missing constraint and in particular you're performing this comparison this less than comparison but the important thing is um in circom or in similar languages uh it doesn't actually assert anything about whether a is less than b instead it's requiring that the user actually insert a constraint to say that this relationship is going to hold and so essentially What's Happening Here is someone is performing this comparison but they're never asserting that uh a has to be less

or bowel has to be less than amount instead that is completely undefined so it's not actually enforcing the relationship that the user expects and so because of this what happens is given the context of this is called withdrawal essentially an attacker would be able to withdraw more funds than they should be allowed to because it's not actually enforcing this less than comparison anyone have any questions about this okay okay so then um if we move on uh this is probably the most interesting case that we're going

to be looking at in my opinion and so this is going to be looking for cases where you have uh discrepancies between your constraints and your computation and so basically what happens is uh as I talked about previously not all computation can be directly encoded as constraints this is because constraints have to have a particular form and this is enforced by a lot of different ZK dsls and so this is going to correspond to constraints that don't comp correctly encode the computation semantics and so basically what we're going to look at is one particular case called divide by zero and so um

I the title kind of spoils it so what do you guys think is wrong in this case I'll just move on because people are laughing uh basically what happens is you have a division the important thing here is that we all know that you cannot actually divide by zero which means that in your computation there's this implicit constraint that you have that b cannot be zero but because you cannot directly encode division as an actual constraint you have to essentially construct that constraint in a different way so a lot of people construct it like this where you know basically they move the division and end up performing a

multiplication by the other side the thing that people don't end up checking though that we found is they don't often don't check the case where B is not equal to zero now this becomes really important because in a lot of cases they assume that b cannot be zero but this is not checked anywhere in your constraint so someone can manipulate your witness and it essentially causes an unconstrained signal and what I mean by that is if we assign b equal to zero then that means that you know a would also have to be zero but they can set out to any value that they want so in the case where b and a are equal to zero out is completely unconstrained and it can be set to any value that the

attacker desires so depending on how someone is using the circuit this can allow them to essentially manipulate this computation and again performing end-to-end testing would not end up catching this case because when you test you're going to be using this witness generator and this witness generator will never generate that type of witness and so this is why it's important to start looking at other tools that we'll be talking about in a couple of minutes now so the last case that I'm going to talk about is logic errors and so again the bugs that we're going to be looking at here aren't necessarily comprehensive

there are definitely other cases that you're you'll see in other languages and I believe there's another talk about ZK bugs that I think will be more uh comprehensive in the main talk but uh out of you know time constraints we're just going to talk about these so uh basically what I'm going to define a logic error as is a programming error caused by someone misunderstanding the semantics of an operation so whereas you know with computation constraint bugs it's caused by someone not encoding the semantics of a particular operation as constraints directly in this case someone might not understand the actual semantics of an operation no matter

where it is included so if we look at this particular case uh the important thing here is we have a transfer it's basically just going to Define you know it's going to take funds away from one person and give them to another person contrived example but importantly a lot of people who are programming in languages like solidity are now expecting that there's going to be automatic overflow checking or underflow checking in a lot of ZK languages you get none of that and so that means that in this case uh because you're not actually checking the relationship between the balance and the amount you can actually end up having an

overflow right there or an underflow right there and so this can be particularly bad we've seen a lot of cases like this in you know old solidity code where an underflow can give someone an arbitrarily large balance because an attacker takes advantage of this and so here the important thing is this output value can become arbitrarily large and this is actually like all of the bugs that I've talked about so far are bugs that we found during the course of our Audits and they are very common bugs that we found during the course of our audits which is why they're really important and so as I talked about previously end-to-end testing is not going to end up catching a lot of these bugs some of

them can be caught using end-to-end testing but uh when you start looking at things like under constrained values you're going to need to start looking at different methodologies of identifying these bugs and so in order to do that paradise has been working on creating a number of different tools and we're basically going to focus on two of them today namely static analysis and formal verification so first we're going to talk about how you can statically identify some of these bugs using static analysis and we'll talk about how you can actually formally verify that a circuit is constrained and how to actually make that scalable so I'm going to hand it over to Daniel

who's going to be talking about static analysis okay so before I move on to aesthetic analysis any questions so far about circum General um okay so um since John already gave a really nice introduction to circum I had like um that is like here this motivating example um I like explain a little bit the the com like the components of silicon but you already know that so the idea here of this algorithm is we take two inputs that are supposed to be bits um we just have them uh um speed solution we had calories for inputs and outputs usually stuff and

we make sure that the outputs are going to be Boolean with these constraints here uh because if you do the math for this for any other value that is not a serial one that will not pass so that's how you make sure and but here there is also a problem it is um since the um we're using the single Arrow and we are only checking if the the outputs are bits we are not constraining much more than that so the inputs are not constrained and also as you will see on the on the examples when I show you the tool the the output cells are also considered

not constrained because they don't they do not depend on the on the inputs so um a little bit of what is static analysis we take a source code right now only supports circum but the idea is we have a bunch of detectors we call them it's just checking for some patterns or structures of the code or heuristics in general one is the constraint output I just mentioned but we have a bunch more I will talk about about a few of them and then we just get a report saying like hey we detected this common Pitfall that you may fail into and static analysis for those that don't really know what's going on here we get the witness that previously we

defined as p and then we get the inputs so we kind of plot this map of inputs and outputs that's all programs no so we can just go sequentially and try in every X and we get every P of X and then we get the results and we know if they are good or bad but that's really expensive or something some impossible directly so we try to transfer the program into a structure that we can understand and the most common and classic technique was to take the the program transform into a set of equations and we just solve them something similar to what we do with l1cs um once we get the results for the equation we just check if the values make sense or not and they are an issue or not

uh other techniques take for example if we have an addition of integers that could be zero it could be a positive integer or just a negative integer so we transform all those values into minus zero and plus and then we Define this special sum operation well multiplication will be easier to think about like this multiplication where minus times plus is minus because Tesco multiplication works so we don't really know what number is but we know it's a negative number for example and then in other cases we just take the shape of the program and we transform it to another one this is our tradition about and this is what we do with Vanguard because in the particular case of circum

and other Sikh languages you don't only have P which is what you have in traditional programs you also have the constraints so we need to mix everything together so we can reasonable both of them at the same time so the main problem with aesthetic analysis and that's why in the slide before we said it has false positive this we paint like a very broad picture of what the problem is doing so we'll be missing cases which will be false negatives because we are not seeing those and since we have this very big circle we may say that something here is actually true when it's not because it's not one of the dots I painted before right so

that's an inherent limitation of static analysis because we are abstracting so far away we lose the the details but it's okay so three dot that we are willing to do so how we understand the programs in in Vanguard we have the inputs um that should be yeah the inputs and the outputs the outputs are slightly darker colored and then we Define the assignments the single Arrow as these thick lines so we say that I write something in O we don't really care and then the constraint is defined with the dotted Arrow so I constraints on how all related in a constraint so we built a graph

of all the inputs and outputs and then we can detect some things following patterns it has graph so call me back to the to the example we have the three inputs and the two outputs so we just paint those then they were supposed to be animations but we lost those okay so we have the single arrows that take as inputs the three signals on big rights to each one of those outputs so we get that bipartite graph and then the constraints since they are only related learn cells we just paint those Arrow step so we've said before okay the inputs and the outputs are not constrained between

the cells as we said before but here is like very clear to see because there are no relationships between the inputs and the outputs using the the dotted lines right so we can see here very easily that this signals the input signals are in constrained because there are no dotted lines pointed to outputs and vice versa okay and therefore so okay so the with this circuit and since this is some constraint we can have this assignment for example this witness where we try to

sum one plus zero is equal to one good enough but since we are only checking if the okay they'll put some bits we can do this where we only change the carry output to be a one so we are trying to claim that we somehow did one plus Z equals three and the constraint system will say okay because that they're checking that their bits but the math doesn't really add up so why not just use the Double Arrow we already talked a little bit about this in this case well for the curry we have an addition here that's easy transport

but this is a model operation so you know it's also an addition but we just take the reminder so the constraints need to be quadratic and the compiler actually that that's all this so you can see like okay a little bit Arrow it's not allowed so you cannot compile this um like you already said then you need to create things with this structure which lead to parameters that I made while making the slides I actually made this one by mistake this was not on purpose and it was quite funny to to notice so um yeah science because of the limitations of circum we tend to make these mistakes so more patterns that we

can detect in the case of all cost rate outputs we just check the opposite relationship are there outputs not connected by a dotted line to the inputs um control input I just said and what they call a data flow constraint discrepancy this comes from the fact that we consider the thick lines of data flows data flows from the input to that particular output and there is like they not do not match between the adult lines and the but otherwise a little bit Rusty so they just have discrepancy between the dotted lines and the thick lines that's what they wanted to say so let's take a look at some examples at

the shape of the graph and let's see if we can see the pattern who can we detect all this so let's look at the example we already knew of less than and we are missing the the constraint to the output so we start working on this and we take the inputs then we have the two component so we are going to Define it with that I created the boxes to clarify what signals belong to what component but in the end it's just like the same graph next to her we have since this is both a thick and a DOT line and internally we know they have the attached shape so

how we detect in this using this graph thinking like the algorithm in Vanguard how we will detect that we are using this component in a wrong way Okay so the idea will be we know that two component has an output but nowhere in the graph that will put this constraint to Something in the main circuit so we are missing that chunk there to some probably we are signal that should be constraining so if we are missing the tank we consider that we are not using the the two component

clear so far now this will be what we call a we have here X2 is odd or even then we assign 0 1 and we use that zero one as the index for X1 so depending on the value of X2 we will use either signal so that's not deterministic and we I got away with that because I use a single Arrow so Circle will not complain about that and then I just constrained that forgot measure

so we get that graph and then again my question is okay how can we build an algorithm orthograph that detects that issue um here are the obviously we can't because following the rules we had so far there is no way to know next two is just there chilling doesn't really connect to anything so we just create a forgot about the label we create a new node which represents a conditional operation like the usual um diamond symbol and okay with those rules now the detection is is obvious right we just check if there if any signal points to the conditional part of the fun

statement and if so then we have that um this one in particular is not a bug but it's considered a smell because it could lead to problems it's not a problem on its own and I mean this is a very weird example like she don't really do this in real life but sometimes you do something that counts us and you know detecting it early is super easy and you know based off so let's go back to the division by zero easier stuff again right we just know that X2 should be is problematic because it's there so we then again have the graph and then again we encounter the same issue we

don't have enough information there right so here I have a really nice animation but um with everything move and was clear but okay whatever so we create a new note that represents separation and then again easy stuff right like who will detect here we use have a note there connected to a division operation this is simplified that usually has to be the the dividend the division departure denominator I mean I learned math in Spanish not in English don't really translate well but yeah that part of their division the

one on the on the right so okay easy stuff but with just that pattern if we actually check if the if the value is zero are we gonna still complain or not so consider this example now now we have this component that sector this is zero this is from Circle Leaf so standard stuff we just check and we make sure that X2 is zero otherwise still this prong will crash the witness now will not complete so we create this graph so far so good no okay so uh animation missing there's some how is this case vulnerable is this an issue no right

okay uh so we will follow the previous algorithm what will the algorithm say is this vulnerable yes because it's just checking if there exists a Nets between an input signal and the denominator of a division so if we don't consider the value of X2 following this we will have the the report which is a false positive because this is actually not vulnerable which is kind of the main limitation of static analysis like depending on how you abstract on how you represent things you may run into problems and detections

that do not make sense or you may missing cases so if we wanted to make this right we'll need to consider the value of the output of this is zero and make sure that you know all the values that are available is the ones that make this true which will be zero and then we follow the same procedure in the internal surface zero when we think we will conclude that this needs to be zero in order for this to be true so we can rule out zero uh no sorry deposit if this is zero then X2 cannot be zero always mix the two so we can roll out from the set of

possible values that X2 is going to be zero so then we check if the value cannot be zero then that division is safe but then we already introduced another static analysis technique so we are mixing things together we need to improve and make it more complicated so yeah it really depends on what you do you may have false positives and no technique is perfect as far as I know there are no silver bullets on the static analysis so that's why we also make other stuff to help to with this more complicated cases which now help will explain about absolutely thank you very much so I'll just talk a

bit about how to use uh formal methods basically and smt solvers for the in the detection of bugs and ZK circuits and today I'll just concentrate on under constrained circuits but of course by modifying things you can also apply the same kind of reasoning for detecting other kind of bugs so I mean John talked a bit about what our what under constrained circuits are so if you have a ZK application you you just usually have like a computation part where you have input X giving you an output y that would be kind of your witness generation and on the other hand you have the set of constraints and you want that the set of constraints really captures the

computation so you want to have the sequence between the two yeah and the set of constraints will be in general given by some polynomial equation and your circuit will be unconstrained if I mean in general if f of x is equal to Y then you want that the constraint should be satisfied but if you have also so if there exists X and Y such that f of x is not equal to Y so this doesn't correspond to input output but still the constraint is satisfied that would be kind of a problematic case showing that your constraints do not really capture the computation that you want to create the proof about right so this equivalence will be important so basically you want that f of x is equal

to Y if and only if X and Y really satisfy all the constraints right and but then practice this doesn't happen always and that's a source of a bug and um and the aim is to kind of discover or to to reveal those and we I mean um Daniel talked about static analysis where you apply some predefined rules to quickly detect whether these circuits are properly constrained I'll talk about how to use smt reasoning to do that so basically what you do is you express this underground strainless property just as a formula in first order logic yeah so you just uh you say the circuit

is under constrained if there exists X and outputs y1 and Y2 such that y1 is different from Y2 but both the pair X Y 1 satisfy the circuits and X Y 2 satisfy the circuit right I mean f of x can be only y1 or Y2 if it's a deterministic computation so if you have two separate outputs that could really satisfy the circuit for the same input then you there's a high chance that there's something fishy there yeah so you basically you have this logical formula and you want to see whether this can be satisfied yeah so if this is satisfiable then you are kind of uh you should be watching out that because that is high a

high probability that there's something wrong there and the moment you talk about satisfied ability of course you think of this sat solver set solvers but these were I mean uh quite uh they're very useful but they're more for Boolean satisfiability problem yeah so you just have propositional logic and you have like uh some formula and then you want to see whether there is some interpretation so if there's some assignment of truth values to your variables such that it evaluates the true at the end right but in our case um our problem is a bit more complicated because we have like a multiplication of elements we have field elements finite field elements we have variables and so

on yeah so it's not just a simple Boolean satisfiability problem so this is what one uh usually uh studies Under the Umbrella of satisfiability modulo theories which basically generalize at this sat to more complex formulas yeah so you include an additional Theory so this Theory could be depending on what you are doing it could be the theory of integers of real numbers in most cases for us it will be the theory of finite Fields but you can have lists arrays and many other structures yeah so and what the smt solver does is it takes a first order logic formula over a given background Theory T so you have this theory of let's say integers together

with all the axioms of the integers and some statements some logical expression that expresses something about the integers right and what the smt solver does is it should either say this is not satisfiable or it will conclude that it is satisfiable and possibly give you a model it should give you a satisfying assignment in the end right and just to give you a flavor of what kind of theories one could look at one could look at for instance just the theory of integers where you only include addition so this would be just the linear inter arithmetics or press Burger arithmetic and this is a complete and decidable theory and so you have algorithms that can kind of Reason about this but you it

is not too expressive because you cannot talk about divisibility prime numbers or non-linear equations and so on and as you all probably know if you include also multiplication so if you go to a non-linear integer arithmetic the usual piano arithmetic then you get the incomplete and undecidable Theory or maybe just to give you an example that's more visual easy to visualize if you work over the real numbers if you just have linear real arithmetic then you would be kind of reasoning with methods like the Simplex method and so on or if you include nonlinear real arithmetic which is kind of a very interestingly decidable by itself so you can really find algorithms to solve whether a

formula in this theory is satisfiable or not using quantifier elimination and I mean the steering goes all the way back to tarsky and currently the fastest algorithms are like the cad algorithms to deal with them and of course the list of theories that you could be looking at there are plenty of them these are just the list of theories that I use that you can use in this solver cvc5 yeah uh so I'll just go a bit quick so just to give an example for instance over the reels you could have such a system that you want to be satisfied right you're looking for real numbers accent why such that those three conditions are satisfied you would how do you feed it

into a smt solver it just has a certain syntax you feed it in and you run it since it is decidable if you're lucky in a finite amount of time you will just get a result which says yes it is satisfiable and this is a model yeah so and that would correspond to kind of you're looking for a point inside the circle on the blue curves such that the X and the y coordinate are distinct and then this one minus two and comma oops there's a mistake there's yeah minus two comma minus one over two will be a satisfying assignment and the nice thing about quantifier elimination is it's so powerful that you can even give a formula that has quantifiers Senate

right you can give a formula saying there exists an X such that x squared is equal to a and you're looking for an a that satisfies this yeah so the only free variable here is a can I find a satisfying assignment means can I find an a such that there exists an X such that x squared is equal to a so if you run the quantifier elimination it will just eliminate your quantifier and it will reduce it to a formula which is quantifier free it will say that a should be either equal to zero or a should be less than or equal to zero and you can play around that's a lot of fun you can look at degree two polynomial equations right and you can ask oh I want to have ABC such that there exists

an X such that this equation holds so you're asking when does a degree 2 polynomial has a root and then you eliminate the quantifier and it reduces to an equation I mean if you see what this means it just says okay the discriminant should be non-negative basically what we know from High School yeah so it's a very power powerful tool just to show you how nice smt solvers are for us it will be more interesting to look at the theory of finite Fields not that the theory of real numbers because our constraints in the end will be just equations over the over a finite field polynomial equations so there is a public Fork of the cvc5 solver developed by

canalient Barrett Barrett which kind of includes this theory of finite fields in it and it's basically based on grubner basis implemented in a computer algebra system called cocoa and that that can really try to use you can use that smt solver to do like some kind of more formal verification so there were two strategies as I mentioned their static analysis that Daniel talked about which is scalable but has many false positives and then we have this method also employing smt solvers which is more precise but it does not scale and the

reason why it does not scale is basically if you trace where the bottleneck is it's at the end you have to kind of solve polynomial equations over finite fields which reduces to some grubner basis computation or solving polynomial equations which are which is an inherently difficult problem yeah and uh at uh at Veritas we have developed a tool called picus which kind of tries to combine the nice things of those two worlds I'll just go very quickly over it it just takes in this polynomial equations and it tries to reason it wants to it tries to determine whether the output is uniquely determined right so if it can if the output is unique you just get the

positive result saying yes uh the the circuit is properly constrained or if sometimes you can prove that it is not properly constrained and there are cases where you cannot really get a response and the reason why you cannot get the response is at times out basically yeah uh but you do combine the kind of strengths of static analysis and smt solvers which is on one hand it is fast but imprecise just uh I mean like the same the static analysis is fast but imprecise and smt solvers are precise but slow and this way you manage to get something that is both fast and precise in some sense yeah and how this works uh is basically I want to go into the

details but it's it's kind of an interactive Loop between two engines one doing the static analysis phase and one doing the smt phase and both can get stuck and then they feed each other they pass information from one to the other and whenever one gets stuck it passes it on to the other and through this communication in the end You can conclude in most cases that something is under under constrained which without having this engagement between the two would not have been possible but eventually I mean you get quite some speed up but eventually this is also reaching its limits because the smt solver in the end does you take

weight off from the smt solver but still it has to do some heavy computation and the reason is that the scrubner basis computations is in fact a doubly exponential problem yeah so that's the main bottleneck and then the problem is okay what to do with it yeah so one thing you could do is you could say okay I'll wait until people working on come to algebra or computer algebra systems improve their methods for solving polynomial equations but if you take into account that that field has been around for several decades it's not gonna there won't be a major breakthrough most likely in the next few years right but what you can do is you can exploit the fact that the system of polynomial

equations that you would be working with uh in the K applications have a very particular form yeah so they're all quadratic equations they are very sparse by definition and so on so I mean you can try to use that structure and exploit it to really speed up things and the idea to kind of exploit the structure to understand the structure of those polynomial system is to just attach to the polynomial system of equations a graph so it's a graph where for each variable that appears in your system you have a vertex and you draw an edge between two vertices exactly when they appear in an equation together now uh so for instance for a circuit like

for the FP multiply circuit you get a graph that looks like this right that looks quite complicated so it has 377 variables and 392 equations if you forget about multiple edges it looks a bit better so I mean here already you see that there are some clusters of variable that communicate a lot with each other right but the variable here would not really care too much about the value of a variable maybe in the other cluster yeah so they only speak to each other through these uh edges over here right so kind of you try to divide your problem into smaller problems using this graph theoretic approach another thing that you can get out of it is I mean this connectivity is an important point

right I mean variables here they would kind of with the central component only talk over this Edge over here and then you might want their own what are those weird working arms let me try to understand the structure of my constraints by understanding what those arms correspond to right and when you do that you see basically that what those arms correspond to they just correspond to certain bit sums right so if you take one of those arms you will have one vertex where it connects to the main body right that would correspond to one variable and then you'll have several other variables and then if you look at the corresponding equations that form

this arm you will see that it just corresponds to saying X has a binary expansion so I can write it as a sum of bits right by multiplying with consecutive powers of 2 and each of these be zero up to B K are bits right so what a whole arm like this would be saying is that this variable corresponding to the part where uh kind of the arm connects to the body is constraint to a certain interval right so if you want to express this range analysis uh using polynomial equations this is how it would look like yeah but then the problem is

this does not translate well into algebra now if you would convert this problem even if you have a small uh like if you have just 14 bits a very small number if you want to con translate this into uh into algebra into a polynomial equation what you would be doing is basically you would use grobner basis to eliminate those bits over there and see which equation the X itself has to satisfy right because that's what you care about in the end so the whole arm is just there to express what you know about the X and then if you take such an range constraint if you translate it into algebra it would just say that X can take a value between 0 and 16

383 but then this corresponds to polynomial which has a very high degree and if you look at the coefficients they have they are huge right I mean they're coefficients that are I mean the constant coefficient is just the product of all numbers up to 16383. so it's kind of a 61 000 almost 62 000 digit number yeah and that's why uh the smt solver really crashes and countries so but then you cannot also forget about these kind of constraints because they are very present uh in many of the circuits and they form the bottleneck that makes the algebra and the polynomial arithmetic so difficult

and uh and coming from this graph you can then try to get rid of those arms so you exploit the graph structure you see how things are connected to each other you can simplify those arms and you can kind of incorporate you can use different methods to kind of separately look at the range analysis without feeding it into basis engine which will really would have to deal with this huge polynomials where it will get stuck and then using this hybrid method pikas which incorporates uh static analysis and these improvements on the solver you can solve many more cases that were previously uh Out Of Reach yeah so I want

unfortunately I don't have too much time to go further into the details but if you're interested I'm very happy to talk about it offline [Music] I'm sorry like does the evaluation run in linear time for the evaluation of snarks work on like Reed Solomon encodings yeah usually the evaluation of that is n log n does this do any better no this I mean this will be I mean like

you will have a circuit which will turn into a polynomial equation and then you will from that polynomial equations you will create a new system which will correspond to encoding the fact whether um things are uniquely determined or not and then you will have to check whether data is satisfiable or not and that's kind of a very non-linear problem which is very hard to tackle in general basically they're solving two different issues so you're talking about is the actual internals and the proving system whereas this is trying to find those and so the complexity is just significantly higher here we still have an undecidable problem rather than something that could

run and uh yes uh yeah thanks for the talk I was wondering if you tried specifically for cbc5 with finite field ethereum core to and for the range constraints to take them out and express them as Boolean formulas over the finite field so because CBC 5 loves that and yeah yeah I mean when I said you use a separate range analysis we did we tried that and we even tried uh using the in integer solver to do that and that's how

you really get the speed up like you have to free the solver from all range constraints expressed in polynomial form and just as you say using it expressing them as Boolean constraint is one way and then you have like different approaches like always this dpln based methods where you kind of and you combine the different theories and that's kind of how you get the Improvement exactly okay what was the Improvement like in concrete terms so I mean um I mean since this is still a work in progress we I I did not really put a table with saying okay this was the timing before this is afterwards and there's always this problem when you

create benchmarks are they representative or not but what we did is we took a lot of benchmarks as benchmarks lots of circuits that kind of uh we encountered during Audits and we fed them first into pikas which was just using a smt solver that has finite field support together with static analysis and it resolved many cases but then they were like among those benchmarks they were like some around 30 of them which it could not handle and then with these additional approach you could out of those 30 that were Out Of Reach before you could maybe resolve half of them or two-thirds of them and resolve means you get an answer within uh five seconds or

so okay uh yeah just one last question what did you do about circuits such as hash functions because for example yeah when we tried to put the whole circuit it just crashes memory is not enough did you separate it into much smaller chunks that's a good point very good point I mean for hash functions um what you do have to do is you have to I mean they are very modular you'll have different parts that kind of uh feed each other right and if you look at them all at once that will cause a problem because it will be too huge of a circuit to deal with but like you have different parts that fit each other and to to conclude that everything is deterministic you could just check that

each of the components is deterministic right I mean if you have deterministic input at each step then the final output will also be deterministic and once you do that modular uh approach where you chop it up into smaller pieces you could also handle lots of those hash function computation circuits that check cash function computations but their modularity was really a key Point as you say yeah yeah thank you for the time static analysis stuff how like one size fits all is it so are you kind of just adding to the list of those patterns that you talked about or for a specific thing you're going to run it on are you also kind of taking into account

television so basically we've got a bunch of generic patterns so you don't have to take into account the structure of the actual code base because we have like Daniel the show we have a method of encoding that into a more easily understandable form which was this graph and so for that reason it doesn't matter what the shape that graph is which is what you'll end up getting from the code base itself instead each of the patterns that we have is generic and it can conceptually work over any graph that's provided to it I guess what even more is like the e0 example that you guys gave like the specific kind of uh pieces that like that that are specific to a

specific on there that are specific to a single you know use case looking at does are you having to do a lot of kind of I guess hybrid approach of human and and static analysis yes analysis you're going to get a lot of fault or I mean we try to trim down the number of false positives so the life of Daniel was showing if you have you have kind of a naive method of expressing this divide by zero you're going to get a lot of false positives because we'll just identify every Division and so at that point it's a matter of refining uh your method partner detection in order to get more and more precise results but when you talk about having like a human in the

loop typically the way that works is uh the static intellectual and unfortunately we didn't have time but we have a lot of videos that show like how this will work in practice and show you what the results look like where it would essentially give you a list of things that will detect it and then it's up to the human to go and look through them and say this is a false positive this is a true positive and stuff like that so the static analyzer itself isn't going to have that humans necessarily but the human doesn't need to go and check and see whether something reported was positive or not and then you know we're obviously working on reducing the number of false positives as much as we can and now the way you grow from that it's not so much looking at the structure of the particular pose but

adding more information about like they called as a concept like with your if you only look at the graph then you have positions but if we look at the values same time they could decide if an X is a problem so we need some more information I just wanted to check my understanding are you going from the r1cs constraint to the satisfiability or are you going from the arithmetic circuit to satisfy build um I mean it doesn't matter too much in fact because this will be quite like agnostic to how we express things I mean in the end you want to express everything in terms of polynomial equations so you

could do that from r1cs directly or even if it comes from another air you would still be able to do that I mean this is kind of the work on the solver side is just to say I have a polynomial equation that comes from a ZK application which will have a very particular structure and how would I resolve it but I mean you start already at the polynomial equations so in practice we started with r1cs it doesn't matter if like Alp was saying if you start performance CS long or like a pump table or if you start with the actual action itself as long as you are able to perform that encoding everything will be fine

um so we focus on the actual intermediate representation for this particular work like r1cs like the the pumpish tables because I'm imagining going from the arithmetic circuit to set would be a lot easier the reduction is like straightforward so I'm wondering if if you do that you go if you will save yourself a lot of maybe challenges that you face when you go from something so unsatisfiability like like all CS equations if you go from the arithmetic circuit directly to the set solver

I'm just wondering if that would make things easier uh in terms of like the some of the challenges that you that you mentioning you see not really just because well in a lot of cases there are restrictions on how you can Express constraints in your aerodynamic circuit anyway and so it doesn't really buy you a whole lot in order to go from there to um actual smt and some languages that are coming up now you might get some improvement where someone can express their computation more naturally because they don't actually separate the computation from the constraints so those could be your languages like um let me say artworks is a very good example of that where it kind of has this uh relationship where it knows how

to translate any arbitrary computation as long as within a certain forms and constraints and so you can possibly get uh better results by going from there to your actual encoding but in a lot of the languages that we've seen going from your arithmetic circuit to your constraints does not provide a whole lot of benefit just because they're so simple um yeah well because this uh all this AKA proves they are mainly based on this

constrained systems but I I'm I wonder if these approaches can also be used for some other Frameworks for for example a multi-party computation Frameworks because I imagine that this uh for example the divide by zero or underflow or overflow this this errors might be quite common and I wonder if we can apply these techniques to a multi-party computation which is slightly different because we don't have those all those constraints so it's the representation in the polynomial form is different but yeah yeah so multi-party computation is something that we want to get to at some point okay yes essentially multi-party competition so uh that's something that is kind of

on our roadmap to start exploring and develop some similar tools and techniques which I imagine will look fairly similar to what we have here or somewhat similar like if you look at them from you know with kind of far back then they will probably look fairly similar yeah yeah okay cool foreign [Music] hey thanks for the talk um do you plan

on providing support for other languages as well yeah so we're working on support for other languages so sarcom was our first one just because you know I think it was so simple the circle because the DSL is the example uh we're working on adding support for hal2 artworks uh funky to images like that as well there are other languages that we might be able to support as well that you know basically take away the effort of expressing the constraints like let's say a1js but most likely because the back end is going to deal with encoding things as constraints tool synthesis are not going to be that's necessary and so we are working on uh expanding the set and in some cases it's easy like with

the s t approach that we were talking about now it's just a matter of encoding your table as constraints which is not very difficult for other techniques such as the one that that Daniel was talking about the staff analysis we have to kind of understand the both the constraints and the computation we can get more difficult to understand in some dsls because like if you're talking about Halo 2 you have to understand the arbitrary request which gets fairly difficult and so instead for languages like that you kind of have to let go of the computation side of things which is unfortunate because it means that there are some things that you can't detect and instead of focus primary constraints so we're working on

those trade-offs for other languages as well awareness nor fall into this right uh Noir is something that that we haven't spent a whole lot of time looking at at this point we you know basically the way that we've decided Which languages to support are based off of where we think in the Audits and so we imagine that we will also start looking into other Frameworks like Noir particularly because uh it's got a very nice representation that a lot of things can count down to but we haven't started looking at you anymore yet thank you okay okay thank you

[Applause]