Ecne, Applied ZK - Day 2

[Music] hi everyone my name is franklin and today i'm really excited to talk to you about acne the first ever verifier for zk arithmetizations let me give a quick review because i know you've seen a lot of zek proofs these last few days zero knowledge proofs allow someone to prove that they have a secret x so that f of x equals y where f is a known function also sometimes called a circuit and y is a known value zk snarks are powerful because they let you do this for any function f not just specific functions that at a high level zk snark construction involves two phases the first phase is converting the function f into a qap which is a set of degree two polynomial equations over fp this is also sometimes called an arithmetization this conversion process is often very manual second this qap is then converted into a zk snark and this process is mostly automatic now let me give you some examples of qaps so a very simple example y equals x cubed converts into x2 equals x times x and y equals x2 times x hopefully it's relatively clear why these two equations are equivalent now a more non-trivial example let z be an array of size two and let y be z of i okay so now let's let i equal zero if i were equal to zero then note that e1 equals zero as well since e1 equals zero and e0 plus e1 is one then e0 is one and by the last equation y equals z of zero this is kind of a tricky case but hopefully it shows that qaps can often be rather complicated even if the functions are simple this also reflects that qaps are very powerful essentially any function can be converted into a qap even functions that don't look like mathematical expressions so why does this matter so for a zk start to be secure the translation from function into qap must be exact and it's especially important in zpdk because oftentimes if a protocol has been exploited we won't really know sort of by the design of a zk protocol today qaps are usually constructed manually which leaves open the possibility for pulls or ways that this function to qab conversion is not exact to show some examples in the real world where this has happened there have been holes in well-known zk circuits for example dark forest a very well-known zk circuit had a missing bounce check which led there to be a hole aztec's non-native field arithmetic also had a missing bounce check which led to a hole and note that these bugs will often appear completely without warning so look at these two pieces of code at the bottom they look very very similar to each other in both of them you have an input x and you have an output of size three in both of them two times out of zero plus out of one is equal to x however in the first one out of zero by this quadratic is equal to zero or one and same for out out of one thus x lies between zero and three in the second example we constrain out of one and out of two you might make this mistake if you have an off by one error but all of a sudden there's no constraints on x anymore circom will compile both of these with impunity so we need to figure out a way to distinguish these and acne can tell the difference so if you run acne on the first one it'll tell you that x is bounded between 0 and 3 and the second one it'll tell you that x has no bounds so this is exactly what we want before i further go into how acne exactly works i'm going to define two terms that i use regularly weak and strong verification so the system of equations is weakly verified if there is at most one unique solution for the output variables given the input variables and this is enough for most security purposes because we have an algorithm that gives us the output variables in terms of the input variables already so as long as it's unique then it's all good the second type of verification is strong verification those of you who are familiar with formal verification will find these notions very similar and this shows that a system of equations maps to a formal mathematical expression so this system of equations defines a function and this often requires complicated specifications for what that expression exactly is which often are not available to give a very specific example say that we had a qap for big integer multiplication this is a relatively complicated qap so this begins your multiplication corresponds to x1 x2 x3 times y1 y2 y3 equals z1 z2 z3 we would consider this qap to be weakly verified if we could show that z1 z2 and z3 were unique given the values of x1 x2 x3 y1 y2 and y3 for strong verification to be shown we would need to show that the output z1 z2 z3 of this qap which is a system of equations satisfies x1 x2 x3 times y1 y2 y3 equals z1 z2 z3 so there's a difference here and note that with strong verification we can hope to use downstream properties of x y and z whereas in weak verification we can just show that z1 z2 and z3 are unique so what does acne do acne will take in a set of qaps that are either weakly or strongly verified you refer to these as trusted qaps and then try to weakly verify an input qap the first step in this process is using prior knowledge where we find instances of trusted qaps within this input qap so if in this system of equations we see a subsystem of equations that we know corresponds to say big integer multiplication we just replace it with big integer multiplication and don't waste our time on all these equations then we use an inference algorithm to weakly verify this qap so to provide a schematic we start with this untrusted input qap we have a bunch of trusted qaps we run it through a prior knowledge engine which gives us a simpler qap plus some special constraints so maybe there's like a big integer multiplication constraint now not just our original q ap constraints then we run it through an inference algorithm now let me describe this inference algorithm this inference algorithm works by maintaining a variable state which tracks currently known information about each variable some of this information includes things like is this variable uniquely determined which begins as true for both the inputs and one is there a lower bound and an upper bound as we saw earlier and lastly a very cute one which i've never seen before called an abz group and an abc group is a group of variables such that at most one of these is not equal to zero and we know exactly which one it is then we also provide a set of inference rules which tell us how to update the variable states to give some examples of inference rules the easiest inference rule is for a constant k if k times z is uniquely determined and k is not equal to zero then z is uniquely determined this is relatively straightforward and follows from the fact that we're working on prime fields now some fancier inference rules if a times x equals b for an invertible matrix a and b is unique then x is also unique lastly with the abz group if x1 plus x2 plus x3 is unique and x1 x2 and x3 belong to the same abz group then we know which one of these is non-zero and that must be that unique value thus all of x1 x2 and x3 are uniquely determined now let me talk about the inference algorithm this algorithm works by maintaining a queue of equations that we consider to be promising okay so this starts with variables equations that don't have a lot of unknown variables for every single promising equation we try every single inference rule to learn about the variables and every time we learn something about a variable x say that we discover the variable x is uniquely determined we push all equations that contain that variable like y equals x squared onto the q even if these equations have already been processed now that we know something new about x maybe we can learn something about y so for example here we can conclude that y is uniquely determined this step saves a lot of time because we only push equations onto the queue when you might when we might make new progress on them and this leads the overall algorithm being linear time now let's talk about some of the very exciting results we got acne can verify with no trusted functions 49 out of 76 of the circuits in circom lib which contains a lot of well-used functions on the more practical side let's first talk about the ecdsa circuit this is a circuit used in cabal which we saw yesterday and assuming the strong verification of big multi-mod p and big mod we are able to verify the ecdsa circuit completely to give you a sense of scale this is about 1 million equations in 10 minutes which is many orders of magnitude better than you can do with the grogner basis solver the more natural approach to this question it can verify tornado cache when we assert the weak verification of the peterson function which is an elliptic curve function from circumlit now tornado cache is a very well used protocol in fact it's arguably the most popular zk protocol so this shows that acne can verify lots of production level certificates recently we also read it on hermes and we discovered that it can verify hermes roll up made with some asterisks that have to do with authentication and hermes withdraw no asterisks with absolutely no assumptions on trusted functions so this is also very cool because hermes is also a very well used set of circuits now let me talk about how we envision acne being used so acne lets you show that something is verified assuming that other things are verified and this lets you home in on the exact conditions that are tricky to verify so say that we can show that a is verified after we trust bc and d if we can do this it suffices to check b c and d and nothing else so we only have to focus on b c and d which dramatically reduces the surface area we need to focus on for example in the ecdsa circuit i was able to show using acne that ecdsa was verified as long as big multimod p and big mod had no issues with them we actually found an issue in big multi mod p and acne told us that we had to focus on big mulch mod p now let me look ahead to a frontier of something that acne can not yet verify acne can verify lots of things but this is something we can't yet verify and it turns out that's that's that happens for very deep reason okay so this is the addition function on the baby job job elliptic curve and initially it looks that everything should be fine beta is uniquely determined because it's the product of two inputs same with gamma same with tau same with delta then we have that one plus d times tau times x out is equal to beta plus gamma and we want to show that x out is uniquely determined here and it seems like this should be fine however there's a problem if one plus d times tau is zero then all of a sudden x out would not be uniquely determined and initially i thought this this was going to be a real problem it turns out it wasn't though because there's this paper that shows that one plus d times tau can never be zero it's theorem 3.3 and that paper linked but this is a very very non-trivial argument so acne wasn't able to come up with it but that's kind of expected anyways furthermore this also shows the limitation of our approach which is that to show that one plus c times tau is not zero you need to use the fact that x1 and y1 lie on an elliptic curve which is not something you can express in a variable state because variable states only concern single variables whereas this point lies on a curve concerns two variables so some next steps are that acne algebraic capabilities are relatively weak like we saw in that previous example it cannot reinvent all of modern mathematics and it would be really nice if we had some more of these right i don't think this is a hugely pressing concern because most programs are not really inventing new algebra and the ones we do need like the baby ad curve i saw previously already have some formal verifications of them like this explicit formulas database from the hyperliptic website in conclusion we're really excited about the potential applying acne to all kinds of zk circuits and if you're interested in an audit please do not hesitate to reach out to me at my email address here you can also get by this lovely qr code thank you [Applause] [Music] you