Hunting Blockchain Clients' Bugs with Concolic Execution

Transcript

Okay. Hello everyone. Uh thank you for coming to this presentation on hunting blockchain clients bugs with concolic execution. I'm Kolina. Uh I'm doing a PhD between Telecom Paris and Ledger Dungeon. Um the Ledger Dunon is the security research team at Ledger and we are working on this topic um since two years now. Before we start, um, I wanted to ask you a question. Um, can you recognize this guy? Yeah. Yeah. Just say it. Who is it? Gopher. Okay. Right. Gopher. So that's this little animal representing the Go language, Go community. That's was designed by Google in 2009.

And Go language, as you know, probably is used a lot in our ecosystem. Um so here's just a representation of how we can evaluate the impact or at least how much go is securing um our ecosystem. So we can estimate that it's at least uh $60 billion uh that can be um that are uh that rely on go security uh through Ethereum ecosystem layer 2 um multi- chains. So um that's a lot and that's why when I started my research I wondered how much go is secure because it's not such um old language. So I tried to look at that um and be yeah and

while doing that I was also looking to the vulnerab vulnerabilities that exist um and that have been reported to the blockchain clients mainly because go is mainly used in blockchain infrastructure also in backends and uh other types of of uh of um infrastructure and for blockchain clients you can see uh vulnerabilities that have been reported to the CV database but as you you know it's kind of uh old uh and not really relevant. So we explored also audit reports for all the main uh providers and we look to the existing bugs and how we can uh improve and improve uh the code uh security and uh reduce the uh

the number of them and looking to the go uh tool chain and to the existing tools for go we we saw that there was a lot of uh good static analyzers uh fuzzers also carry based tools um which are good of course they are part of the ecosystem for several years for most of them. Uh but what was surprising is that we didn't had any uh specialized symbolic execution tool. Um and just for those who are not familiar with symbolic execution is just one of the techniques uh that enable you to analyze the security of of a code. So normally you start with static analysis

which is just scanning for uh for bugs. You then normally do fuzzing just uh sending uh concrete values to your code and trying to make it crash. Um you'll heard a lot about formal verification. Formal verification which is a good method to mathematically prove the correctness and coverages of your code. Um and in the between of fuzzing and formal verification we have hybrid methods uh somehow based in symbolic execution. So um this consists of just taking your code and trying to um trying to look at all the execution path of it and uh look to the one where there is a vulnerability at the end. Um so that's what we we do and to be even more precise um there are different types of

uh symbolic based u execution tools or methods. Um so here I wanted to for the one that are the more most experienced among you just to give you the difference between what we call compositional execution and concolic execution. So we saw symbolic execution. Concrete execution is just when you normally execute your code with concrete values and you can combine these two because sometimes symbolic execution um explode. So when you have too much path to analyze uh at one point it just crashes. So you have to somehow mock uh or um add concrete uh values at some path of the at some places of the

execution to uh keep it uh keep the explosion. Um and we can do it with compositional execution. That's why I think runtime verification is doing with their tool symbolic that is a focus on application layer. Uh and in this work we've choose to to do concolic execution which is both concrete and symbolic because we think that um it's it gives the the most um tools and the most material to have a good analysis of of our program. So that's just uh what it is and then we had to look at the existing tools in the web two ecosystem because um if you reme remember right now we are looking to go uh go is mainly

used for infrastructure as I told you for go clients go ethereum all the forks uh the layer 2 forks that are based on on go uh it also happened that some uh several smart contract are also written in go uh but for go we wanted to know if existing web two tools can handle go binaries and for that we had to look at um um the method they use the intermediate representation they use. So this this is a concept uh that is just taking an intermediate level between um uh the the language that's uh the source code of the binary and uh using this representation to be able to better analyze the the the code. So this is the

intermediate representation and also you have SMT solver. Um most of the time it's Z3 but there are also others that are specialized for special purposes of of finding special types of bugs or verifying properties. So this is all the thing we you have to look for. Um and uh for go what was striking is that you can't really analyze a go code um statically because the runtime and the garbage collector are heavy and they are deeply linked uh to to to the code. So we tried to for instance take a blockchain client and to compile it as just a library but that didn't work and that was not even realistic. Um and

that's why we had to have a tool that was able to um handle the runtime and the garbage collector which mean handle cys calls and CPU instructions. So knowing that you have to go low level and most of this tool didn't have the symbolic implementation of u cold instruction or CPU instructions. Um that's why uh we wanted to create uh to propose a new tool which is called Zorya. Uh it's written in rust. uh it has the intermediate uh representation that is the pod. It use Z3 and it uh is able to handle most of the runtime the go runtime and uh the garbage corrector. Um and yeah let's

let's deep dive into these choices that we have made. uh first the intermediate representation. We could have chosen others because for instance LLVM is used a lot but it happens that the Go LVM compiler is not maintained anymore by by the developers. So uh we couldn't really use it. Um others specialized languages um have less support than PCOD has in our opinion. So picod is associated to the gra disassembly tool. Uh for those who do reverse engineering uh this is one of the only open-source free uh tool uh that is uh well used and maintained especially by the community and it also

uses intermediate representation. So using it uh for our symbol our concolic execution method uh sound a good idea especially that it's quite granular uh which mean that you really um go uh down in terms of the of the stack. So you will ask me what what does the pod look like? Um this is a screenshot from gidra interface. Um you see the addresses of the program that you analyze. In the middle you see the intel set instructions. So here we have move and cmp exchange. Okay, whatever. What I just wanted to to show here is that uh for one uh instruction like CMP exchange uh which is one Intel uh instruction um

from the the Intel set you have many uh PCOD instructions and uh that's that shows somehow the granularity of uh when you are looking for vulnerabilities and patterns of vulnerabilities that you can somehow understand that we can go um in a precise analysis of of the path that can lead to a vener ability. Um yes. So this the this is our intermediate representation and since I told you that we have chosen to do concordic execution we have to implement each of these instruction both concretely and symbolically uh in Rust with the Z3 uh crate. Uh so yeah so each each time there is an operation that is done uh we

do it both uh concretely and symbolically. And uh you can also see here uh registers um and memory spaces. So we also have implemented that um CPU registers and uh memory section uh symbolically and concretely to do all this operation uh in in the both way. Um and this is the overview of our contribution uh of our contributions. So when you take a target binary in our case is it is mainly go binaries in ELF uh format um we generate uh the their pickut so it's a file and we use for that pick generator uh which is a homemade also tool because there was not

easy way of extracting uh the pod from gedra. So we had to to go through things to do that. We also implemented a parser uh and since I told you that we do concolic execution, we also have to dump uh the CPU register values and the memory uh regions uh to know uh what are the values at the starting address that we have chosen. So we can start the execution from start uh from main uh from any address of a function uh and uh and and do that because of this uh this mechanism and then the execution goes through Zorya. I hope you like the logo.

It's cute. Oh, I hope it's okay. And uh and yeah and at the end you have in the execution logs uh uh statement if uh Z tree has found any satisfiable states or not um given the environment that we have chosen. Um so here is just the first strategy. It's very very simple. It's a small piece of go code where you see that there is a nil map and you try to get a value from the nil map but that triggers a panic because it's a Neil map. This is a very simple code and um you expect that uh symbol on the symbolic execution tool would find this um however um so yeah that's just uh the

workflow you choose for instance the starting address which is start um and uh the your binary and your you you you want just to find this because it's straightforward uh but it happens that the state-of-the-art tools like radus 2 or mash are not able to find this uh Um it's the reason is very simple is that these tools have been built for C or C++. So when these tools look for these vulnerabilities they look for for instance actually uh a pointer to be uh a new pointer to be the reference.

However in go that never happens because the compiler is smart. Uh so it will not let the execution to uh to uh to to the reference a pointer. So it will uh lead the execution to a function that's called um new pointer neil panic. Um so that's what that's what we are looking for in Zorya and uh that's why we just can find this but this is a very simple example. uh also wanted to underline this important point which is um pod uh is used in gidra and with gidra you can analyze many types of binaries uh including C, C++, uh Rust or all other types of languages. So uh since we are

working with POD, Zoroya is also in theory able to do concordic execution uh for any types of binaries that can be translated to Picot. So we also wanted to try if Zora is able to find these three um simple vulnerabilities in C binaries and uh yes it was it was able. So yeah that's the conclusion. Uh but just uh what it what it requires is that requires us to write the right invariant at the right level. So for C binaries your instance you look at the store um the the store uh instruction if there is a a new reference that is being done and so on and so on. So you have to do it manually but once it's done it can be

detected for any any binaries and any any function. So that's kind of can help. That's the ongoing work strategy two and three uh which consists of uh starting um for the strategy 2 uh starting at main. So for go binaries main is main domain. Okay. And we want the the strategy is that um the tool is designed for uh developers who built for instance layer twos who have forget and who wants to check if the implementation is good.

So they know values that make uh succeed their binaries. So for instance here we work with a broken calculator uh which has uh this condition. it it does any type of calculation plus minus divided etc but if the two operand are five and five then it does a nil panic that's just a test binary that I have been using uh for the development of Zorya and uh the goal here was to know if Zorya would be able to say me to say to me that if input one input two equals 5 then there can be a panic even if I give to it a two plus three and this is a kind of simple example but technically

it requires um some uh uh engineering uh for instance you have to follow uh the the arguments of the uh of the binary which are stored in os.orgs args and then each time that there is a conditional branching uh you have to explore the non-taken path to see if possibly that could lead to a panic. Uh so that's what we we do that we what we call the negated path symbolic execution uh which uh which uh which here uh enable us to to find this type of uh uh of of vulnerabilities and the strategy tree is the same but then you start at a function. Uh so here is just a a function that pars a string and in terms

of background and uh engineering uh you have to um to get the function signature uh to be able to know uh where are stored the arguments of the function uh what are the types and then to generate the correct symbolic uh uh the correct symbolic variable that uh correspond to to to the to the type. So for instance here we know that the two arguments um we have the a function that parse a string and the string has a pointer and a length and both will be stored in register LCD and so we have to follow it symbolically and concretely during all the execution of this function. Uh so

yeah that's just just two examples to show what we do and how it's a bit done uh uh in the back end. So our challenges are also to implement the symbolic length of argument of a binary and a function. In short, we just want to be able to see if there are overflows or underflows. And this concept is very interesting for that. Uh work on a concolic multi-threaded execution with a symbolic gouler because for now uh we can only uh analyze monotreaded binaries. Um there are all these tools that I show you before they all works for monotreaded uh binaries.

uh ours too. But the goal is uh to analyze real world uh um real world binaries. We have to handle multi-threaded symbolic execution. So that's the next step and it's a big step. And also write reant relevant invariants. For now the only environments invariant that we have is that the execution can never go into a panic function. That's the main argument. It's generic enough. Uh but we still have to think about other uh relevant invariants and maybe also more blockchain oriented. Uh to answer your question also we can write invariants in source code in like macros and compile the binaries with them and and see if uh

the execution can also follow um validate or not this invariance just in in parenthesis. And how far are we from real scenario? Um we are currently trying to automatically reproduce uh bugs that have been found in manual audits. Uh hopefully we will share some result soon. And of course this uh symbolic gouler that we are we are thinking about that for several months and hopefully also we we'll suggest something uh in the next months. Uh yeah so that's the conclusion. Zora is the first congregate execution tool uh using gRA pod uh as intermediate representation and optimize uh for analyzing go binaries. We have open

sourced Zorya uh one months ago. So that's why I'm doing this talk here. Even if it's not everything is not finished yet. I really look forward for your feedbacks if you can test it if you can report issues if you can uh do anything that can improve this. uh it has been peer reviewed also and accepted in academic conferences. So it's already already in archive. You can also uh look for the paper and uh yes I think I'm done. Thank you very much. Yes. So we have time for a couple questions if anybody has a question.

Thank you for the talk. Very cool. Also very cool tool. I'm string trying to trying to understand what is Z3 and what do you use it for? Z3 is a SMT solver. Uh so it's um we use it if I go here in the graph uh here. So uh it's a it's a satisfy satisfy module theory solver. So when we write invariant for instance that the execution can never go into a panic function uh we then uh if we are in in a in a path of the execution when we detect a panic we ask uh Z tree uh what were the condition uh that can lead

to this path which mean in our case we ask for um for the arguments of the function or of the binary. So if we are here in this case that we panic uh we at this point we ask Z3 uh what are the values of uh RCX and LDX which were the uh the arguments of the function uh that could lead to to this panic and and same for the case when we start at main and that's how we uh then uh can find that it's five and five because of all the symbolic constraints that we have accumulated until uh this conditional branching and if you want to know more

in the GitHub I have some examples of uh how it looks like in the technical side. Okay, thank you. And also another question um why does it work on tiny go and not with the native Go compiler. Yes. So um tiny go is the go compiler that was designed for tiny spaces like microprocessors and it generates a binary that is monotreed so one thread and for now as you see we our analysis goes from a starting address to the next address to the next one next one but we are not still able to create a new thread uh so that's the only reason um uh if I if I if I if I if I would uh give um a B a Go a binary compiled with

a classical Go compiler um Zorya would get lost but not only Zora all other symbolic execution tools because they are not done for that yet. So it requires some optimization because if you just duplicate the state each time you have a new thread again you have an explosion. So you have to do optimization to for instance only uh duplicate the register or the memory that is relevant and so on. So yeah, for now this is where we are. Awesome. That's all the time we have right now for Thank you very much.

[Applause]