Journey into building security tools for Cairo

Transcript

[Music] okay we are getting ready to start because time is short cool thank you very much everybody for attending this uh Speech and I'll just give Mike to Patrick to introduce himself and to go ahead with it and we'll have no questions and answers but you can ask him when he goes down of from the stage this is quite a good setting for this so Patrick let's do that thank you so yeah I will need to be quick because I have a lot of stuff to show you so let's start so I'm Patrick I'm the

founder and CEO of fezzing labs so we are mainly doing fuzzing vulnerability research on a client and nodes but we're also building security tool for some Foundation like the stock like stock wear and the stocknet foundation so that's basically what I'm gonna discuss today is all basically we build two tools one is tot uh security toolkit because it's like kind of multiple tool it's more like a framework to do security on KO a smart contract and then I will discuss what the Cairo feather which is a further 4K raw smart contractor so just to that everyone is aligned that's Cairo 0 10 and basically when you compile a Cairo smart contract

you will get the Json artifact that will basically contain bytecode and so on so taught as being created because typically back then especially like September last year we find out that when you compile to um your chaos man contract you will basically get a designer artifact and it's not there is no tools available to basically analyze this smart contract so we will it was a need for us to basically analyze what was the output of the compilation so that's why uh tot have been created so it have been created many in July August and we basically start with a disassembler a decompiler and a choreograph so the

design layer is basically a visual representation of the byte code I mentioned so from the stuff on the side the The Purge and data you will get something a bit more visible like the assembly code that you have on the right so you have multiple function and you have the different instruction at the at the lower low level then based on that we create a decompiler meaning that we will take this by code and try to represent in a more easy way what is inside then since we have the decompilation and the disassembly we are also able to reconstruct the call graph so again that's a feature that was actually used

a lot by people in the ecosystem because there was no choreograph tools by default so the main idea is you will take your contract and you will see direct interaction and relationship between different functions and also depending of like Imports and so on so we are representing that at the at the same time that's an advanced example of typically your code graph but for something like a bit more complex like the dye bridge and you will see it's like kind of huge a lot of interaction but it's a good start to to analyze the contract so after that we decided that the basically the decompiler was not good enough so we Implement SSA which is a

static single static assignment so the main idea the concept is pretty simple you have each variable will need to be only assigned once and since we're able to do that we will be able to get a proper representation of each methods is depending of which variable and so on and so on so we are getting something like on the side I will not go too much into the detail but the the idea is we are able to reconstruct pretty properly the the contract so that's SSID complete edition basically and what you can see is from something like the original source code on the side the tough version one was looking like the stuff on the middle so

mainly showing AP and AP and so on which is not really clear for most of people what is what is it exactly and then on the new version with the decompiler we basically create variable and we are able to follow the code a bit more in deep so that was in September in October we got the integration of our tool directly in Voyager and we also start to create a static analyzer so for the integration in vayager the goal was since uploading your Cairo code is not monetary when you are uploading a contract there was a lot of contracts on Unchained already deployed I mean on the

test net that was actually without source code so it was really interesting to actually be able to take a look at that and see what exactly this contract is doing for analysis or even for kind of classification purposes so that's what was done and then we implement the static analyzer so the goal is since we have now a really good representation of from the byte code to have the the contract and be able to do manipulation on that we are able to provide the framework and you can basically write your own analyzer in Python directly so we have multiple of them some kind of detects or some kind of analytics stuff and so on and we also started to

implement security analyzer so back then it was Cairo 010 so there was some vulnerability like integer overflow and so on that was possible and it could put your smart Contracting tool kind of an instable state so that's an example of the of the analyzer it's really simple the main goal was um it was like the basic um of the of the tool and the goal is basically to stamp up um on top of it and create new stuff along the way in November we Implement data flow graph analysis so again it's always to provide more information about what the contract is doing especially if you are doing

reverse engineering on the contract but even for developer it could be really valuable to know actually your input in the in the contract or far it goes and what he is doing so that's data photograph analysis will represent the data basically the data interaction and then we also Implement tenting so that means we're able to tell you okay variable 5 is actually dependent of an input or not and so on we also Implement symbolic execution which I will discuss later what is it exactly so that's pretty much all for 2022 then arrive the Sierra file format and the announcement of Cairo 1.0 so

um that imply a lot of new stuff we are not just dealing with bytecode anymore we also have a new intermediate representation layer that is here and we need of course to deal with it because it will also provide a lot of additional information so the main idea is right now cairo1 is looking a bit more like rust kind of a subset of rust and when you compile that you will compile to CR Sierra is an intermediate representation it's going to be used on the on the on the sequencer part and improver and everything so that's that's used on on one side but you will still get the assembly and the CR code the important Point here is that the CR and the

assembly code is actually uploaded like both so we always have both stuff available so it was looking way more interesting to directly take a look at the Sierra because way more information are basically inside so we basically do what we did again on the assembly level but on the CR level so the compilation it's more like yeah disassembly in in steroid so from the um pure CR cord that is really linear we are able to reconstruct something that look like on the on the left so with tabulation and so on and it's a bit more visible for you to to analyze and especially if you're completely new to Sierra and you don't know what is inside it's uh it's um it's interesting to

leverage on that again we implement the call graph and we Implement some analyzers so again the main goal is to provide you like the maximum of information about what is the compilation output of your code then we started to like deploy more and and make it even more easy for developers to actually use the tools so we Implement vs code plugin and GitHub action really simple it's just calling the tool basically but I'm pretty sure a lot of You Are user of vs card so you can see on the left is basically what this here representation look like so not really the most appealing stuff to to read it

and it's not even the purpose of it you are I suppose it's not on the developer workflow to actually read Sierra code so that's uh that's also why and then we Implement CR symbolic execution so basically symbolic execution means that you will have you will Define a bunch of constraints so you want to have specific variable with specific values and you will ask the similar case equation online okay can you solve this value we basically generate a mathematical representation of that we give that to a smt solver like Z3 and it will give us the the result so in this example we are looking to know the the different value of v0 V1

V2 V3 that are the argument of the function and we basically ask as a constraint to go in some specific path in two specific part of the of the code of the KO code and the final result will be basically the input in order for you to reach a specific point on the on the contract so it's really interesting especially if you are maybe looking to improve the symbolic um like the the different unit testes and so on that's the the kind of value that can be added and also if you implement some mathematical algorithm directly in Cairo this kind of tool could be really useful for you just to assure that potentially it's not possible to go to certain paths

and so on so that's pretty much all at the third like recently last month we Implement something kind of an extra based on the symbolic execution engine that is the symbolic Bond model checker for sure so the main idea is kind of doing some kind of let's say a minimal formal verification but directly in Cairo so you are writing your uh test property test I'm very clean Cairo and you will ask the symbolic execution and join basically can you solve this and can you verify that the assertion is correct so on the left you have like can you verify that if I'm multiplying two number it will not be equal to 11 so it

will fail because there is multiple value for a that will make C different than 11 and on the other side you can see a valid check where we are doing basically two addition between one and two and we want to assert it's equal to three it's really basic really simple for more complex stuff you might get past explosion especially if you have loops and so on that's mainly because the smt solver will have some issue with that so you still need to do minimal testing like really focus testes but it's actually proving you mathematically that the stuff is correct so that's basically all right now for

for third we are still improving the tool and so on and especially with Sierra and the different evolution of of CR and the stuff that have been added over time and it's basically a tool that we will contain to to maintain um and um yeah so if you if you are planning to use it and if you have any issue please just tell me to finish I want to mention the second tool that we we built which is called Cairo further so it's a further 4K or smart contract the main idea with fuzzing is basically to send input directly to the KO smart contract so basically the argument to a dedicated method and we're gonna see in which path of the of the smart contract is going

and if you are doing that 1000 million of time you will basically be able to reach a lot of different paths and get kind of unit testes for free and so on and especially also find bugs so the architecture of the the K officer is actually not that complicated you have a config file and so on pretty basic you have the further you will spawn multiple thread and then depending if it's okay or smart contract or a stark net smart contract we will use one VM or another both VM have been developed by our friend from Lambda class and in terms of exact speed is pretty important like we are able to own like if you're running that on 10th thread we have like 404 uh

for 40 000 execution per second which is really fast and we are able to monitor the coverage so the trace of the execution and based on that the determine like a set of input that is interesting to to you there is a bunch of additional feature but I will not talk too much about that so you have an uh an example right there on the right you have the first symbolic execution it's the same test we are using for symbolic execution as well it's basically a simple contract where each argument of the function should be felt it's representing like a letter so it's fuzzing labs and at the end you have an assertion that is incorrect and the main idea if you want to Brute Force

this stuff you will never succeed because there is too much character to check so you will never reach the final point but the fact is since we are doing coverage guided phasing the further will at the beginning try to enter in the first if check and at some point you will succeed to find the letter F and since he will discover that he is going deeper in the coverage because the trace will tell him okay I'm actually in the song check the second if in that case you will keep this input and reuse that later for other mutation and over time actually we'll finally uh go to the assertion and detect a crash so that's what you get at the bottom of the K officer he actually detect that we have

an assertion an assertion that is incorrect and so on so in that case uh yeah again really good execution speed and we're able to reach this specific point uh in like less than I don't know three seconds something like that so it's really interesting the find the the evolution of that expression on this tool will be the addition of a sequence of calls which what I mean by that is right now I'm we are facing only one function but ideally what you are looking to do is a sequence of calls to maybe put the smart contract in a specific state that it was not before so classical fuzzing stuff if you are already using Echidna or Foundry on evm

it's basically the same but on Koro and it's actually really fast so some future development we are planning to continue to work on on 10 career further we are working with stockware and stagnet to maintain the tool and and to do some stuff in a more generic way I mean we are doing phasing on a lot of different chain so we are also planning to build new further for webassembly substrate Cosmos and other potentially smart contract and also blockchain platform and production framework so that's what we were planning to do and yeah we will continue to do phasing because that's what we like and um if you ever need some Custom Security

tool or of the link please just contact me thank you [Applause] okay [Music]