ZK12: Improving ZK Applications with Formal Verification. - Marcin Kostrzewa

Transcript

[Music] all right uh hi everyone uh my name is Martin Costa I'm the CEO at rabs and uh today I want to talk to you about uh formal verification of ZK ciruits and our approach to it and how it can also enrich your development experience um Beyond just the uh ensuring security of of your systems so formal verification what is it how do we do it um so formal verification is uh the use of specialized software to reason about programs um we typically use uh proof assistance like lean or Co

soon to be called Rock because of the obvious uh reasons um and it's already used in in many critical Industries so like uh airspace or uh Automotive they they put their uh their most critical systems through uh formal verification to make sure that uh well planes don't crash um and it's ging some Traction in ZK already so there's been some some recent very exciting results there's been the announcement of uh collaboration between ZK sync and uh nethermind on uh on verifying their onchain verifiers um we also did uh some work with worldcoin for example so like worldcoin circuits for State Management

are now formally verified we know that that there is no like funky business going on in the circuits um and the typical process is audit like um meaning the team freezes the code base they send it off to like a formal verification shop or like a formal verification plus an audit shop um they look at the code they write some proofs the proofs verify we are done my main point of this presentation is that you should do it inhouse and you should integrate it into your into your development experience so it should be uh it shouldn't be an audit it shouldn't be a oneoff it's something that you should have running on your continuous integration server uh it's something that you should be thinking about all

the time and I'm I will try to convince you that this also gives you some additional tools um that are sort of missing in the in the current landscape um so you can get this two birds with one stone situation here so uh let's start with what a circuit really is and and how it works and how do we build them um so one part of it is the witness generator which is a normal well behave well behaved program uh you write some code the code outputs some numbers it's all deterministic all nice also all of it is irrelevant for security um so this is almost like a a side helper kind of uh kind of program that uh isn't really

checked cryptographically the thing that is checked typographically is the constraint system which is a bug of equations and all of those equations have to to be satisfied simultaneously um the witness generator is a tool to instantiate the variables uh in the constraint system and the tooling that we use uh typically pretends that they are the same thing right so if you use cir for example or Noir or gar or uh some dsls like this um you will write everything once um and then the tool will output both the witness generator and the constraint system um this has some problems because those are two very

different paradigms right like a buag of equations um that do not necessarily have a a unique assignment is a very different beast from a program um but obviously most of us are developers so we are trying to uh make everything fit into the mold that we've been trained to to work within um for years so let's look at a at a quick example so binary representations um the first food gun NK developer uh Encounters in their life um so the problem is get the binary representation of a number the witness generator is what a developer would do um so the E uh number on the on the output is some bit twiddly magic extracting the uh extracting the if bit

from from the input right this is great um but we are working with bugs of equations over finite Fields uh we don't really have access to fast uh binary operations so what we do instead is we invert the logic and we just say I will be given a bug of numbers and I'm going to Output some equations that these bugs these this bug of numbers has to satisfy such that it has to be the binary representation or foreshadowing a binary representation they are not unique not always at least um so the constraint system is just a bunch of assertions that every output bit is a uh is really a bit so the number times one minus the number must be zero so the number must

be zero one and when you run the uh sort of binary reconstruction on that array you get the original input so that's the property and it's this this split is problematic um it's nondeterministic so this can lead to issues if you assume wrong things for example if you if you assume that this has a unique solution you may have some problems and examples of this are actually vulnerab I found in uh both Gnar and Noir at this point uh where some comparison operators assumed the uniqueness of binary representations and now I can prove that

zero is greater than one uh and it's really easy to prove that and the other problem uh one pertaining to tooling is that there is no way to interact with the constraint system directly um if you if you use any of those of those dsls the way it usually works is you just try to write tests using the witness generator but that sort of defeats the purpose right because if the if I'm using the witness generator then I'm assuming a unique solution so there is no way to like play with the constraint system try to break it actually like what I'm arguing for is a sort of repple where I can just look at the at the constraint system and try to break it and I will show you how formal verification can actually give you that

missing developer tool so um all of our work is happening in lan4 uh which is first of all a dependently typed functional programming language um what that means for people that are not in the like programming language Community it's a functional programming language uh dependent types means you can really do a lot on type level right so like think generics in generics in generics uh kind of stuff it's also an interactive proof assistant um so you can write proofs about uh about programs and about mathematics structures you can join the two words together very smoothly um and it's interactive so uh the way you write it is I will show you later but you get

a tiny window that tells you this is what you need to prove then you write some incantation that will hopefully move the proof forward um and you get okay here's your new goal um so this can really be used as a repple for for theorems a repple for for logic um and also all the proofs you write are code um which comes with all the NCS that code really has um they are maintainable they are collaborative um they are inspectable right so so the other side of formal verification is using smt solvers which are really like those magical black boxes that either prove your uh prove your theorum automatically or there they fail awfully and there is nothing you can do um in this in this regime we are

uh we are able to edit our proofs we are able to like nudge the approver in the right direction so let's let's look into how we actually model arithmetic circuits in lean um so first of all we will use the proposition type uh prop is a shortcut for proposition so the type of logical statements um so our logical statement will become a huge proposition that needs to be proven um we also will use continuation passing style for composing different constraints because uh you sometimes want to have a a sort of abstraction of of a function right so so we want a sub circuit that returns a value uh we will use

continuation passing style so really callback uh for composing larger theorems uh like that and we will need uh two gadgets uh one of them is unconstrained and unconstrained is just using existential quantifiers uh to produce values out of finer I'm just saying that a exists and a will satisfy the later Builder or like it will have to satisfy the the the continuation of the Builder the Callback um but I'm not saying anything else about what a is um so this is a great abstraction for the uh for the bug of equations model right because the the the equations do not give you assignments by themselves um they just

tell you this has to be satisfied uh and we also have an assert which will take a proposition and it will assert it so it will just end it uh with the rest of the uh with the rest of the Builder Okay uh let's look how we can actually use this to do something let's go back to Binary representations um so the first definition we have of a subcircuit is going to be unconstrained beats um so you can see on on the first line I'm oh also uh this is using do notation which is like a syntactic ncity if you are into programming languages it's a monad uh if you are not then it's a it's syntactic sugar to make it all nicer um

so line one I'm just producing a vector of field elements of length L out of ther I'm not saying anything else about it just that and then my binary representation for f is going to be a bunch of unconstrained beats um oh sorry I also forgot to mention uh the second line of that function I'm asserting that for all indices in that Vector uh the number is either Z 0 or one right so this is uh this is the first half of the of the binary representation constraint system and then binary rep uh it takes a bunch of constraint beats uh and then it asserts that F so my input to this

function is the sum of uh is the same as the sum of this Vector zied with the vector of powers of of two uh is this definition clear for now I will take the silence say yes so uh we now have this let's now see how assignments to the Circuit correspond to to proof so our constraint systems became theorems or became propositions they become logical statements now what does it mean to assign a circuit it means to come up with a proof for that logical proposition for a particular set of inputs so assignments will give rise to

proofs um on the other hand if I prove The Logical statement I know that an assignment exists uh we need to be a bit careful uh with the notion of existence here so I can sometimes prove that something exists non- constructively um and then I cannot actually extract a a witness right so so the so it's very useful that we actually have the witness generator uh output by the uh by the uh by the DSL right because that that is the the constructive leg of it so just to give you an an intuition of what I'm talking about here uh let's say I have a circuit that asserts uh that I know of a hash

Collision in ketak um I can prove non- constructively just by just by accounting argument that this exists therefore this circuit definitely is assignable um nobody knows how to actually assign it but the assignment exists so you need to be a bit careful when you when you think about it but this doesn't compromise the security properties it just uh means that you can sometimes prove properties for which you couldn't actually extract an an assignment and interactive proving is now going to be our repple for interacting with constraint systems um how does that work uh let's go back to the to the example of of binary representations so I have this like run circuit which takes the the continue the

the the Callback based uh Builder uh I'm instantiating my field to be uh numers module of 17 so the prime field uh FP 17 uh and I'm going to be looking at at uh binary representations of length five for the number one uh and you can see that as soon as I type this magical buy Here Lin is going to give me this popup with my current goal so uh this this Turn Style like this this sideways t uh it it tells me this is what you have to prove now uh and now I'm going to be doing some incantations in the uh in the proof script to move this goal forward so the first is simplification so what I'm

doing is I'm just unfolding some definitions um simp stands for simplifi simplification uh the name was created before it was a meme um so yeah uh simplify uh those definitions and I get a new goal and the new goal is there exists an a which is a vector of of length five such that for a they are all zero or one and the sum is is correct right so once again rehashing rehashing the same example now it gets uh autom automatically inserted for us by lean um so I can now just come up with an assignment and I can say exists uh which is I'm just going to give you the

example directly um and I give it a vector of 1 0 0 0 0 um that's a great binary representation for one um but now I can also be malicious here and this is this is where my uh sort of red light uh should pop on this also works um this is 18 right and uh the natural number 18 or like the binary representation for 18 um this is also a great binary representation for one if you are working mod 17 um so this is how you can shoot yourself in the food uh if you are not careful enough um and this I will tell you from my previous

experiences that this is something that is really really missing from most existing dsls um so I actually found this bug in in different in different places uh for example in gark it's really difficult to show them that there actually is a bug um so in order to in order to inject the wrong witness generator uh I actually had to Fork the tool mck with the witness uh with the witness generator and then generate a proof on the like generate a circuit the the constraint system on the original version of the tool and then I had to Fork it I had to change the weakness generator and show them that I can use this forked version to actually uh inject something uh something malicious so this is much easier right like I had

an idea for okay I can cheat here I can just show that this idea actually works this is a valid proof so really we are achieving the goal of lean becoming a reppel for con Trin systems without witness generators um so let's move on to a more involved Case Case Study um so this comes from work we've done with uh light protocol uh which is like a ZK compressor for Solana we were auditing their circuits um and they use this definition of of a comparison um so assert is less uh you subtract the two values uh then you add 2 to the^ 248 and then

you check that the result is less than 2 to the^ 248 um this is a very good way to to do a comparison because uh range checking a value is cheap comparing two values directly is not cheap so this is like a good proxy for that um can you see why why this works right like if if a is larger than b um then when I subtract this is going to go over 2 to the^ 248 so the only way for this to be smaller to 2 248 is if this is negative right or infinite field a very large field element that is close to uh Zero from the from the other side um so this works great uh as long as as long as all the inputs Like A and B are

checked to be two 248 bits long if they are too large you get a you get an overflow you can you can actually break this um so they have to both be range checked um the client didn't really know that uh but uh they used it for a sort of double check or like a a a range check but I'm not using that term because of the of the name Collision um for like a sandwich check so they wanted to check if a is less than I is less than b um and a and b were values that were already publicly known and we knew they were always going to be uh less to 2 to the^ 248 but I was not so my first thought got them right

like they are using they are using AR range check wrong uh here I go uh this is this is an example of assert is less P minus 20 p is the the the field I'm working in so this is a huge huge number uh because this is happening on the B and 254 curve so this is like a huge 254 bit number and I'm proving it's smaller than 10 um that is definitely what not what they've intended so hooray I got them right uh I got a very nice finding to write in the final report it's broken we saved you so I'm trying to construct a counter example for the whole thing and now I'm cooked um it's actually impossible um this thing

actually works um and I can use lean to prove that the first comparison acts as an almost range check um so if the uh in the first comparison if the if the a is already range checked uh and it's a bit of a weak range check for compos composability later uh I can know that my assert is less implies the arrow is an implication that first of all a is less than b as expected so I don't actually have to check the right hand side parameter I only have to check the left hand side but I also know that the right hand side is not too big I know it's at most a plus 2 to the^

248 so this this is an accidental range check almost um so I can I can then prove that the second range check uh is now safe the second uh the second comparison so actually the double check if I do it twice right so I I I go assert is less low with value and then assert is less value with high I actually get the get what I want right I get the the semantic comparison that I really wanted so it's not a buag uh it's an ingenious optimization it's a feature I've proven it's a feature um but we should also discuss if it's really a good idea to have this feature in your code base

right um like none of it is happening in the void this is this is happening in the life system um people are probably going to change it uh and this this reasoning that I've that I put forth is kind of brutal right like it all it all hinges on the fact that 2 to the^ 240 eight is still far away from the from the size of the field so I still have some leeway to like go over with the rain checks and it's not going to overflow it's it's very brutal um what happens if someone doesn't understand the logic and just changes it well then they've introduced a vulnerability to the code base so um this is the really really awesome part and this is why you should have this integrated uh in your development workflow and not just a part

of of the audit uh you just put it on CI uh um those proofs uh they get uh automatically checked by the by the link compiler so you extract your circuit into this you prove the theorm you check the FM on CI if someone changes the CC such that the theems Do Not compile anymore the CI fails you are safe so so you can really do some some crazy optimizations right like optimizations I wouldn't really be comfortable with normally uh you can do them now with formal verification because they are now magically safe and they become much less of a food gun so yeah uh the missing bit of it is you need to compile from your DSL to uh

to lean to make all of this possible um so we've built a tiny compiler uh you can you can take your gar circuits output equivalent lean definitions then you can prove things about those lean definitions put it all on CI um we for example have it uh in production at at worldcoin where this is exactly the the workflow and this is coming to new this year I'm working on the on the next version of this tool um so you will be able to compile newr programs into lean and then reason about them um and hopefully with some nice composability so like we will be able to hopefully build an ecosystem of formally verified libraries and then if you depend on formally verified libraries they can

expose some Lamas that you can then use in your own proving making this all uh very seamless so the full full workflow is you write your CS in the DSL you use some compiler if it exists if not maybe you create it that would be great if this uh ecosystem could actually grow um you use a compiler to emit lean definitions and then you you have at it you poke at it you try to break it you prove things about it then you check everything on the CI and then you repeat it so this is this is the strongest Point uh don't just do it once actually have it be a part of your of your development workflow and that is all from thank [Applause]

you thank you we have some time for questions if anyone has any yeah uh super interesting talk um I've been kind of learning Le for myself so really cool to to see this use case uh I wanted to ask uh to what extent have you thought about um automation I know that lean has like a way that you can like Define tactics and like some things are like especially as a noob like hard to prove or like if you haven't worked with like mathematical proofs so to what extent is this automatable and or like some parts automatable of making these proofs and to what extent have you looked into that yeah so so the situation is a bit different for for the gnark tooling and

the Noir tooling I'm working on so for gnark it's um you're mostly reasoning about mathematics at this point um so just usual in automations come into play you just you just do it uh as you would with with any other program uh with Noir it gets a bit more involved because like Noir has for loops and ifs and all of that um so we actually have some some automation for that so we have like a tactic that will convert your your goal from talking about lean to back to talking about mathematics again so that's okay so little follow-up question there um so you're translating the Noir code itself into lean not like the outputed a constraints or other things

yes so you're kind of trusting the Noir compiler that it's like basically compiling things correctly yes yes I'm I'm totally doing that um and that is uh that's a very interesting uh like philosophical debate that that that we could have um so on one hand yeah it would be probably safer to work with as for example directly or with in in in case of gar to work directly with the R1 CS constraints but that gets very unwieldy uh those are they they just get very very big um and it's difficult to actually maintain such such a proof system right it's uh you cannot you cannot easily split it into lemas you cannot really say that like you you

cannot really prove something for a subset of the equations um because you just can't see them all at once right so the the added structure of I'm actually uh working with a structured programming language that's very helpful for me I see thanks thanks a lot I have a question on that um workflow when it's integrated into a project where you say okay when you change the circuit um then you see CI breaks and the proofs doesn't work anymore and so um you have to you have to fix the circuit maybe but I think in practice what often would happen is that the proofs can be can still be patched so usually it would break if you change the

circuit but it's still correct I don't know so do you have any experience with that with the workflow like P patching the proofs um do you go in and do that for your clients or is there workflow um that this projects developed for how to do that so uh if we if we do it ourselves we just try to go hand in hand and yeah when you change something in the circuit the proofs usually break so it's not uh like the the the structure of the proof typically kind of resembles the structure of the circuit so even if you if you do a non like if you do a safe change you still have to revisit the proofs and and fix them um kind of like a test suit right uh like very deep unit tests or maybe even worse than a

test suit because you're actually depending on implementation details but that's the only way we can do it um so yeah uh when we do it ourselves we try to do it at the same time for for both the circuit and the uh and the proofs um for other clients for example Right light protocol uh that was an audit audit like process not really an not it but uh sort of one of we come in we write the proofs for you um it happened in August and they haven't changed the circuit since so I don't know what's going to happen there thanks thank you [Applause]