Zafny, framework for writing formally verified zero-knowledge circuit | Dohoon Kim | ETHTaipei 2024

oh hello everyone um my name is dohun Kim I'm from PSC today I'll going to talk about formal verification framework for circuit constraints using uh horal logic so let's start so today my talk is about first is state of formal verification of ZK circuit programming and second uh existing approaches and Frameworks for formal verification and third uh I'll going to propose new formal verification framework grounded by uh hor logic so uh this work is joint work with uh plrg Leb and Ka and the idea was inspired by the talk with kuk Le at plrg and my also my colleague suan from PSC team yeah so let's start uh so in advance uh let me just briefly talk about what this arithmatic circuit so in order to generate ZK proof we need arithmatic circuit that encodes constraints so these constraints are usually represented as polinomial equations over final field and developers usually write their constraints in domain specific language and the DSL compiler uh often builds arithmetic circuits based on the constraints so there are lots of dsls for now for example like circom Cairo nor and all other things and there is a security issue so there's an a security issue in the circuit when the constraints are incorrect so this kind of security holes and constraints uh can let malicious Prov generate the valid proof so this security of zerol circuits is very critical matter so these are of well-known famous security issues in the zero circuits so there are lots of uh security issues for now so we can ask a question uh what is secure circuit and how can we prevent these kinds of security bugs so let me start with defining what is the secure circuit so first the SEC secure circuit in the secure circuit constraints should be uh uniquely satisfiable so this uniquely satisfiable means that given the constraints and the given public inputs there should be a unique witness to satisfy this polinomial constraints so if constraints are not uniquely satisfiable malicious prover can generate valid proof without knowing the valid witness Witnesses so these kinds of unique satisfiability problem usually can be handled by uh algebraic methods and formal verification methods and second circuit constraints should align with the specification of the developers so circuit constraints should enforce the desired properties the intended specification properties of the developers and if constraints cannot enforce this specification there might be a misinterpretation of the circuit and also the misuse of the circuit so these kinds of specification problem can be handled by formal verification methods so this is the picture for what is uh depicting what is the secure circuit the constraint should be uniquely satisfiable and it should Express the desired specification properly correctly so uh let me first uh to I'll go through the approaches on the satisfiability problem so most naive way to approach this kind of problem is to directly solve the system of polinomial equations to decide the satisfiability so these kinds of problem are usually starts by Computing the graer basis of the polinomial ideal generated by the polinomial constraints so uh I not going to talk deeply about what is graer basis and what is polinomial ideal but just uh think that polinomial ideal is just an algebraic structure and the graer basis is just the generating set of this ideal that has very unique that has very special property so if we are given grab a basis one can apply various algebraic me methods to solve the system so in this paper like on satisfiability of polinomial equations over large Prime Fields they the authors explore various algebraic techniques to solve the polinomial systems uh using graer basis so the most uh most notable approach was that they apply a primary decomposition method by using grabner basis so this primary decomposition method is also based on very very math heavy things but it is just decomposing the problem into the smaller sub problems using the graer basis and then solve each sub problems so this looks really fancy but it has a quite poor performance and scalability issue because uh when Computing the grabar basis of the polinomial constraints we usually uh consider this kind of field pols so I'll going to talk about what is this field pols is in the later slide and this is another approach so second one is it is based on the combination of smt decision procedure and the algebraic methods and they use like conflict driven class learning like decision procedure in this paper so they also used graer basis but this also has the poor performance and scalability when Computing grab on the basis because of the field polinomial and the third one so this also combines the smt decision procedure with algebraic methods but they are have a kind of performance breakthrough uh compared to the prior approaches so the diff difference between the prior approaches was that in Prior approaches uh in order to uh ensure the completeness of the graer based based uh testing they usually uh take into account into the field polinomial into the grabar basis computation but in this paper they removed fi polinomial in graer basis computation and defer the completeness of the test when finding zeros of the polinomial systems so they were quite more faster than the prior approaches but still finding zeros of polom system was quite a very very uh computationally heavy things so uh until now we have SE we have seen the approaches on satisfiability problem and now let's see the approaches on the specification problem so in this paper certifying zero knowledge circuit with refinement types they introduces a new DSL called Koda for formal specification and verification through proof assistant like coch so they were very powerful because that that kind of proof assistant can verify uh every desired property of the program that developer wants but it is very hard for developers who are not familiar with this kinds of proof assistant programming so these are this diagram is the overall uh formal verification approaches so the xais is for the usability of the research usability and performance and this vertical line is indicates the capacity means that what problem they trying they're trying to solve so in satisfiability problem there are several approaches now but in the specification problem we have only for now uh as far as I know uh there's only Koda DSL that solves that tries to solve this problem and this Coda DSL is quite not very uh easy to use for the developers who are not familiar with this kind of proof assistant so I thought that there there are some kinds of Gray Zone here that is trying to solve specification problem and very usable for common developers and also there's another hidden metric of these approaches so this approaches usually um focus on the security guarantee after the construction of the circuit so these approaches are usually applied for con already constructed circuits but this kodad DSL they uh try to guarantee the security by construction because they are uh providing a DSL to program the secure circuit so uh I wrote the wish list of this gry zone so what do we want so we want uh more easier to use tooling and also it should provide formal specification and verification framework and it also should provide guarantee by construction so inspired this um my hopes on this new research I try to propose new framework based on this world logic so as we saw we require better tool for formal specification and verification of the circuit program and we also require easier automatic and systematic formal verification method to solve these kind of specification problem and uh the horr logic system uh I will explain what is hor logic system in later slide but this system serves as a fundamental framework for verifying the correctness of General computer programs and this is generally based on the first order logic in computer science so okay let me explain briefly explain what is hor logic so hor logic is essentially based on this hor triple so this hor triple is consists of precondition program and postcondition and this precondition and postcondition they are just a logical predicates Al so they are logical predicates uh in the first order logic statement and what they States is that before program execution the predicate p is true and this what this post condition Q States is that after program execution Q predicate Q is true and this and these collectively says what is that if program starts with p predicate P true and program executes and terminates then predicate Q becomes true so this is the very uh simple example of this kind describing this word triple so before the program if the variable X is bigger than zero and in the program we simply add one to the variable X then after the program the post conditions might says that variable X should be bigger than one so this part if program starts with predicate P true and program terminates then predicate Q comes true is usually the specification of the program and uh okay we saw the horror triple till now and the horror logic is uh they are just a logical system and they are composed of aums and these kinds of inference rules so you can see that uh in axm and inference rules all the uh basic elements are the horror triple that I described in the prior slide and the horic system decides whether program satisfies the desired uh postcondition from the precondition and the program with these kinds of axioms and inference rules so there is already a programming language framework based on this or logic so it is called Daphne this is just a programming language framework for writing verified program and it is also grounded by the horror logic so if developer writes the program in Dey automatic verifier checks the correctness of the program with based on the horror logic and uh with collaboration with DMT solver and since hor logic is as I said generally it is based on the first order Logic the developers can write their own assertions or invariance like kind of lub variance and lmas to assist this hor logic system so my question was can we adapt this kind of horror logic to write verified circuit so we can imagine like defy like circuit progam circuit programming DSL so like we can augment the existing dsls like circom with automatic verifier that is also grounded by horic like dfan but the difference with de is that uh Dean is for verifying the general compter program but we are focusing on verifying the correctness of polinomial constraints inside the program for our desired specification so like irrelevant part with the constraint generation like uh irrelevant part like witness generation Parts can be just ignored when uh in the verification procedure and also as in like dfan developers can assist hor logic with their own assertions libin variance and lmm too so let's see one example so this is the circom num two bits templates so this template uh inputs the parameter n and it has input signal in and the output signal out so out is an array and this num two-bits template is just converting this input in into their bit representation and contain them to this array out so and this num tobits template is uh useful when we want to constrain that uh certain input should be smaller than 2 to the^ of N and but uh have you ever thought that this template is really really uh constraining this post condition correctly like we we always believe that but we want to write the verified program for this desired post condition so let's uh reframe this circum template into the horic framework so we have a precondition that n is less than equal to 254 that is based on like some other facts but and this template become a program so and the post condition becomes that the input should be smaller than 2 to the^ of N and it can say that if P becomes true if p is true and after C executes then Q becomes true so uh actually this num two bits template is not a self uh executed program but just let's imagine that this is a program for uh yeah program yeah so now we can augment this circum template like this so it is uh Defan style programming uh syntax but so we can write our precondition with requires and we can write post condition with insurance clause and uh in order to uh constraint that this input should be smaller than two to the^ of n uh we can use these kinds of uh loop invariance so let's see more closely that so this part the loop is the most uh important part and inside the loop we can just uh ignore that witness generation parts and we have one constraints that out I elements of out array should be equal to zero or one and based on that we updates the variable lc1 and variable E2 and the developers can write in the Lubin variant that variable E2 should be always equal to the 2 to the^ of I and variable lc1 should be less than 2 to the^ of I and I is always less than equal to bits then at the end of this Loop we can say that this uh lc1 is less than two to the power of bits based on this Loop invariance and after the loop ends there is a constraint that lc1 should be equal to in and now we can say that this n is smaller than two to the power of bits so this kind of um inference rules are very uh crucial in horal logic so yeah and in this style like developers can assist or logic system with their own Lubin variance uh in this fashion so uh in order to achieve this we propos new extended horror logic system so now we can uh think about this new extended horror triple like this so we still have precondition post condition and instead of uh just general program now we have a constraints and now the precondition and post condition they are the polinomial constraints augmented with first order logic and what they States is before program execution uh this p is satisfied and after the correct program execution this Q is should be satisfied and collectively they say that if constraints p is satisfied and program terminates it means that c is now satisfied then it should induce that Q true so uh in extended horal logic also we ignore as we saw we can ignore the witness generation parts of circuit inside a verification procedure and also we should cover polinomial constraints and polinomial constraints is not natural inside the general program so it is not basically supported by the original horor logic so we should extend the horologic rules in order to handle these kinds of polinomial constraints like this one yeah so still we have only one extended rules but maybe we can have more and more rules after the research uh proceeds so this is the recap uh now we have a precondition and circuit constraints and the first question was is precond condition and circuit constraints can be uniquely satisfiable and the second question is that is precondition and circuit constraints can induce our desired post condition so it is uh our specification problem and as we saw this unique satisfiability problem can be handled with grabiner basis or like elimination Theory like various algebraic methods and these kinds of specification problem now can be handled with this kind of extended for logic or new kodad DSL from uh the previous slide and key takeaways is that now we can classify the circuit verification problem into two problems so one is unique satisfiability problem and the second one is the specification problem and we can adapt hor logic to solve these kinds of specification problem and ex ention so we extended the horor logic to embrace these kinds of uh polinomial constraints and we also proposed like new systematic and automatic verification framework for circuit programming based on the horror logic okay so this is end ofline talk uh thank [Applause] you and now we have like 3 minutes Q&A a time does anybody have any question do you have a repo of examples for zne code with const strings so uh this is in very early stage and still in PC so I haven't open sourced it yet but I will soon open source this uh repo too yeah thank you thank you does anybody have more question okay thank you thank you