ZK9: Fuzzy Knowledge Fuzzing SNARK circuit primitives – Innokentii Sennovskii (Aztec Network)

Transcript

foreign [Music] now we're going to learn a little bit about fuzzy knowledge which is uh fuzzing snark circuit Primitives by inokenti from astok right all right let's hear it [Applause] so yeah hi my name is Anakin say I work at atstack and I'm going to be talking about how we added fuzzing to our circuit so that they became a little bit more secure before I start I'd like to thank Edo Rankin for helping me with

this project so uh to start with let's look at what security of circuits is to me it's like this hellish Tower of complexity which can Tumble from the smallest touch at the bottom we have the basic uh base field Primitives which for example in our code base are implemented with Montgomery then on top of that we have all kinds of stuff such as elliptic curves multi-scale multiplication ffts on top of that we have scalar Fields where we actually start implementing the circuit logic with various gates for example we use ponkish arithmetization obviously and on top of the gates we can

finally build some of the basic Primitives which the application developers that are using our systems to create final proofs we'll actually use so this whole Tower complexity very easy to break one thing and if you break even one small thin then you can disrupt the correctness of the whole agreement and the pro or the whole proven system so let's see what we can do with the circuit security so one of the traditional ways to kind of cover the security is through unit test it's the most basic thing you should always do it for example our code base is simply covered with them and they do ensure that you uh do just the

smallest base the most basic uh security it means that your circuits will not suddenly fail on the most basical functions so for example you know that Edition works the way you insert it that no new changes to the code base especially if you are actively developing on top of it no new changes actually break all of the old stuff so yes it's a nice place to start obviously not enough then we have the end-to-end tests which kind of help you cover the base that the whole system works as intended at least for the thin one you are trying to ship so this for example we added it to a code base when I understood that yeah

unit tests are definitely not enough sometimes there are still small things that fail so an end certain tests help you see that what you're deploying is actually working but then we actually want to improve on the security we don't simply want to check that our code base is working so the first thing that most people do is and internal audits that means that either the person who implemented the the classes implemented uh the code base or somebody else for example somebody who wrote a similar primitive a different part of the code base comes and looks into what you've developed suffers a lot takes a lot of time to look into this stuff but uh kind of

holistically checks that there are no strange assumptions no weirdness that another person implemented and usually it is quite an in-depth check but obviously this never covers anything so what do we do we go to external Auditors and one of the issues is that with external Auditors you always have a very limited time frame which means that even the best teams of which well there are some but I think there are more projects than there are audition teams that can actually check those projects nowadays so those teams have only a very limited time so they can look at a small primitive and maybe ensure that it's correct but that's the limit of it

obviously they can't cover the whole code base especially um such a huge one as our bresenburg library so even after all this the thing that we have is this which is not enough we'd simply like to check our code base even more especially the core Primitives that we're using so for example we have several core circuit Primitives which are very important to us so what do we do in this case well we need something automatic that's a very important thing we can't simply delegate to various Auditors internal or external because that means that we spend more and more time on human resources our code base grows we need to spend even

more and any small change to any part of this code base after the audit can complete the just right away all the money that we spend before that because it's a new bug is going to be introduced and now all of those checks are useless so what do we do well in the last 10 years apart from the ZK Cambrian uh blow up there has also been a Cambrian explosion in uh gray box Farthing so you can look at it this way originally you have this very simple uh way of testing which is called the unit test we are testing a very small primitive we're checking that it

simply works then we have black box fuzzing which we'll go into detail a bit later but the idea is you stress test a small part of your code base you do a lot of computation on it with different random data to check that it is operating correctly and what you do next is at least to me when I started learning a bit more about it seemed like magic because now you have some sort of algorithm that learns itself what it should research and how it should test your code base so let's start with the basic Black Box fuzzing harness to see how the system actually works so let's say we have this very small program which simply checks that a particular stream is being encountered in an input

if a particular string is being encountered then it writes out then it triggers an abort so this would be something like a bug in our code base Basic Black Box uh father would fuzz this function in a very simple way it would generate some random data for example we are taking this random data from the system Randomness or if we are more efficient we are using a pseudorandom number generator and then we are sending this new created input data to the program under test this function then we see if this has triggered some sort of bug in the function and obviously if we check at

the bug we found something new great for the first uh if not we go into the next iteration and we continue doing this the problem with this approach with the black box was an approach is that especially for this letter like style of code how about the good your generator is there's always a very low probability of the Black Box fuzzle reaching somewhere deep inside your code base like for example with this function their first step takes around once divided by 256 uh probability the next one is even less than that it's one divided by 2 to the power of 16. and so it continues so if you had eight steps uh in this code

then you'd never reach them on a single core on a single machine in your lifetime it would simply be impossible so obviously this has a serious drawback so what do we do well with gray box fuzzing there's a smoke change instead of Simply generating the inputs to the function we now use mutation so let's say we start with no information about the process and about the program initially we have what's called an empty Corpus and Corpus is just a collection of interesting test cases for us we take something from this Corpus right now it's just a simple zero length test case Zero length input we mutated so that means that we are

changing in such ways that at least some part of the original test case of the original input is left so it doesn't completely generate something in you it updates something that was before then we said it to the program on the test and this mutated test case operates uh just as any other the input would then if a bug is triggered we do just as in the Black Box further we just output the bug finally we found something if not then instead of just repeating the loop like we did before we send the coverage data for analysis and coverage data here means that either we collect the information about various branches

being taken or maybe various comparisons being taken then we look if any particular branch in on this new execution has never been taken before so for example in this case if we are starting from scratch we see that oh the first if has actually been passed through so we found a test case that goes that starts with an A and we save that test case so now we've actually changed our probability distribution because in our Corpus we have a new test case which has already found the first symbol so to find the next one uh now having if we pick the this test case from the Corpus would have the probability that originally for the Black Box father and for this father

was to find the first symbol a so we continue like this and after several steps we trigger the airbot so the basic info is we have an algorithm that remembers where it stepped if it steps somewhere in you it also remembers that and then it tries all of those different test cases that it found and updates them instead of just forgetting about them and running along with something new and this is a very powerful technique since 2014 when AFL American fazilop was published it was kind of the first open source I'm not sure about 100 that it was the first that it was the most popular rise at the time uh father

that used this mechanic uh with the coverage there has been just an explosion in various vulnerabilities found in open source projects just because people started using this technique and applying it everywhere to each project that there was so now about The Primitives I'd like to introduce Big Field as an example of a Primitives that we'd really like to fast so today on this stage there has already been a talk about this field arithmetics that is non-native to the scalar field that we are operating on it is a big headache for us at least it has been for some time and we're using it kind of in

a different way to mina we're using it for the roll up the base principles are the same so we are trying to emulate these uh a base field element on top of scaly field for that we need actually five elements that's because we're using the crt's formulas which I'm not going to go into detail here about but we're using one scalar field just for the scale affiliate modules and Ford for 2 to the power of 272 modules we also have tracking units which are used to optimize constraints in our circuits because if we just do it straightforward uh in our code base without trying to optimize this a lot along the way it

will just cause an explosion in the number of gates so we need to optimize this quite a lot so yeah constant source of headaches tons of bugs found at various stages there so how do we fast Big Field well let's start with a simple stupid Black Box fuzzer let's pick a function for example here we see a basic addition function we take two random elements convert them to The Big Field elements add them and check by creating the proof and verifying it seems pretty straightforward so this is the simplest thing you can do this is something that you can start with you just run this function in a loop and you have a basic Black Box button but obviously there's

lots of room for optimization the first thing is well creating the whole proof each time you want to check a simple a simple circuit Primitives is way too much effort so for example if we you were to use the plant Province system it would mean that we'd have to commit to stuff so that's multi-scale multiplication then we'd have uh we also have to spend a lot of time on ffts we'd have to do theater to just check a few like maybe less than a hundred Gates well in long maybe a thousand but yeah that's just a lot of effort to check a very simple primitive so instead of that we do the simulation in our case it's just going through

various Gates looking up the values of variables instituting the witness value is there and checking that all of the gates hold for uh concretely for our Witness having done that we've already increased the speed of our fuzzing a lot I think when we did this the speed went up by a factor of a hundred so what do we do next uh in our C plus plus code base we use the function lvm for the test one input which is something that's provided by clang there's this very nice Library parser it it is very simple uh to add fuzzing to your project if you are doing rust there's lip processes uh cargo package which basically does the same thing so

you also you can do absolutely the same stuff so what we do here is we receive some data from the leapfos from the lip Plaza backhand so our father is already supplying to us mutated data this way we check that the size of the buffer is enough for us to take two elements in the base field we just realize them into the uh into the base field elements set Big Field elements from that and after that we add the values check the circuit also one of the nice features of the fuzz is

that you can simply return -1 if there's some sort of problem with which you on which you want to trigger the father to say okay some assumption has been broken Uh something's bad here and you simply return zero if there are no issues so that's already pretty good now we've added very simple gray box fuzz into our code base we're checking it automatically creates coverage so the the only thing is you have to compile with a particular Flags now you have coverage now you have an automatic fuzzer that checks that your circuit is correct and goes through all the various stages to look for yeah to look for the correctness of a very simple function in

your circuit so uh what's next well there's this concept of Oracle in gray box fuzzing it's quite different from uh the oracles that we encounter in crypto the basic idea is this you have some sort of security policy you'd like to adhere to for example in binary fuzzing you'd like to check that you haven't read any uninitialized memory or you don't have any undefined Behavior once again I know for rust people it's not as important but for us it is uh so there are these oracles but we can also add cryptographic workers and Oracle specific to our code base so in this particular case we not only check that the circuit holds but also that the

value produced during this simulation is also the correct value so we choose to check that the value produced in The Big Field uh class is the same as the base field element that is also down through the summation of the original elements so now we have already graybox fuzzing we have a simple Oracle this is probably the most you can do with the one function by just using live fuzzer but one of the problems with lip fuzz and one of the greatest features for binary mutation is that liposite has very binary specific mutations uh so there are three classes of mutations in lip

fossa on the left here we can see the individual value mutations so for example when you take a particular test case in this case it's coffee that's one of the few words you can write in HEX so there are several things that you can do one you can flip a single bit in the test case you can sleep a sequence of bytes you can substitute a particular one two four by chunk by a special value for example there are values like oxf or values like ox2 which are special because there are lots of constants like that because there are a lot of underflows that can happen like that

then you can also trees some part of the some part of the test case as a unit of size four you can do small additions and is small additions and subtractions on that and that's basically what the instruction what the value limitations are then you can also do structure mutations on the test case uh you can insert bytes you can duplicate bytes you can Shuffle some bytes in the test case and the final and one of the most important mutations in leapfroza is splicing where you take two test cases and you start picking by sequences of bytes from the from one of them and from the other so you're kind of mixing them

in together this is done so that you can take features from both of them and maybe find some new code paths inside a class by getting information from some other code path so this is very powerful but this is not very efficient for the cases that we are talking about so we are working on uh the uh we are working in field elements so we want field elements so one of the first things we did was introduce specialized mutations and here there are several things that we can do the first one is we treat the values as field elements then depending then we

choose whether we want to treat them as something that needs to be converted to Montgomery form first or not the point here is a lot of the time when we are doing this fun and stuff we do comparisons somewhere in between lip Plaza can do that so for example it can look at these comparisons somewhere in the code and check oh this is a nice value if I can substitute this value somewhere in the test case then I will probably pass this if statement and that's really powerful but not when you have a Montgomery form in your code base when you have some sort of form which is very nice for additional multiplication very nice for actual arithmetic but that is not the actual value that your outputs and not the actual value that is

present in the test case so to use this powerful feature like half of the time when we are mutation a particular field element we first converted to Montgomery then we apply the mutation then we convert it back to plane to save it in a test case and then we have three choices one is to delegate to live for the mutations to use those powerful features the second is to use additions and subtractions with small values but modular our base field Prime because we know that the arithmetic is different here and the final one is to substitute special values but special values that are special for the base field because obviously they are different from the binary ones so here these are various

roots of unity to the scalar field that we are working on because that is a very special value that can also break some stuff so just various special values and yeah then we either convert back to the plane form or continue and this already has produced some very so this already produces some very powerful mutations we apply uh several of them at the time so both in leapfaza and in special mutations not just one mutation is applied every time there are several mutations usually applied in a sequence so for example in deposits five so now we have a very specialized Father which for one function we have an oracle

we have uh coverage and we have specialized mutations and now there's really nothing that we can do for just one function so what did we do next well one of the problems with Bigfoot is that it has an internal state so that means that if we take two values of our base field and we construct and we construct a Big Field element from them we might never reach some of the internal States in Big Field by just do one addition so obviously we are not checking for all the cases all the problems that could arise there so the next thing that we have to do is basically substitute this one uh one

function phasing with the fuzzing the whole system of The Big Field so instead of fuzzing just two field Elements which you see on the right we create this instruction vector and the instructions there are pretty simple so we can store a witness or a constant value in Big Field to a particular stack that we use in just as an intermediate so for example here the stack is all four elements and then we have different basically all the various methods and operators that we have in the Big Field cost multiplication Edition division assertion that something is equal to a different value and by using this instruction Vector we are basically manipulating the different interactions

that can happen within the Big Field class between all the different methods that can happen so for example here on this slide we see an instruction Vector where we first store a witness into the zero positions or a constant in the the first multiply them together store the result into the second position on the stack add the results from the zeroth and the second and store it back to the second and then divide the second position by itself and store it in the third so just using this instruction vector and mutating it we can explore all the various different states that can happen in Big Field and at the

same time coverage and leapfos is guiding us so obviously mutating it is a bit different to the accumulating the just The Big Field element so what we have to do here is once again reintroduce value structure and spicy mutation the spicy mutation works in the same way only it operates on instructions instead of bytes so for example you take the first instruction from one test case and the first instruction for the other you you can just go like Checkers you can take different sequences with the value mutations we mutate either a particular index on the stack that an instruction is taking

inputs and output and outputs into so for example we can substitute the index from zero to one if it's a storing instruction then we can change the value from witness to a constant and back or change the value and there we delegate the value change into the thing that we saw before that the way we mutate the field elements and with structural mutations yes they're kind of the same we can swap two different instructions together in the test case we can duplicate instructions delete instructions and this way we are exploring everything that can happen in Big Field obviously it's it's not formal verification but it is very efficient in

practice so yeah one of the last things is we have to update the bug Oracle because we don't just have uh one uh function here so because in The Big Field we are tracking the maximum value of Limbs because we're tracking the maximum value of the whole uh because element and since we are checked since we are checking that the value of The Big Field is equal to the value of the base so these are the checks that we implemented that no limbs ever overflow with the maximum value that there are no overflows to the whole maximum value and that it's always equal to what we're actually trying to

simulate uh so yeah uh one of the apart from that one of the things that we introduced is a random seed instruction so apart from storing and all the uh instructions in the various methods uh this is a very simple instruction that allows us to cycle through various Constructors through Big Field there are various ways to initialize a Big Field element this allows us by changing one value to switch between them so that we can holistically check all the states then we also implemented instruction weights at some point because multiplication is obviously much harder than addition and we don't want to use tons of multiplications at once because it will

degrade the speed of the puzzer and one of the cool features that we used in lib fuzzy is the length control because if you limit the size of the length of the instruction Vector initially and you allow it to grow slowly instead of just quickly explode it means that your father has more time to explore individual cases before it degrades speed and reaches more more complex situations before going through all the easier ones and I'd like to finish with what kind of bugs we found with this so even though we had an audit for our base arithmetic uh before that we found actually a Montgomery Square in box that's why it was that plank in the

beginning that's why it was that problem uh we actually saw that our basic big field formula is not always correct we found a case where it was broken it was a very uh low probability Edge case like astronomically improbable but somebody with a particular mindset could have used it for something bad then some of the infield assertions have been broken we had several range constraint overflows Sac Falls because our code base agency plus plus and uh Winston Constantin consistency so this is a case where a lot of the time when we're building circuits we are writing the circuit Primitives for a very particular use case and we are not checking that the witness and constant stuff is

actually 100 percent identical in logic so because here we are cycling through where the values are witness or constant we are kind of ensuring that they are identical in logic so yeah and that's it thank you for listening to me [Applause]