Zero Knowledge Security in DeFi and elsewhere

Transcript

hello everyone I'm Dimitri coverturvich from abdk Consulting and Emperor also from ethereum foundation so some of you may know me is no deter sum of Sam as a cryptographer and today I'd like to talk a little bit about security of defy and internal applications in the world of zero knowledge and well the talk is pretty short but I would like to introduce you to some really nice bugs that you can see there so that you can get some understanding what are the real problems so when you coding your application in their knowledge so um you might be familiar with the zero knowledge not only in the context of

proofs but also in the context of for labs and you may know that a typical scenario in ethereum is of course the adjustment the transaction then it's executed on all nodes and then the storage is updated with the results of the transaction well if it's executed correctly and in the ziki roll up scenario a little bit different so instead of the instead the transaction itself is fully executed on the nodes the transaction is crafted on the side of a so-called prover but then it's a proof of its execution is submitted to ethereum and the proof is verified on all nodes and then the storage is updated so the proof just uh convinces all the nodes that the storage updated has progressed correctly

so the node themselves they don't know uh uh what are the all steps that led to the storage update they just check that the update was done correctly so what's interesting about it is that of course the nice thing about it is that when a transaction is Big then it's of course better so that it's executed only on the proverb side and the other just verify that it's correct so the verification is faster than a person the transaction itself the downside of course is that still the verification of physique proof is somewhat expensive so we may hope that

in the future we can aggregate these proofs we can batch this proofs we can do various optimization with those but so far well as the correctly mentioned so zakira labs are still it's kind of somewhat expensive another interesting downside well not a downside but rather feature of ziki programming is that the it's the language that is used there it operates on a bit different domain so you may know that in usual programs well in ethereum virtual machine or in solidity you operate with the 256-bit numbers and to use the 56-bit arithmetic or on a regular xatx machine you use like 32

64-bit words bytes and so on so they are all aligned to powers of two but in the ziki code usually uses a different domain it's called a prime field it's a set of numbers that are smaller than certain Prime p and as you get and they you can infer from the name this Prime is not the power of two because it doesn't factor into other numbers and because of that there can be all sorts of issues when you code in decay so we at abdk well I'm DK in abdk and the other a b is my my blood 500 so we at abdk with my longtime colleague

Mikhail has audited a lot really numerous projects that uh did ziki programming and we have found quite a number of bugs While most of these bugs are pretty subtle so I will not go into details but I will try to cover the most kind of simple ones but still uh kind of informative enough for you to see what's the issue of Suzuki programming so when you talk about it's like a programming we usually talk about so-called circuits so circuits are not exactly the programs so circuits the feature of circuits is that they they consist of so-called constraints

and these constraints are relations between the variables rather than functions that are executed on those variables so in regular code you could just do instructions one after another in the world of constraints you impose relations on the data and if you are familiar with for example database programming uh working with the relations is way more different and working with real code and with circuits we when we code in circuits we have to satisfy two basic properties which cryptographers call completeness and soundness so and they are like two sides of pretty much the same thing so the understanding is that the circuits should behave

exactly as the code but what does it mean to behave exactly the code so on one side the data uh by completeness Will mean that every valid code should satisfy the constraints but on the other hand if constraints are valid this means that the code must be valid and this is called soundness if you make a mistake in either side there will be problems so sometimes people say well completeness is not that big a problem because well in the worst case maybe you can just regenerate your code so the the key the problem with completeness is you have some execution that is valid you

just cannot make a proof for it because of some bug in the circuit but the thing is of course this may also lead to fund loss for example if what they are going to do is to withdraw some money from a roll-up for example and if this transaction doesn't work if it cannot be converted to a valid circuit because of a circuit bug then you're screwed so both may lead to funds loss of course and let's see some concrete examples well not about the fund loss but let's see concrete examples of bugs how what bugs are there so the interesting thing about uh problems in the code and in the circuit

is that when you when there is back in the code is usually when someone exploits this bug it's noticeable you can usually so the traces of exploit are stored in particular when you submit when it's in blockchain that everything is in the clear text so a person submits a transaction you see who calls which contract to see all the commands so you can see the entire stack of code execution and everything is clear is clear and it's very noticeable after the exploit after the code was exploited the sedation in the circuit is different the difference is that

since only a proof is validated on the nodes the transaction itself is not validated and because of that if there is a bug and an adverser is able to create a proof a valid proof for an invalid input this means that the proof will be seen as valid everyone sees that the proof is valid but the input is not known you just the proof just asserts there is some input that satisfies the circuit but if the circuit is wrong you just don't see this input itself well for data availability purpose we often

require that the data is provided so that it's it can end well the transaction is should be reconstructed but in general if the proof is valid you don't see what happens inside and because of that it's very it might be very difficult to trace if there is a subtle bug in cryptography or is it back and code in Circus programming you may not see exactly how it was exploited you just say well well there is a valid proof and then all funds are lost so you must be very very careful when when programming circuits so let's see some some small examples what I mean when I talk about constraints

suppose that I execute the code where I compute a square root of x so Y is the square root of x assume that X is perfect square so we don't have any uh any rationality here so suppose that Y is integer here and then in the circuit program that y y and x are linked by some relation What relation is that the relation is that Y is a square root of x it's the same as y square is X is it the same well it's almost the same because we want to exclude ambiguity here the ambiguity is that if

you tolerate in negative numbers then you should make sure that for example Y is bigger than zero uh well I already have six to begin the zero but if x is allowed to be zero then y can be zero as well and constrained here is that y square equals X and Y is bigger than zero so far so good so for for this sort of arithmetic operations writing constraints is not that difficult uh well ensuring that Y is non-negative somewhat's difficult but we can we can omit that so assume that you can do this range check

so this is a simple constraint but let's go into some more interesting examples here so before we go into examples I [Music] um explain why it's a problem that you can work you work on a different domain so in CK programming and when you talk about things like zika snark we operate on so-called Prime Fields this means that all operations are done model of P this p is typically typically for snarks is close to two to the 256 but it's not at all to 256.

because of that when you do operations uh where the result or intermediate variables go get close to this barrier to two to the 56 you may get problems and these problems are exactly here so you see for example when you have like two variables X and Y and so that there are multiple overflows to 256 and in plain evm you just get model reduction in solidity starting with say Smith check you'll get a panic but in the snark what you have is completely different you you don't get panic don't get modal reduction well you do get modular reduction but this reduction is model a different number

so you multiply four by this to 54 plus one what you get is 2 to 56 plus 4 but this model of P well this p is known it's a constant but it's not at all to the 56. so the result is some weird number possibly 250 something bit long and as you can see from this example you have to take care of this so-called H cases so whenever you approach wherever your arithmetically approach to 56 bits you have to somehow constrain it so basically you have to have to prove that overflow doesn't happen in your case because if it happens it's very difficult to recover

so let's see which problems it it brings us and let's consider the second example the second example is modular reduction suppose I want to prove so I execute and decode a modular model of B well A and B are just valid numbers well it integers they're both bigger than zero and R is there is a remainder so uh is it okay if I program my circuit in the and I write this constraint that a is just Q times B plus r this is the definition of uh modular reduction right so is it enough uh a equals Q times B plus r well

clearly it's not enough you should probably introduce R uh smaller than b then it's almost enough is it uh it would be enough if it were if we worked in integers but we work in modulo t What Happens model p in the world model P everything that may overflow will overflow so how it looks exactly here the thing is adversary who want to break who want to submit invalid data and get a valid proof at versic may be able to select both q and R maliciously the queue you might don't even care here

you may not even think okay what's what the problem with q I ignore Q I only care about r but the thing is you do have to care about Q why is that uh the thing is in the field uh any number can be divided by any other non-zero number the division is always produced a valid operation and a valid output in the field and the thing is if adversary wants to get certain r as an answer for any R smaller than being bigger than b

there exists a queue that leads an adverser to this result so if you simply give this as a constraint what adverser gets what adverse is selects he selects Q equal to a minus r divided by B and this division always works in the field ersen is divisible by anything non-zero and if you substitute a minus r over B to the constraint you see that the desired R will be the output so if an adversary is able to select both q and r then you're screwed um

I will later see how we get around this problem but in this get around this rather complicated so let me maybe outline several sources of bugs are all kind of most error-prone scenarios when we have this or similar problems so whenever we have arithmetic that goes over the entire domain so if you work with numbers then that with multiplication approach to 56 bits or close then there might be a problem because you have to range check almost every operation and your arithmetic whenever you have divisions you see you have a problem because division in integers Works

differently from division and Fields you have to take care of that you have to always keep in your head that everything is divisible by anything and the result May explode for example in a field you can divide two by three and the result will be just a huge number uh we never have branching in your code uh it's usually non-trivial in the circuit to implement it because you have to compute all the so-called flags and you have to make sure that uh only one part of the circuit is executed or taken into account depending on the flag value

and of course whenever we have so-called invariance and you have to work with relations among the Dayton rather than direct functions with the data then you also have problems let's see if no I don't have this update Okay so this were the most popular things the less popular things are I just listed here so when if you want to program some kind of they need automation like in Ezekiel zika sync and its relatives if you

uh do range checks and sometimes you you may have problems if you work with different flags like if a b c and d happens but e in depth don't happen to do this e and at the same time if B and D happens but e doesn't happen then do that and so on so all this sort of exploitable all the edge cases that in normal code are never executed will be exploited because an adversary can select all the variables that are part of a circuit that are not enforced from outside and usually an adverser can exploit these edge cases so

this is cases that can't be reached in a normal code will be reached by an adversary so you have to double double care about those and of course whenever you have some implementation of cryptography in your circuit you also it's also error prone because usually cryptographic schemes have very strict restrictions on how they are used and with which parameters and because of that uh it's easy to misuse those so uh getting back to uh to model a reduction uh let me see if I do have model reduction here

and no not exactly uh so with square roots actually the problem with the square root also here the so-called geometric mean bug when you have two numbers both of those smaller than 256 bits and we want to compute their geometric mean the problem is that the square the multiplication May overflow and that's not even obvious how you how you deal with this overflow because both A and B are valid inputs so you can easily program the second part that x square equals to Z but dealing with overflow is non-trivial what you have to do you have to

partition the number into kind of chunks and do kind of school book multiplication and deal with those so you see how how it's done here you can uh you split actually not into two chunks but into three chunks because when you multiply these guys you have to ensure that they will not overflow themselves you have to uh switch the representation for a for B for X you have to multiply all these guys you have to check the equations uh for different terms and only after that you can make sure that this geometric

mean is computed correctly pretty much the same thing happens for model reduction for long multiplication and so on and so forth so I think I'm running out of time and I will not go into branching bags but uh but those who are interested may go into our audio database where we have a number of audits for various zero knowledge projects and circuits and see what kind of critical and not so critical but also dangerous bugs we have uncovered

thank you [Applause]