Picus: Push button zk circuit verification

Transcript

hi my name is shankara pylor I'm a research scientist at verdice and today I'll be presenting our work picus which is push button verification of ZK circuits and so this isn't work done just by varadise but also is a collaboration with our friends at Xerox Park and see conduit so as many of you know we have seen a big emergence of ZK applications in web 3 space so we have privacy based smart contracts roll ups and even privacy preserving blockchains and we at verdice have done a lot of work auditing these applications across these different domains and to make our lives easier and their lives of other Auditors easier we've

been building tools to help find bugs in ZK applications and pycus is one such tool so before proceeding I'll briefly go over the general workflow of building a ZK application so at the heart of every application is a circuit and this circuit will typically be written in some domain-specific language like circom or in a framework like Halo 2. and these kind of have two components the circuit will get transformed into two different components one which we call a witness generator and another which is going to be a set of polynomial equations over a finite field and the idea is that you can use some proof system to take these field

equations and construct a prover and a verifier and then at runtime you would use the witness generator to produce Witnesses and generate proofs and ideas that when you're auditing these systems the source code is going to come is going to contain both the computation as well as the constraints and ideally as I'll get uh I'll get into that a bit but before going forward I'm going to just briefly go show you an example in circum so here's like a very simple circuit in circum it's a template technically but here you have two input signals a b two output signals and these three lines of code describe both the computation and constraints so the

computation is going to just do two things one is a field division the second which sets the first output to is a field division and then the second one is going to be the sum of the inputs and then the constraints basically enforce the same thing and then as I mentioned before at runtime you would get some inputs execute the computational part produce a witness and the idea is that ideally there's some caveats before I say this but the computation and constraint should be equivalent and I'll Define what I mean by that more precisely so basically so you're given some program P takes inputs X produces an output Y and a set of constraints C over inputs x y

the idea ideally you'd want for every X Y pair if P of x equals P of x equals y if and only if C of X Y is true so ideally you would want basically the only satisfying assignments to your constraints to be those that are produced by your computation and at Veritas we have found many many different ways that this equivalence can be violated and I'll talk about one today which is under constrained circuits so um more precisely we say a circuit set of constraints see here are under constrained if there is some input X and multiple distinct outputs y y Prime that both satisfy the constraints

and the reason this is kind of bad is that essentially what you're what this means is that your verifier is going to accept some witness that doesn't actually correspond to your computation and in practice this a lot of serious CK hacks have been due to under constrained bugs and resulted in severe Financial loss so to make things more concrete here's like a very simple example of an under constrained circuit so if any of you have worked in circom there's a template called numb to bits so this is a an intentionally buggy version of that circuit so what this circuit will do is it'll take some input signal some integer value in the finite field and output its binary representation as an

array of n Bits and so the reason the circuit is buggy is that it the loop condition iterates over the first n minus one elements instead of all n elements and so when this template is instantiated with n equals three so you only have basically a bit Vector of length three the last element in the array is completely unconstrained so no constraints are generated for that for that bit and so that means that an attacker can basically pass in any value they want so now there's um basically two strategies broadly speak two very simple strategies for detecting

under constrained bugs and circuits one is what we call a static analysis of these constraints essentially you start with a set of predefined rules and then you use those rules to prove that certain signal that signals are uniquely determined by the input so for example suppose you had a set of constraints like the one on the left the rules might say something like this since Z is a function of X and the output Y is a function of both x and z then we can infer that Y is actually a deterministic function or a mathematical function of X and so we know that it's uniquely determined by the input another strategy is using something

called smt reasoning so basically under constraintness can be expressed as a formula in first order logic um and I won't go and basically if this formula is satisfiable that means that the circuit is actually under constrained and so there's a very there's two trade-offs between these two approaches first static analysis is highly scalable you can actually analyze very large circuits and prove they are under constraints but in practice they have a lot of false positives in order to scale you have to do a lot of approximation now smt reasoning the idea ideally you can be as precise as you want and actually you technically have a decision procedure for determining under

constraintness but the downside is it's very hard to scale especially because we're working over these finite Fields with very large primes and lots of constraints in practice however we found that these two approaches are actually quite complementary and so with that Insight we actually built a tool called pikis so pikis takes this input the set of field equations and it actually works in an interactive Loop it has both a static analyzer and an smt solver but the idea is that these static analyzers and smt solver actually share information interactively in a loop and so that allows both to make progress when the other is stuck and the

idea is that the information shared can make each other's lives much easier and so pikis will then output a green check if it can prove meaning that we have a certification that all the output signals are probably are uniquely determined by the input so we call that properly constrained Red X if it can actually prove that the set of constraints is under constrained and then we're going to call this question mark if um it cannot so as I mentioned before technically we do have a decision procedure but in practice because solvers can take a long time we have a timeout and so we return a question mark so the the key there's three key insights here first we're really

combining the strength of both static analysis and smt-based reasoning and we do so by having these phases interact in a loop and I and the idea is that the partial results from one can't help the other vice versa so I'm going to talk about each phase in slightly more detail so we have the static analysis phase which we call this uniqueness constraint propagator takes as input the field equations along with a set of signals K which we have which the procedure has already proven unique and the idea is that at the beginning the algorithm has K be the empty set or technically just the input signals and the idea is that this unique

disconstrating propagator is going to Output a set of new signals K Prime that that its rules have determined are actually unique and the idea is that if all the output signals are subset of this K Prime then we know that our circuit is properly constrained otherwise what we do is we send K Prime these new signals as information to the smt phase and so we call that the semantic reasoning engine so similarly it also takes the constraints as well as these signals that have already been proven unique and it outputs two things which we call K double Prime new signals that are proven unique as well as signals that are proven to be under constrained and the idea is that the input K Prime

can be used to actually simplify the formula that we give to the smt query and similarly uh we have the the correctness condition is the same as before but we if it turns out that if the smt if the reasoning engine says that there is an output signal that is under constrained then we can return this Red X and then if you know within the timeout no new signals have been proven unique then we reached a fixed point and we return unknown and then if we have found if we have found new signals then we kind of pass that back into the static analysis phase and repeat and so here's how the kind of loop works as a whole this is the big diagram I'm

not going to repeat it but we actually published a paper at pldi this year I'm describing this in a lot more detail like what rules we used and stuff like that and so please check out our paper so so going back to this num to bits example this is I'll just show you what pikis produces when we run on that on that example so recall this is the buggy implementation and on the right is going to be the output that picus produces so here you can see debug information that corresponds to like the uniqueness uh constraint propagation so it's applying these different rules and it found like some signals that it knows that are uniquely determined by the input then it

passes those to the smt phase it smt runs the query and it finds an actual counter example so yeah output's a little bit uninterpretable but trust me that's an actual counter example all right so to evaluate picus we collected um so to both evaluate Pikes and also have a you know to facilitate more development in the space we curated a set of benchmarks from circon lib which is like one of the the standard library for cercom sercom is one of the more most popular languages for writing ZK circuits so it has 163 circuits um and we kind of broke up this data set into two individual benchmarks one which

we call the circumlib utils so basically this is a utility templates for be fixed with integer computation as well as some blockchain Primitives and then with another one which we call circumlet Core which is um pretty much that I think it's like the 50 most security critical templates um in circon lib and so here's some aggregate statistics about the circuits so they kind of vary quite wildly in terms of the number of constraints but I think we tried to design them to replicate real world usage and so I'm going to summarize some of the results from our evaluation so we found that picus was able to successfully prove that 101 out of the 163 were properly constrained

we did manage to find eight under constrained circuits and we have reported all those under constrained circuits to developers and the fixes are under review slash under discussion and so now to conclude my talk there's two main takeaways basically we have a tool called pikis it's a fully automated tool to verify and find under constrained bugs in your circuits it uses it leverages static analysis and smt reasoning in a synergistic manner and we have actually made our tool and benchmarks completely open source and here's our link to all our socials and now I'm happy to take any questions

oh okay hi hi I'm Miguel from Surfer monkey so we do privacy preserving techniques we have circuits with circum how can we test it uh how can we are you asking how can we use our tool yeah how can we use picus uh well actually we have our GitHub link here and I'm you can I think we do have instructions in our readme for how you can use it so Pikes currently takes the r1cs format as input it's not a fundamental restriction but that's just the current implementation but if you can pass it the r1cs file uh then it should be able to like automatically run on the circuit and you know determine whether it's under

constrained or not what's the average time for like a circuit okay yeah so we found among the circus that it can certify I think it was like 18 seconds on average it's going to depend obviously on the size of your circuits um so I think you could be anywhere from 18 seconds to a minute but there's timeouts if it's more than a minute then it's unlikely to ever terminate so but there's there's you can configure the timeouts obviously and um we're obviously happy to help you if you have any issues with it and yeah yeah hi yeah really exciting work you know I'm jinda from cellular network we do the extensive ZK framework

benchmarking across you know different Frameworks my question is exactly about the timeout part um looks like there is no guarantee your Loop will always make progress right okay and K Prime yeah there's no guarantee it's always getting no there's no guarantee that that's that's not like my major concern like for some of the circuits we generate is like 40 million constraints so there's like um one thing you can use pikis uh the way I presented it is you just kind of throw everything at Pikes and then have it do it that's not really a reasonable way to use tools in general I think I think the way we like to use pieces is if when we do use pikis is that we take like individual like

if you if you're basically a larger circuit is composed of several sub-circuits then what you can do is like pass in maybe components to pikis learn some information and then you know uh kind of do this in a more modular way rather than giving everything all at once I think that's generally probably the best way to do it [Music] oh no we actually so I think what we you know we do because what we will say we I guess the way we determine no progress is if like you know there's some kind of time out like within the solver or um yeah

yeah so if we so the idea is that so if we observe a fixed point then there's no way then we can prove that there's no more progress that can be made because you know the solver will take the same amount of time every duration um but uh yeah yeah one one thing we've observed is that actually the bit um so first of all the timeout is still due to the solver I think while the

solvers are we're currently using a very prototype prototype version of the of a finite field solver which is specialized to this for this domain but it's a very like new prototype and so it still times out even with all this help from the static analysis some of the reasons I can talk to you offline about why it actually slows down but yeah thank you very much if you have questions please take them outside we have our next speaker right now thank you thank you [Music]