Developers guide to ZK Security: from Bugs to Fixes - Petr Korolev | OXORIO

thank you okay hello everyone my name is Peter uh I am co-founder of company that named aoro so we do security audits mostly we focus for the last two years for solidity but now we also switched to ZK and found very interesting things that we want to share with mostly developers and everyone who want to know how to write the code how to write it safe on uh circom and different others uh uh languages that using uh ZK and I want to show you what you need to uh point out in in your code and how to make it safe because it's totally different how you write the code in solidity and in circom and different other ZK languages so um the agenda is uh we will check the basic attack vectors that could be possible in uh ZK proofs and ZK circuits and uh the wall ZK systems Al I will show how to prevent these attacks and sorry uh some like mitigation strategies how to developers can fix it and uh some other security approach that you need to check beside the code so I will start from very basic things but this is one of the most important and most common vulnerability it's something like in solidity like reentrancy we can find in almost half of our security audits uh re attacks becomes more complex but still they exist and I think in uh the circus the this type of attack will be most common so uh what happens in just in case I just want to get to know who is my audience here can theise uh hand uh who is the developers okay good uh who write the code on solidity great yes and uh like who know what is the circuits in terms of ZK okay less but I will explain it a little bit more um good so um the circuits basically is there some programs that mostly um from De developer perspective it's like close to the functional programming you work not with the just variables it's more like a signals it's more like um traditional uh circus that you have um just like circuit so you I don't know how to say it in function yeah it's more like a functions and you work with the signals so um under constraint uh circuits it means that you didn't check the inputs and outputs uh correctly so you need to check and verify that everything that you put into your code is uh valid so you usually you just put there like uh some by byes into the input and there is if you didn't check that it's correct so uh verifier can prove something that doesn't uh anything uh I I I will show you an example it will be easier so this is a one of the most important thing just to not get mess with the uh circum assignment operators so if you do something like this on the left is just assignment it doesn't do any kind of checks in your code if you do like this assignment I don't know Point yeah so so this is a constraint so if you want to check that something is constrained and satisfy some uh uh some logic in your code you you have to use this kind of constraint people very can just mess with this very easily and it becomes a a lot of issues with that so like as an example um this is a very basic code so here is a like um uh like Hello World you have two uh three signals and you want to prove that you know like two Factor one factor two and and you know that uh if you multiply them you will get the value three and uh when you do these checks like basically this this is a all all single line proof that you can use but you need also to remember about many different things that you have to check like um that the factors are um um not equal to one so you can just very uh pass through the checks if you will just send not like Factor just one here and uh Factor two will be equal to value um and you will just uh pass and uh prove something that isn't correct um I will show you so how to mitigate these things uh here's a code like basic that we this is a real issue that was in one of our um code that we audit so if we just check this outputs we need to uh add EX extra checks with a uh it looks like this you convert component in Num to bits and uh work with the um with um this amount of um uh bits okay sorry um I think this I just get messed with the several uh slides it should be it's very hard to explain because I just keep several slides yeah that's why um okay I I will just come back later to this so yeah so first I I want to tell uh about arithmetic overflows so when we work with a circus we working with a um elliptic curves and with finite Prime fields and you need to know like if you just do uh didn't check the overflows so uh you you need to check that all the the Valu that comes into the signal is less than your uh prime number of your Prime Fields it's the is depends not of the your code and it depends to the proving system that uh that you're using uh for running this code so you need to check the proving systems and what kind of cryptography is under the hood so uh this like very basic example about how how it works for example if your uh field order is uh for example uh 100 and you have a value like 10 and uh you can just simply get the two two factors like uh and uh pass um uh 11 10 instead of 10 and it it will pass the validation with so to mitigate this so you can check this uh um component that that works with n to be a special fe uh special function that checks that uh your signals doesn't exceed the maximum uh maximum number of your Prime field so uh this is a real example from Tada cash and uh uh Cod and um it was a Sy for issue that was in in the library named semaphor so in it was in 2019 uh it it appears in many libraries that using like C circus nobody checked that the maximum am amount is 2 power 254 in growth 16 and uh In classical solidity code you have uh you in in 2 power 256 because of this you can just easily do double span attack for Tado Cod luckily they found it before uh it get to the life uh so this is a issue you can just check details like uh Roman simonov one of the developer of Tado cash found this and later a lot of researchers uh did a quickly fix for their quot some of them was in production so um there's a like zorres mixus and snar GS this is a very common uh librar that was popular at that time and they're all was affected by the same very simple things uh simple issue with the maximum number that can use in this elliptic curve um yeah so how to medicate uh you you need also to think about your uh signals is not like it's just uh parameters is like number of bits so you need to also to check bit bit lens and uh because they can just be simply trunked in your code if you didn't didn't do special checks for example here uh in yeah I think it's not easy to check this code but the simple thing that if you pass like 01 or one 0 01 it could be be uh both of these things will pass in this code and it will get you the wrong uh proofs so how to mitigate this you just need to uh do these checks with n to bits again with Max bits uh another thing is uh mostly relate to the compilers maybe it's like it's back or feature but compilers uh can remove unused inputs that you uh don't use in your circuit for example again Inn cash they are using some uh inputs to check the um data of relays who will operate with the proofs and uh in the beginning um when they start to use it they realize that you can put any kind of uh inputs into this unused inputs and uh proof will be valid like you you can just do so as many proofs as you want so for now there is no any compilar flags that you can use so you can just do some work around and add some fake calculations that's it and like multiply this uh input by itself and then this thing we will be preserved in in your proof so uh another thing is uh very um basic but I need to mention that please don't use your own cryptography so many developers try to implement and improve some crypto cryptography functions it's very bad idea because uh there is so many cavas that uh just normal developer can't realize that it will happen so I can recommend to check ZK do ZK dogs.com it's a website from audit company trail of bits and they have very good examples how how to mitigate some issues and how you need to use uh how to work with the cryptography functions what you can do with them and what is prohibited so here is some kind of example with fat Shamir so if you just use use the function please don't just put it in just check documentation it's super serious and important in z k especially so also now you can see that so many proving system appeared and uh and they are still in research uh stage so most of them are not audited or verified and even if they are pro are very promising and you think it will improve and give you competitive advant advantages in front of others please don't don't use it because uh later we I'm sure we will find so many of them are not uh uh ready for production code so like things like growth suem this is a proving system that works in most uh uh zy solutions that we have it's very good stable things but not very convenient so because we have a Hala and plon and other things that now also in production they has also like folding schemes they have pairings and everything that uh you need to improve your system you can use them but for new researchers like just don't take it if you see it just faster okay uh one more thing about trust setup this is uh the basic thing who know what is trust setup okay so most all of you uh so in wordss is just the thing that you need to do uh uh before you start to use your verif pro verif ver uh verifying system um uh there was issue in zit cach Zach uh in 2019 this is I think one of the most the biggest and older company in blockchain that using snarks and even they miss uh some parameters in their trust set up mechanism so they did it very well they put their computers in the farad cage they destroy their computer after they did trust set up but the issue was that some parameters uh leak leak not through the MPC like this trust setup Solution by the by but by the sum extra data that before they assumed that they are not related to the trust setup but later they found that from the um final parameters of this trust setup you can recover all these things and you can simply just do validate whatever you want on Z cache they fixed it they say that nobody exploited but now we can don't even check it because nobody knows what happens there so the latest thing I want to check some example from our latest Audi of privacy pools so privacy p is like next uh generation of um uh of Tada but that they fixed the thing that you can prove that your inputs or outputs are not in the list of some hackers group so you can create some dedicated list of inputs and say hey my transaction in this list or not in this list so you can separate your yourself from uh hackers and prove that your money is doesn't relate to money laundering for example which is super useful and could bring the Privacy to the people without any obligations that now we have with Tada um so very interesting thing was in Num to be manipulation so I this is a complex bag that uh related to all the things that I show you before first they uh improve uh num to beats function that so actually they try to write your their own cryptography don't do this please uh the second thing they uh mess up with the constraint thing so they just assign operator instead of do the constraints so technically you can just put uh give here any kind of inputs and it allow to the prover um substitute input that's uh uh originally like uh user give to the prover and generate the valid proof from invalid data or do the opposite very simple thing when only one you can just do one liner fix but this thing can break the wall system so just if and they just try to I think optimize like num to bits and do do some test uh inside so don't do this uh okay so besid uh this you can use this set of tools there is a some statica analyzer some of them do try to do fuzzing with the ZK things and um in the some tests use that cover um cover uh circuits I highly recommend to use the them because for now it's not easy to write the test on on the circuits but if you don't write it at all uh it's very hard to support this LS as as usually in development so in conclusion so programming with the K snarks when you do this just keep in mind this is a signals this is elliptic cryptography and you need to check the math behind that it's not just a normal code so um check the backs and most common things that you can find in the internet and check what what what what what was wrong with them uh the most uh popular is under constrain circuit that I told you arithmetic overflows and you can check like frozen heart and just set up leak this is the things that's related to zit cach issue and uh some other uh things you can easily find this is a lot of information you can check later um also try to subscribe to some ZK groups because there are so many things happens there and uh uh ZK technology updated every months or three months completely so it's very fast growing ecosystem that uh development even faster than solidity uh so just check check it because if you not into this you can easily Miss very important things uh for for for the groups and the reference you can ask me so also if you have some question so we can talk later I will be happy to explain you some details and how to work with the circuits there is also we explained the circom but there is also K noer and different type of languages so they are bit more complex but they are newer and have some extra benefits for the developers they have very fast growing techn development ecosystem um yep that's it thank you and your questions and welcome to [Applause] ask yes thinkk thank you for the talk um maybe like a naive question maybe not fully understand the whole like picture but when you describe the overflows and underflows like looks to me like a issue that should be solved at the type checking level so why isn't this solved at the programming language levels like solidity why am I even allowed to uh make a subtraction from A to B where B is larger than a so so it's because of when you I think they good uh example is so circum is like a circuit there and there is some kind of software then you can write on uh right on top um you never know what kind kind of software and Hardware will be compatible and not you can just constraint the like size of your inputs because if you use different proving system there are different uh uh numbers and uh if you using recursive uh snarks you can also need to work with different math uh approaches so it's not easy to like just simply constrain these things in the circuits even in solidity how many years passed before safe math become a standard so I think five years and only in solidity version a they fixed this and uh before everyone used safe mod which is like like external Library so same happens here here in Circus you just need to check maybe later when there will be some one single standard they will put it into the uh some into the framework and you don't need to check but for now it's all relable the the wall things it's like a Lego you can just build your own from different kind of system like proving system and language that you use cell and so on is it possible to make uh so so is it POS oh so is it would it be possible to implement something like safe math on the circuit level such that I can use the circuit and write this like programs as you described without like if I have a and b and their meaning is um like some balance then it is positive by definition and don't don't have to check it because it's kind of by definition they cannot be lower than zero for example [Music] Yes actually you you can do this and there's a some mathematical functions that's already implemented but the thing is usually uh all the calculations that you do is very unique and you always have to change something in them but of course there is a functions like less than more than and uh num to beats is very basic function then just check this overflow you can put it in the more complex circuit but since you try to optimize everything that you can uh usually there is no reason to make a complex function if you will use only several checks from them yes so we have more questions don't be a stranger raise your hand anyone with that being said let's conclude this session and thank you p for sharing the note with the community