Contract Library: Thorough Smart Contract Decompilation and Security Analyses
EDCON 2019 · 13 Apr 2019 · 14:56
Neville Grech presents Contract Library and the Gigahorse framework for decompiling Ethereum bytecode and running declarative security analyses. Examples cover bad randomness, reconstructed control flow and data structures, gas analysis and ERC-20 checks, showing how Datalog rules can support analysis at blockchain scale.
Speakers
Topics
From EDCON 2019, hosted by EDCON.
Transcript
so we have our next speaker and I'd like to welcome on stage Neville Gretch he is the security researcher at the University of Athens and he'll be talking about aspect of the contract library welcome hello hi I'm Neville thank you for coming today I'm gonna be showing you under the hood of contract library which does thorough smart contract D compilation and security analysis so what are we up to we are static cold analysis experts static analysis is about techniques for creating tools that model all possible
program behaviors this also includes the unintended behaviors including bugs and security vulnerabilities in this talk I'm gonna be talking about Giga horse which is the underlying framework of contract library it's an EVM D compiler so from byte code back to a source level representation but it's also a framework for doing sophisticated security analysis tools with very little code so contract library is a free service right
so you can go contract - libraries comm while I'm speaking I don't want to scare you but most of our security analysis are specified declaratively in the language called data log now I don't want to worry about the details of data log I can tell you that it's prologue without constructors but that's not interesting you can think of it as SQL on steroids and growth so it's like SQL with complex recursion and all Rd compiler and our security analysis are
written in this so take a look at this rule over here here we're saying that a loop is bound in its number of iterations by some variable var that's the first line okay and in order to conclude that property you need to conclude all the properties in the body of the loop and in the body of the rule so the first line says that if we have an induction variable I which is actually a loop counter and there's an exit condition cond and I flows to that exit condition together with some other variable which is not an induction variable then we can
conclude with some measure of success that the loop is bound in terms of its number of iterations by that variable var okay we have over a thousand of these rules running contract library so I'm gonna give you a demo now so here it is in order to use contract library all you need to do is deploy your smart contracts on the aterial may not or any of these test nuts right let's let's take a look at one of these contracts so
as you know in on aetherium when you deploy a contract you don't necessarily need to upload sources but if you want to on contract library comm you get a decompile representation of all the smart contracts so we can see features let me sort by eater to get something more interesting so here for instance we get data structures inferred automatically based on the pointer arithmetic that we see in the and the byte code here we have mappings you can also get like the function names those things are lost in the and the byte code
you also get things such as private functions now at the bytecode level there is no such thing as private functions but we know as software engineers that you know the composing programs is is the way to go so let's get back here so some school statistics about contract library we analyze every smart contract that's ever been deployed on a GT remaineth or on the test net that's over 10 million contracts which is over 1 billion lines of the compiled code after
D compilation it takes less than 20 minutes to analyze the entire main net with one security analysis okay so for one security analysis less than 20 minutes but obviously we have many of these in fact let me show you one of these so if you go here contract library here's a list of security analysis that are publicly available of course we have many more so let's see bad randomness same thing I'm gonna sort by eater to get the most interesting ones and I'm gonna take the first one which has sources so let's look at the
source code of this ok well here it says bad randomness in get random number so let's look at the implementation of get random number here ok let's increase font size so here the author is getting a random number by calculating the block hash of a past block okay now this is not really a random number because as an attacker you can write a smart contract which uses the same random number generator and if the outcome is in the users favor then you you know buy the
lottery ticket or whatever so many of these vulnerabilities that you final contract library are true positives and that's important because developers don't want to be bothered with a lot of warnings which don't mean anything so in terms of analysis and decompilation success we have over 99% of the smart contracts which we scale to and contract library has the best analysis fidelity when compared to existing systems which do security analysis so here's one of
the heuristics that we that we use in the D compilation so this is a disassembly of some etherium byte code this little compiler erases the private functions when outputting the the byte code but however we can reconstruct them so if you look at the first line that's how a function call is is compiled - so the further the the returned addressed is pushed to the stack followed by the data followed by the function address that is going to be called next and then
you jump effectively that jump is a function call right so it jumps till the end here okay now this function then just pops the data performs its computation and then jumps to whatever is on the top of the stack now the last thing that was pushed to the stack was this return address and this will then therefore to jump to the return address effectively that's a return instruction so the D compiler needs to understand all this it needs to figure out where these
jump labels and return Labor's are pushed to and track them via interpreter all calls this is just one of the heuristics that we use finally I want to show you how easy it is to write client analysis security analysis using the Giga horse framework we already have quite a few security analysis implemented including re-entrance e bad randomness which I showed you and this actually looks for just outcomes where the user can have a favorable outcome based on a random number denial-of-service of gas under flows and
overflows in e rc 20 contracts various kinds of taint analysis but also high-level d compilation which is the stuff you see on contract library so here are some of the high-level concepts which you can use as part of a security analysis so we have syntactic sugar where you can use familiar concepts such as these solidity assembly instructions you can also see that there's an instruction called private and this is not something which appears at at the evm bytecode high level control flow
reconstruction to reconstruct the control flow such as loops or if statements and that sometimes useful for security analysis i can give you an example of this like for denial of service attacks it's useful to reconstruct loops customizable dataflow analysis so there's some concepts from the security domains such as taint analysis and the simple dataflow analysis as well and these could be interpreter also apply to the entire contract these are fully customizable moreover we also reconstruct the data
structures of course these are erased at the EVM byte code level but a client analysis a security analysis in order to be precise it must reconstruct these otherwise it will give a lot of warnings which don't mean anything guarded code analysis so what properties what modifiers apply to which code gas consumption analysis thinks such as how much gas do I need to reach this block this statement for instance and that was useful for doing analysis of the
constantinople reentry sea for instance so here's a simple dataflow analysis this is written in data log okay so if you want to create a custom data flow analysis you say new local flow analysis you customize if you want to the transfer functions so this says that when I see a mask instruction the inputs from the arguments flow to the output and I'm also saying here that this dataflow analysis only applies to loops code and structured loop this is useful
for tracking how loop counters flow within their own loop so here's an example of a client analysis so this is a very much inspired by Thomas's Kalinka example for doing ERC 20-under flows so and the second and third lines there I'm saying that I want to analyze functions that match that signature so that's at the transfer and transfer from from ER see 20 tokens okay and then I'm saying that an underflow applies if those conditions
hold but you can see they're in red for instance there's dataflow analysis being used there and at the last line there is also the use of a control dependency analysis controls width so these are very sophisticated concepts but there are easily used within a security analysis in fact the entire thing fits on just one slide right so in conclusion contract library achieves very good results in terms of fidelity I attribute that to high
fidelity D compilation and the use of sophisticated analysis technology the use of the declarative specifications in data log we provide very powerful analysis libraries which can be used in pretty much every security analysis which means that every security analysis will be as powerful as as any other right if it uses these libraries we have industry strength scaffolding so this is not just a research project in fact we scale to the entire block chain and on multiple test nets - thank you very much [Applause]