Formal Verification for ZK Circuits Using Symbolic Compilation, Applied ZK - Day 2

[Music] right um hello everyone thanks for the introductions my name is yufeng i'm a co-founder of veridise a new startup for blockchain security i'm also a cs professor at ucsb in which i run a lab for doing verifications for for security and so today i'm going to present our ongoing work for applying phone verification for zika circuit and this is also a drawing where with my student yanji who does most of the heavy lifting stuff unfortunately he cannot be here because of visa issue um so so before we get started so what's form verification for those of you who don't have much backgrounds on form verifications so essentially the goal of phone verification is essentially to create construct rigorous mathematical proof that a given applications behave as intended right so your given application can be your defined smart contract can be a zk circuit so which means that so when we say for verification essentially take two inputs first the source code of your program as well as a formal specification which essentially encode what's the intended behavior of your desired target and then so when you run form verifications over your program and spec so it's going to generate two kind of a different outcome either it's generally a mathematical proof in this case it's certified your program it's correct with respect to the spec you provide or it generate a county example showing that um the edge case that you didn't satisfy okay and so just like when you are doing mathematical proof um in your elementary school sometimes you cannot make the proof per se and then you might get help from from your teacher so in this case occasionally so for firm verification too you might also get like actual human expert inputs for some domain knowledge that you don't uh it is not accessible by your formal verification tool so you might wonder why this matter right why do people care about phone location because it's provide the highest level of assurance over the behavior of your software artifact compared to ad hoc approach such as testing and or manual auditing right in the sense that it actually ensure all the edge cases are considered using rigorous mathematical proof and so why this matter because for instance all of you uh probably know the reason hacked uh from from being stacked and for instance even though like all those kind of defy applications they they feed a huge amount of money to those audience companies they're still getting hacked like every month so and the reason is that existing auditing process they actually fail to reason about all possible behavior of your artifacts so now we come to formal applications uh for zk circuit in this case we use like a zk circuit in terms of r1cs as an example but the idea can generalize to basically leakage circuits in arbitrary intermediate representations that you might be familiar with so in here i'm going to reuse the example that you see from you saw from ignis example in a sense that you have a circuit on the left side which is essentially a set of polynomial equations okay so in this case um so so you just need to um understand that there is a couple input uh x1 x2 x3 as well as some intermediate uh what we call weakness a variable i1 i2 i3 and and then the circuit essentially is going to produce an output y okay in this case i want to verify this circuit what do you mean by you verify the circuit right so in this case um what you want to verify is that uh first it is correct with respect to certain spec okay in this case let's assuming that we use the the original silicon program to represent the spec of the desired behavior of your circuit uh in r1cs which is essentially on the left-hand side okay so when we say we formal verify a circuit in this case we concerned about two properties the first property is about equivalence so the equivalent thing is that for those of you who might not familiar with first order logic is that this is essentially universal quantifier what you quantify is that for all possible space of your input you want to assert that um the program on the left hand side as well as a program on the right hand side they should always return the same result okay no exceptions and then so that's equivalence property then the second property you also concern this is the essential uniqueness property that can be handled by ignis in a sense that right now i'm i'm concerned whether my programs my circuit on the right hand side can potentially violate the notions of uniqueness what do we mean in the sense in this case so you're going to use a query with existential quantifier in the sense that well can you actually give me um two different kind of like witness variable such that it satisfy your polynomial equations but um they actually different with each other right in this case you make a query to the solver and if the server returns yes which means that your circuit are potentially bugging because it violates uniques so once we um agree on the problem definition about what to verify and then the next step is to how do we even build the verifier right so in this case uh it turned out so to be um in order to verify your program essentially all you need to do is send to convert your program into its corresponding mathematical representation in this case your mathematical representation is going to be a logical formula and how do we do that here comes the design of our system called pickers okay in this case the system is going to take two inputs the first input on the left top left is essentially correspond to the circuit to be verified well in this case um we use r1cs circuit as an example but you can use essentially the system can be generalized across object representation for instance you can replace r1cs with relax r1cs or some reason representation it doesn't matter okay so this is a circuit you want to verify as well as a specification that you want to enforce that knows to denote the correctness of your circuit so in this case i'm just using its corresponding circum program as the reference implementation but you don't have to for instance you can use a program in leo or you can use like arbitrary like high-level programming languages to to notate the reference behavior of your desired circuit okay and then so once we have those two inputs so essentially the core idea the call the call of the verifier is essentially just to interpreter okay so what those two interpreter does is essentially it's going to be interpreter for the corresponding uh target language that you want to verify in this case we have an interpreter for r1cs program we also have interpreter for circle so interpreter is nothing special other than the the homework assignment you might down in your compiler class in a sense that if you fit your fit interpreter with a concrete input as well together with circuit it's going to interpret your program and then generate the concrete output so what's more interesting is that once you you fit the verifier with your program with a symbolic uh input in this case this x corresponds to the input and then you want to reason about the behavior of all possible x okay not just one certain x so in this case we actually our verify actually leverage rosette um so the the solver aided programming language to lift executions of your interpreter into its corresponding uh formula okay so we do the same thing for the second program which essentially turned into a mathematical formula which can be reason about using of the of the shell server okay so in this case the output of the system is going to be either correctness proof to certify that your program is correct or it's going to generate a counter example to demonstrate that um such that those two programs actually behave differently okay so here i want to mention that the design of the framework it's actually highly customizable in the sense that um the quiet the core implementation is just two interpreter for for r1cs and circon and then you can essentially replace your interpreter with arbitrary intermediate reputation or programming languages and it turned out that so when we build the the framework and majority of the effort is actually spending on like because of the poor um documentation in silicon uh certain programming languages and so and at the end we actually facefully uh follow the semantic of r1cs and circle semantic which actually leads to both good news and bad news the good news is that this is actually close to some sort like a real usage prototype in which you can apply to your circuit and then the bad news is that uh it leads to some challenges and those challenges are actually not quite surprising uh to existing solver because as you can see the circuit we're trying to verify most of them are essentially non-linear operation right so basically polynomial equations are just everywhere which is essentially very very bad for existing smd solver so in this case what do we do shall we give up or just like develop a specialized uh polynomial solver okay so the second challenge is that so there's a lot of arithmetic operations over large prime number as you've seen from uh brian's previous presentations and the last one is essentially like scalability issues in a sense that how do you even verify like a circuit from this project with like several millions of constraints right so in this case um i just um i'm going to briefly uh illustrate our ongoing effort about the first two and uh so i'm going to elaborate the last one with our future work so for the first one so because like non-linear operations are everywhere which is very very bad for existing constraint solver so what we do is that but we still want to still want to leverage smd solver so what what we do is that we are going to model those expensive nonlinear operations as an uninterpreted functions so what do we mean by interpret an interpret function in the sense that i don't care whether it is modifications or mod operations i just treat it as a regular function okay so which means in this case let's take a look at this example probably the font size a little bit small so in this case i have two functions from one and found two and obviously those two functions are equivalent so essentially you just square the the parameter okay where the first one essentially do some like intermediate uh movement about those data so in this case i want to prove the equivalence of those two functions so what what you do essentially you just traverse every single statement of your program and then you translate into its corresponding formula translate into its corresponding formula and then at the end so you want to assert that where those two programs are equivalent right which is essentially equivalent to asking of whether there exists um an input such that those two uh return different value and then it turns out that even with those simple like verification tasks if you just naively feature the smg solver it takes over five minutes to um to terminate and then one of the reason is that so the server has to actually concretely reason about the behavior of these modifications and it has to exhaustively search the space of all possible solutions to give you the answer whereas if you treat these functions as an interpret at the bottom in a sense it's just a function which means that what does function do in the sense if you just give me the same argument i'm always going to return the same result that's it and it turned out that if you model as an interpreter function it can give you uh return the answer in a fraction of seconds however there's no free lunch when you like do this kind of a interpret functions model uh non-linear operations there's going to be a trade-off in a sense that you might generate false positive okay and then so i'm going to uh elaborate like the trick that we are going to do to illustrate this uh problem so now i'm going to talk about the second trick that we deal with uh challenge two in the sense that there is dr like essentially a arithmetic operation over large prime over everywhere for instance this is the documentation from sircom programming languages in a sense that for every binary operations if you always apply a mod operations over the operands over a large prime number okay so which means that internally so the circum compiler is actually maintain some variance or rewrite rule like the following which is not accessible by the smd solver that's why it has a very very hard time to reasonable that's why it has to try all possible like computations to see whether there's a counter example in this case what we do is actually pretty simple in a sense that you can think of we design a theory of prime in a sense that we encode this kind of rewrite rule as actual axioms to fit to the smd solver to feed the smg and then let smd solver to aware about those kind of equivalence of those rewrite such that it can actually uh reduce those kind of complex prime operation into its simpler form okay and does that even work so what we do is that we actually evaluate uh those um our two on on the same benchmark from igni which contain uh most of them from a circumlib and we use a timer of two minutes you might wonder so why do you use two minutes so if you can verify a large circuits i'm happy to wait several hours or several days right and the reason is that because um so we uh we are actually working on this uh actually at the last minute um so just to get rid of actually like a 10 minutes before my talk like yenji was still making push so that's why you can think of what we what i'm going to present you can think of it's the lower bound it's essentially lower bound of the verifier and then in this example since you already see the result from franklin's presentations uh i'm going to only focus on equivalence checking and then so but our two do provide like a building support for uniqueness it's essentially just a different query you're going to send to smt solver so the result is not as shiny that you can you can like present in a let's say top tier email conference but it's still like show some uh encourage like uh um like information in the sense that among those data sets um so even with two minutes of timeout we can already prove like 32 of the circuit and so and you might wonder what's going on with the rest of the of the benchmark that you cannot prove right it turns out that there are multiple reasons the first reason is of course scalabilities like for instance what happens if your circuit has millions of constraints right and then the second uh limitation the second reason that we cannot prove is because of earlier i made this kind of assumption in the center for all non-new functions i'm just treating as i interpreted so which means that for some circuit they are obviously correct and equivalent because of those like over approximations so it's essentially you fail to like verify and then you generate false positive okay so now i'm going to talk about briefly illustrate some um ongoing uh future work um that is essentially driven by the the limitations okay so it's essentially um so the first one is about the specification language for zk okay and then the second one is like how do we design scalable yet precise algorithm to verify like larger circuit and the last one is uh the third one is about modulation for large circuit and finally uh what we want to do is how can we go beyond r1cs and circum let's say for those programs written in prong okay so for the first one so one thing we um we realized that it's very urgent it's essentially we need a separate and then language agnostic specification languages to specify what kind of property do you want to verify for instance previously uh in our current implementation we are using the reference implementation from circle circum program and which means that we are assuming that the behavior of the silicon program is correct which is not for instance in this case uh this is actually a bug report by tornado cache team in the sense that for this second library so the developer actually instead of uh originally it was supposed to use let's equal equal it use equal so which means that in this case if you use this program as your reference spec then you're going to like generate bogus result okay so and that's the first um direction that was mentioned and then the second um direction which essentially how do we um like apply like a more scalable algorithm for circumvent for circuit verification uh especially to deal with this kind of non-linear functions so as you probably remember so when we want to reason about the program i made some over approximations which is like imprecise but in my works however so let's say right now i want to perform verification right so i want to verify let's say um brian and yi they are equivalent in the sense that they are the same person so which means that one i.e what you can do is that you formalize brian as a mathematical representation right which is impossible so even you can formalize like brian as the mathematical representations you there's no way you can reason about like your formula so what do we do is say if we can actually use a standard tree from the verification community in the sense that we can do abstract refinement in a sense that let's say at the very beginning we use rereason about brian and yi using an abstraction of gender right in this case you cannot differentiate those two those two because this abstraction is not sufficient enough so which means that if you generate a counter example it will generate a counter example to show that right now sorry i cannot differentiate it so in this case you can actually further refine your current abstract refinement in a sense that well in addition to reason about gender maybe we can reason about the the color of the code that they're varying today right which is sufficient enough to differentiate those two so as you can see so you don't necessarily need to reason about the complex behavior of your software system you just need an abstraction that is sufficient enough to achieve your approval so as you can see this iteration will keep iterating either it returned yes in the sense that i cannot find any kind of example to dispute your argument or i'm going to say that i failed to prove your system which essentially indicated your system might be unsafe okay and the last one is actually pretty straightforward in the sense that let's say once we uh spend a lot of effort verify those individual circuits so for those like a big circuits of million million lines of constraint what you can do is that it's essentially just like when we play with lego right in the sense that for every circuit that we already verify we essentially write down its summary in terms of input output behavior so which means that one and we already verify that we know that it is safe so which means that in when you reason about like a larger circuit is essentially just a matter of stack those summary together okay um that's essentially on all the presentations and then if you have any questions feel free to reach out to us using our first name very nice.com and so you can also access the the prototype uh using the the barcode so one thing i want to mention that's um so this is still like a ongoing very preliminary work in the sense that this project is not even a thing like a month ago so so uh so i highly encourage you that to check from time to time because we are going to spend a lot of put a lot of manpower to make rapid progress in the next few months uh thank you and i'm happy to take questions [Applause] with the specification language basically being circom and the like that's the verified program being the r1cs representation this is basically it it feels more like a test of the compiler than it is a test of the code itself yeah yeah so yeah so in a sense in this case you can think of you're trying to like testing the correctness of your compiler right but like if you replace the silicon program with the actual specification that you want to enforce it's essentially it's a verifier right so so as i show you in the figure so we don't necessarily need to buy to the silicon programming language hey uh thank you for this talk this is actually very interesting here because i do some work in full verification of evm circuits um two quick questions first one at a high level could you give some like quick intuition as to why even though the equivalence spec is based on like this universal quantifier which like z theory is like notoriously bad at handling um how you guys are able to still get it to to work so you mean how do we uh get z3 to work with um with those kind of uh uh like uh like constrain uh in in circuit is that your question right or or at least on one of the slides i saw there was a universal quantifier for um describing like the equivalence between two circuits is it that at some point like you you remove the universal quantifier oh so there's a standard trick in the sense that if you want to when the reason that you have this kind of universal quantifier is that you want to prove um the validity of your uh argument right so that's why you need this universal quantifier and then there's a very standard tree in a sense that to prove the validity of your uh formula it is equivalent to check whether the negation is satisfiable okay so which means that in practice and to get rid of the universal quantify all you need is essentially just put a negation on top of a formula and then you can essentially like use extensional quantifier gotcha okay thank you that makes sense um and then the second quick question is have you looked for or does there exist like theories on um prime modulus operations because i know it's not natively supported in z3 and it seems like you guys have to do this weird modular stuff which you know can result in errors of like unknown sometimes so yeah what what is like the the thinking process there um so uh the short answer is no there's no existing theory theory for prime right now the existing theory for z3 that work very well is a link limited integer arithmetic big vector uh on interpreted functions and their limited amount support of string so right now what we are working on essentially we are working on the theory of prime and then those the one that show you essentially very very preliminary result and we are working on the rest of fragment of the theory awesome super cool thank you thanks for your talk um what difficulties do you foresee um when trying to verify planck is it just like larger polynomials or what what do you think will be difficult um so well like the logic polynomial is definitely going to be a problem uh so everything becomes bigger like it becomes nasty to reason about so which is like not specific to like a zk right it's essentially applied to every software artifact so i think one thing that is specific to zk verification is that um so it's about like the operator this especially for those crypto printed operator so they are actually involve either super non-linear functions or include like a very complex hashing functions so which will create a lot of trouble to the constraint solving for instance we observe that even like some small verification tasks they might generate simple like smaller constraint but it's actually very difficult to solve thank you okay thank you thank you [Music] you