New Ethereum talks, every Monday. The week's conference uploads by event, in your inbox.

Loading player…

The Inner Workings of a Smart Contract Decompiler by Tomasz Kolinko (Devcon5)

DevconFri, Oct 9, 2020, 12:00 AM

Visit the https://archive.devcon.org/ to gain access to the entire library of Devcon talks with the ease of filtering, playlists, personalized suggestions, decentralized access on IPFS and more. https://archive.devcon.org/archive/watch/5/the-inner-workings-of-a-smart-contract-decompiler The workshop will teach some of the most useful algorithms and tricks needed to analyse and decompile an EVM smart contract: symbolic execution, memory modelling, loop handling and so on.Techniques shown during the workshop are useful in anything related to contract analysis - from writing your own decompiler, through using existing tools like Eveem, Mythril or Manticore, to working with formal verification K Lab style. Based on the experience from building Eveem.org decompiler and analysing all the bytecodes on the Ethereum blockchain. Speaker(s): Tomasz Kolinko Skill level: Intermediate Track: Security Keywords: technical Follow us: https://twitter.com/efdevcon, https://twitter.com/ethereum Learn more about devcon: https://www.devcon.org/ Learn more about ethereum: https://ethereum.org/ Devcon is the Ethereum conference for developers, researchers, thinkers, and makers. Devcon 5 was held in Osaka, Japan on Oct 8 - 11, 2019. Devcon is organized and presented by the Ethereum Foundation, with the support of our sponsors. To find out more, please visit https://ethereum.foundation/

Transcript

[Applause] myself and videos so I use this decompiler saying that when it goes to the website in the contract name and put together this for almost every contract the source code that is kind of human readable which i think is a new thing because they weren't that many compilers that could allow you to create sources like to view the source of most of the contracts and I really build this whole thing out of frustration with either scan because it's only like doesn't allow you to access all source codes easily and a lot of source codes are not open there so I said I will just beautiful compiler that anyone see any source and it will be open so anyone can start their own thing and work with it a little bit so so that was one of the main innovation behind us so you go to the website and most of the constructs you see the compiler right and the second school thing which is I think even cooler is that for every contract there is this intermediate form so this is the same thing as this but but it is alright you can write the others all right so so anyway there is this intermediate form which is quite cool because it's I know that it's looks like gibberish but this it's really a Chinese 100 percent every single contract out there and it's quite nice because the way it's constructed is it's constructed in such a way that is very easy to analyze by machines so we can write very simple merciful analyzers or source codes and you can get like you coming you can do a lot of cool stuff that I will talk about it in the end do it so anyway again the decompile forum and this right and there are of course other tools that are yeah that are in the same thing so there is mention for example that that is doing symbolic execution of every contract and and tries to figure out what are the potential backs there right there is magic or that does a similar thing from from 12 bits and there are some other decompilers but they have to solidity and I don't like curly brackets even though here also what I am that's anyway mmm in this in this quick talk at workshop talk a little bit about what symbolic execution is because that's the basis of the whole compiler and that's a basis for a lot of security tools and contract analysis tools so I will explain how exactly it works and then I will explain a few different things related to simple execution and how various tools solve them so it gives you a better understanding on well essentially how these things work and perhaps your own thing or or the seal those things better then I will talk about some crazy stuff that I have to do to make make the results so pretty and yet I will show you a little bit more about the broader context of the whole like the compiler slash contract analysis space I think it will take care of I don't know an hour probably and then we have some more like a lot of time for questions and answers and more products that one atmosphere and all right so symbolic execution how many of you know what simple execution is alright alright so so they're here with somebody education is that we never like we're securing your honor it's always the beginnings of the presentations people coming in now so you have the assembly right and and you have the Santa code and the beautiful machine of gear you works by executing that code and now it sees I know put something on static and then it pushes that thing on the stack right Linc's Pulsifer static and post on from stuck and just executed comment by comment right and that's how the whole information works symbolic execution is essentially the same thing but you don't deal with complete values so you start the program and you know if the program says push number one on stack we also have the static and English number one stack right but if the program says food call data or some something that you don't know because you're you're not writing an actual transaction you push this this is variable or this symbol on the stack right so here for example this function has access and assembly come on same core value right so it wants to push cold value on the stack regular virtual machine will just push that concrete value that was you know value on the call on the stack and my face which was just you know we try to the stack there is some value I don't know it is just I push it right what happens then is you know there are other things that operate on the stack so so easy o command for example you know grab something from the stack make it sit and then puts it back on stack right to put swanee there is if it's zero and it's zero there's it's anything else so we checking our virtual machine it's easy because you just have regular arithmetic with symbolic virtual machine you have to you know abstract especial expression and you would be put on the status value saying oh is zero compiled exam right is this kind of clear because I don't want to know some of the people that I want to be I want to be dressed so so yeah another example here and you know pushing this value on the stack so now we have stacked with two values 0 and 60 91 and then the fun part is when you have jumps because regular virtual machine might see something like this damn right it just checks what's the value of the stack if it's it's higher than zero that it makes the job it's zero that it doesn't make the job and it's quite straightforward it just continues execution but when you are running as a bullet execution even if there's actually more to help you toward machine and now running in parallel right because you don't know the jump is performed or not because the knows the finalists a because it's easier kabadi right so it can be anything so you have to kind of fork the stage and then execute everything below authenticity right so so you're just you know call here and Frankie from this month on right so so you kind of executed the execution and yeah if you just execute one line by buying enhance and at the end which is oblique at the calculation whatever they do to erase whatever it is something interesting to the user that changes the state of the contractor involved require receive this redefine phone right so if someone the contract rights to a storage somewhere to the storage and all your eyes it's just removed right and well the decompile code is really like this trace of execution of the symbolic machine and and that's wrapped it so I know there is some kind of storage right right and I just write you know right it's the storage and that's the part of the program that actually gets up to the user so at the end of the second function let's ignore it is we had fight a series of ease and we went deeper here so so we not perceive the receivers so this is the new copilot form so essentially I just executed the whole program symbolically and I quit about all the storage drives all the eaves of rebirths everything and this is this is it right and to ease to build I started that by the way I absolutely no idea what I'm doing so I just grabbed the crypto keys my contract that I said I will don't know of going out there I didn't know that it's called spotting execution actually so the problem with this is this is doubtful that you will actually see on some of the compilers I think recently other decompiler this society like it is way way simpler right it's just yeah the function is really much much simpler just the executions of so many paths that depend of speed here so there are other algorithms unity it's mighty compiler that emerged is right later so the whole function was like this so we went from assembly code everything identified by I so this huge tree of execution right and then we called it is something much simpler that's the function yeah [Music] okay it's it's difficult with the slides I yeah you have to come cause they're sorry because I cannot like on three do decide right now you killed stole like you have to see it yeah there are some I didn't know yeah so the other thing that that is done is for any contract that you figure out all the fashions that I can figure out what are the other factions for some storages and based on that I can say oh this functional internally storage dysfunctional name is Diego address so so this storage is my CFO address and then I end up with very nice code that just doesn't care right that's readable so that's it yeah that's mm-hmm that's like the outline of the compiler does and how simple execution works and then any questions here I will concede what proportion of the routines you have to collapse into smaller oh that's like I noticed solve an immersive South Korea in England war on the polarity looted class like I would say most of them had some kind of things to the to meet collapsing it's just like super nice super nice experience to work on this folding algorithms because some of the functions usually were less of screens and screens and screens in land and then you write it with algorithm and they fall to this so I yeah so it's not Q by okay I'm street I was gonna ask how you handle area stuff that Pfeiffer doesn't normally do yeah so so in general like that's a question of commonalities and you think I'm part of something that can be recompiled and feely like it's very hard to do something that it's not just some kind of a pseudo code because exactly the stuff that like either a viper or sewing it easy think of like it's hard to really compare to something so it's just yeah yeah how do you do the mapping for the function names and the function identifier I mean they're there libraries but you don't know all your function names I will talk about the baldhead all good quality morally the same as optimizing no I mean that is it like correct translation oh yes it is yeah what I mean where I'm having with this question is you weren't partly on the youth talk by saying so they have this intermediate language high cap and it doesn't seem you know to hide ever but what they do is that they have this optimizer which is like collapsing greedy and also stabbed right and maybe viper or say disease not the targets for you know this mighty you is yeah I think it's always best to try and work with existing tools right I mean that's an exerciser I mean I use people switch to my intermediate forums it's like they got 15 play yeah okay so those two questions will be answered later on anyway so there are others willing execution energies and then sort of them and we can both get solicited for Gant about about other teams working but like two significant ones the team I doubt it though oh no thanks material from consistently a chance right so they use a very similar process so whenever you have to work with material like you know they'll be that's what they do that's what actually does and so we execute the whole cold and right like one of the things that we did our strategies say execute the whole called symbolically and then month or from trade trade of beads they in do analysis verification of the software right and they use very very similar problems to the mother I just described so they execute the whole program and and they just volley so if you understand this about execution part you really are like you you really understand how like the most significant tools on the market right now right it's worth spending some time to work with that know somebody game is between is like this is the double dating right and there are few super super difficult things most of the tools don't so properly sometimes either one of them to sauce and I would say of I don't know eight months that's like eighteen time working on this whole thing I spent probably half of the time doing memory handling process explosion that was this folding thing I do that in an afternoon but it's like I don't understand how it works something good answer so a little bit about Memorial and me now and then another processing and then move to they're like tiny things that we have that you asked about so when we are handling I told you how somebody execution engine execute the program right and it's easy when it's just I put somebody on the sky to get some value from the stack there's some APIs plead to stay don't but what happens if someone pushes some variable of this time and then try to rights to the memory to the body right like the question is I know as long as as you write to program rights to a very concrete number in memory so if you try to do the number I know 64 right the virtual machine can just say okay at the end is 64 there is this volume right later on or operates from 64 it's just this value and executed right that's that's very easy you'll just create an array that represents the memory and you just try the question is what happens if the program takes some unknown variable I would say X or whatever it says you know right to this memory at the position X right and then it says read from memory position X plus 1 and you have to figure out your whole execution and who now has to figure out this X plus 1 is really like what's there right is it the thing that was written in X and just move slightly awesome like perhaps overwritten by something else like how how do you deal with that and quite quite a difficult challenge right so you can imagine for example and are very cases the program says write to the memory position eggs okay so you remember that there is something at the solution X and then it says write to the memorial position 60 bar so remember the 64 right and then it says read from the memory position X but you don't know if 64 was X so this memory was operated or not right so so you make its target some somepony and it's quite like seriously difficult challenge so I looked in January it may perhaps they improve it at material so the poem it really happened it was a true gentleman so again perhaps they tasted like whenever it reached some symbolic memories so memory where it was written in just know so some variable which I'll get out so that was my whole execution and then okay super Maria I give up I don't know I think next action please and that's why you didn't have a full coverage and mr. Elkin tanks Manticore what they did was and that was a very similar way a diamond ring in hand with that is they use like some very very like complex structure and SMT solvers which which help with the kind of managing this algebra rights also assembly solvers help you to figure out SMAP signals roughly so so multiple rhesus SMT solvers and has this complicated memory structures and I had never begin to the problem was that little bits so many times and I think Manticore and the second problem was that sometimes the programs get so complicated that we need them that doesn't cut it so I spent like two months rebuilding the whole memory model to it all right that that's something that I will show you which is I think we need so okay this is the demo time Can I grab a char yes all right they are not locked so actually open source TV two days ago so any one of you it's an MIT license and one of you kids we can see it and you know if you might sell the sources are testament to the power of duct tape engineering and Kowboy call being like the best practices in those those if you're serious programming are all implemented so it works quite nice but it's being battled us at a lot of times so it works quite nicely you just you know typing the contract name or a short path for crypto kitties you can't be compared so it is around eight seconds to become pilot fully which I think maybe like it's way way faster the manticore it's around the same speed as as material so anyway you get does the sources everywhere like for all the contracts right but now this time I implemented just for dead calm if you fetch eating from from github you have this parameter called explain that shows you how works exactly and I can increase font size right so so I have this one pension and this is what you saw with the previous step right so so there is assembly there is stack and you can preview stuff that is happening here right so so we have here push right and then you have memory load and this gets stored this as something soaking up all the assembly right it looks like this whenever I encounter work whenever EDM encounters a memory read it doesn't try to analyze it at first so it just pushes out to the single assignment variable oh there was read from memory 64 like I don't you know like I don't care like how exactly it's tied to the rest of the thing it was just a memory to memory 64 it's number one variable number one whenever it uses them this memory just puts into the code underscore one so that's that the first iteration that comes out of the initial depopulation process and then what it does is sorry I get a little bit so yeah what happens then is you toss in a loop and in a loop it tries to optimize the whole thing clean it up simplify it as much as possible and in case of this function for example first thing that it does tries to inline all the variables so it can see here you know there is variable underscore while it's being used here so it can mean like it so you can put it here right easy now it doesn't put it here and then idea why yeah like it it's a like there's a lot of things to analyze when you want to invent something so this variable and being like here because it doesn't get overwritten for sure in the mean time right like for sure it's not overridden but here right now like we don't know because perhaps this this overrides this this memory right so I will just put in memory 64 like it would be incorrect because memory 64 we would mean this power 64 this one right so so right now we told the algorithm so for the way it goes is that perhaps everybody involved and then post find by line and tracks if if the value of the variable was overwritten in the mean time because if it was potentially was it has to stop the process is doesn't inline anywhere anywhere further right so this was the first step it went all the variables inline them wherever possible and and then the next step is of course in lining all the memory the same process right so it grabs of the memory and so it grabs this memory and first this memory right you can put it here right they also sees know if thanks everywhere where you can put it and kind of we have it already something that sighs listen there it goes like this in the in circles and also tries to simplify it whenever it can the whole thing right so after the next iteration we don't have the variables here because we we could finally no replace this with this because this is a complete value then you can simplify things so it also goes there and tries to figure out what are the expressions that can say goodbye so you can see here that this is 96 minus 64 so it's 32 then it sees that ok this program vectors memory many 6 32 bytes so so this is essentially is so you can also put it here and then ends up with this super super nice very simple thing right so we went from this complex thing to this very tight in one liner function and like it's super rewarding working on that becomes a header by the way because like the way it is it's like almost entering this crazy battery room or whatever which is crazy crazy huge function and then you you see that the compiler simplifying a lot of stuff and then you try to figure out alright what are the other rules that are not given to the system that I can implement correctly speaking and that would also simplify the program right and because because helium is so so fast like like a like a festival on thousands of contracts so so before every release I can just look for contracts that were it simplified enough and just find all the missing rules and try to simplify that and just in a work with that and end up with something that so one more thing that he does is no I thought you about this intermediate form it's also quite nice because it's it allows us to really analyze the program very well so you know we took it just a few moments to write this from a figure out what kind of partner what kind of stuff can definitely terror right so we can see that the function returns this story for example right it's very simple to see if the function is payable because we'll just check if there is a require at the beginning looking for that we can check if the function is resolving because we can see if it gives us some storage rights or some calls right and if we have all of those things we can figure out that this function is really a gather so it returns only value for a certain storage in this case storage too so we know the name of the function and we know that it's read-only it means it's together for a different storage so we can figure out o this storage name is we can name it after the pension and it's okay right we probably more or less correctly that without you know okay that's right any questions yeah also there's like a meeting on edge cases right so negation is one simple thing but then actually for bully hacks I you I already put that for very specific action names because there are so many for such cases that I usually don't think storage factor the bullion's example will sometimes the bully has returned already in Texas of our eyes so because there's a factual code are there any focus right they try keep the tokens size is higher than zero so I cannot really name the whole storage are there any tokens the storage thing is to be focused right so so in this case before anything is they like very few cases where we're actually it makes sense to name storage after and after that well it's funny that people ask about the meanings and the patient's because like that took like the least amount of time the whole be compiler I remember teaching soda really like you know first question people ask and that's what this is pirate master anyway there's the second part and that's the move processing and I I don't think there is another tool on the market correct with like there are some other people from other other other security things but I don't think there is at least an open-source tool that actually handles looks properly that means that the last time I checked either a materialman car or another I think the compilers figured out loops and I will show you what they mean so the problem is we have some kind of a semi right and the way it works in virtual machine right the code that is a loop iterates over something in solidity because compressed to get some ties to this so you know put some index jump if the synthesis bigger or smaller than 0 right and then subtract come back and just go in circles so essentially this is now when we do a Samoan execution the problem is that if we don't discover what the books are we'll just see a series is so we'll just see because the 0 increase X x0 decrease X and just go and not be deeper into that's all as well continue the execution or whatever right this is super figure out it was following do you figure out oh this is I'm really in a loop like I'm just throwing you know I'm executing the same code it's not as simple as figuring out that this equals the same line in code because sometimes for various reasons but you know turning this into something like this on the fly is really like seriously explain exactly deliberately because I don't fully understand around there but it works I kind of you know like the craziest stop by every row because I can understand bits and pieces of it if I hope is very hard so I think I know that I know that it's correct but my mind that fails to grasp the whole complexity of what's going on there like I cannot imagine it's go down there but anyway it's turn here and I think some other it's going to look like so they don't handle this at all so that's when their place will where they would right so for example they will just go deeper after they experience a timeout and they will say okay I give up I don't analyze stuff and occurred so this is how the reason why I think again half a year ago with me that Manticore they couldn't they didn't make this connection to drive here so I will not explain exactly how this works but the sources are public if you can clean up the code and understand how the concert explained method and then I go ahead and appreciate that it's possible that perhaps it is but after the first iteration then the comparator figures out much you can say but there was some kind of a loop here like the program encountered so some kind of a loop and there was this one he takes variable that starts with zero okay so this was that in this variable and then who's this here the hook through the ends so degrees and gets back here and kind of execute and then sometimes it goes these paths so essentially against the program so far unreadable right so it's it's hard to understand what's going on here so after the first stops that's that's what we end up with and then crazy awkward like terms or to not send it to something like this which is still not not nice enough we can also hear out pay this is the condition because if this doesn't get fulfilled we continue and if it does there is some other program for the repair nobody is here right so so this is a condition of the road and what we can do we can do is we just look at the program and you say alright this looks like the wire loops we can replace some of this with something simpler so there is a wire here right continue and then the rest of the program so like this is relatively simple compared to like the blue protection also shows all the power in just working and rewriting the whole the whole the whole the compact program because if this for whatever reason fails like they say is that we end up with something like this which is still kind of writable right so there is this graceful graceful graceful degradation one when then the compiler fails to understand something right so so we you know and again inside the variables we can we can again convert into oh yeah so we unite variables and then what we end up with is this loop and I know the text is barely visible from there like for you know like might make you slightly happier if you are in here iq them understand it's very well show there's many letters anyway so it doesn't really about so the thing that you have to believe but there is this will is really a memory come you look so it what did I see it copies this memory from this index this memory in a circle right so now the compiler it sees it has so the pattern is that it kind of recognizes have been let's say it could prove but thematically that they're really remember loops and they only think that those hoops do is just move memory from one place to another so of course it can remove those or better and we end up with some is just a statement saying copy this memory in this land is this memory to this memory and you know like the goal when I was in the other was really to get rid of all the loops because who knows make it's crazy difficult to analyze nice smart contracts so you know like I think 495 thank you 9% of the loops we can really replace them with some other statements that are very easy to to analyze with to analyze with other other programs so like a lot of statements was removed and you will not actually see loops in the output code even though sexual okay it's like there is no solidity head loops so so it's simplified it even more that weren't enough but if this is still not really low enough like this is some crazy numbers and whatnot so we continue all the united reading so we can have variables you can see us text okay after some more learning you can see more text and actually there was a lot of these decisions here because sometimes like what they would say they're simpler but they would still more human readable where should you stop right so my idea here was okay I want to unite everything at the start like you remove yeah in my everything possible rings all the loops and then kind of just for the human readability and clean it up and perhaps add some variables here and there so it's more readable and yet it's kind of different from many compilers that that's just yeah so anyway this is this is not the best again this is the same code now it recognizes that this is really an area return statement so this oh this could be really represented by s so this is kind of adorable still not not as well unfortunately this is the best there is but it's a part of this function and the bad thing is and I can honestly tell you that I think it's not just amazing the single faction I spent probably like two weeks full-time work if not more I was you know almost making up screaming at night and saying ah God the world needs to know how simple dispassion is because this other contract and repress whatever this contract returns so it's like this shouldn't be here it should be not return this what gets returned from this code this should be this release appear oh really and it should be like four lines and you know the problem is that this single function actually breaks under certain visions so if I just put this right here like a like I cannot simplify further and maintain the correctness of their program of the translation like you know it hurts me so much and simpler but I would lose this correctness sorry on the outside what it means also is the very sick cool thing about the compilation processed the way it's perform right here is that sometimes infections don't be compared correctly that means is that really you should look deeper and figure out what's going on there because perhaps you know there is a reason why it wasn't simplified perhaps just by certain rules but perhaps there is some edge that if that's there that's an expert for profit as a back-end know it's all about giving better tools to blackhat so they exploit contracts sooner so you can use less money but you know if it's probably contracted $50 then like people who know something else right anyway the cool thing is so this was the original function right so it really is squash and very simplified and again super rewarding process when you see this huge juice function you wonder what the hell is going on here and then you end up with something that's almost as simple as possible yeah so here hands like the question is when an amenity compilers to do systemic analysis thing where they try to figure out they kind of try to look at all the compiler leave use some of the hints to speed the program into trance and then create a graph and try to work from that graph right so I think that's what these do and here I I don't do that I try to avoid any compiler specific patterns like looking at comparisons figure patterns and often you know this come from you oftentimes you know assumes there are certain things on the stack or the very certain structure and here there are other things are easier like this right where the programs were much more context [Music] agent Ranson although there is a part they will talk about in a moment where I try to analyze this chapter of the storage but that's mostly for the naming purposes but but you know there are there are no assumptions about what the executive storage structure or the sort variables are at that point but I think that the output could be then analyzed and like some cool stuff would be would be possible there I hope that this answer is the question I noticed in your out there there's things we're like you have storms for your player and ask address right yeah and it's like have you determined that sort of thing okay I would look up all that in a second okay well okay and that's let me ask the other question which is where do you think is it possible at all were you good an animal like jumps to like a variable location save women from storage that's that's one of the benefits compared to the control yeah this actually handles handles this kind of stuff quite smoothly yes because like you executed actually that the current version is not as smooth as the previous one but but you actually you know you're just executed all the jams and whatnot so like with other tools that are more in line with with static analysis they oftentimes the lost or the respective prefer results when someone calculated the dark location or the knowledge I hear it just calculates it also on the fly right and exact with you know proper jams but the question is what happens if you like a some good examples you like from the other compilers but anyway what happens if you jump to allocation from the storage right so yeah so right now the way this handles it it's does well it will just always talk to a storage location of another all right I don't think I'm encountered do that actually yeah I mean I don't think it's a common thing but yeah I was wondering it's like you can't do that in celebrities so you can this summer this one one example no yes yes there are other examples that are closer to that for example dark tables right so in my current quarter break but interpreter yeah yes so this approach can be used to have a laugh and original products are used it's quite nice to go and get some Java patients in the memorial but not the current version doesn't work with them as smoothly but you know it also needs by together as a pumpkin used to the end of that I kind of try to work on the examples of real contracts but keep in mind know if there are long contract that engine sputtering then again it can be extended to handle death as well there was question from here right yes so you have like a bunch of girls my sorry you to think carefully about having over all that baby stuff southern Oklahoma my name is the real implementation and by applying one to greatly doula take the pattern on match yeah I was afraid to go into this kinds of roles because like if you simplify a little you simplify to write if you had some other role perhaps it simplifies to something that brings the other girls turn so fortunately there there were that many cases of this so so somehow it works without putting these products there were some cases but then you can you know steps so it's not like I will combine the pros where is things figure out which part should be by which they do some we evolutionary algorithm something on top trying to pick the family or part and they can combine English maybe later attributed by drizzle fury maybe I mean I think what happens really is people just use dry and embarrassed by pedestals and see which one's the river the best outcome for a given function and what not so so I think that's that's really good like the practical practical mystically it will be cool with this this approach like the way I implemented it at least like it's really like it doesn't work well with the state exponent but but there are like there are ways to make this approach work just as good even in these cases I think that from your perspective maybe not I did not work or you can fill out of work whether you can manually like compiler to another yeah yeah because I think you need to integrate into policies it is very compact yeah it's very complex so there are other things that would be more able to do you know yeah actually happening well there are a few ways actually at the energy perspective that so or I will get back to that yeah you know in a moment as well all right okay okay I try to remember everything I thought the president didn't come so like a lot of things tonight okay so one more thing that they wanted to talk about before I come to the part where I titled it answers to all the questions over here I mentioned already the Jason with your presentation at the beginning and first talking about the table like why these or someone else would make something very similar it's very very cool so like the cool thing about this series of small letters that people from the back don't see is extremely simple life so compared to just you know grabbing solidity or the stuff that people do hello this doesn't have for example recursive functions or anything like that but usually kept loose doesn't have memory access this is almost a functional representation of every function in that you can use smart contracts and this this makes it very very easy to analyze by ultimately ultimately tools so so there's a lot of cool use cases of order trying to know that all these all this in in a big query database so we can search it with JavaScript even a seconds and there were some cool use cases so Constantinople intensive greedy when there was the content they don't perform for example the question was no some changes in the protocol may affect some of the contracts but how do we figure out which contracts will be affected by some changes we need to figure out we need to find and search for that right so the way you actually found contracts that are really affordable to a certain exploit was by grabbing on that from the database and searching in JavaScript all the contracts that mattresses in pattern and I think this was one of the two tools that actually managed to do content of them without help and cooperation with a change cleansing vehicle so so you know a huge potential also for by some other stuff that it was finding all the tokens that don't check transfer function properly and allow anyone with that was like five lights of JavaScript to analyze this thing and there were like hundreds of contracts where you fit their own vocals because they must have decoding those skill areas if I put them actually valid contracts that someone had a smart young so I have to try before releasing that if they are still online so there were some like the sad stories you know don't use this concept anymore like this this approach each other of the copulation and and this intermediate forum and working like this like rewriting the code it's very important for auditing and I would say that it will replace solidity called auditing in full because that gives external memory still but really working bottom-up and taking the virtual machine and and just monitoring it this into some intermediate form language that has a lot of benefit and also make very various tools for auditing and I would see not necessarily might be paying and if you check the sources you will see one of my English but it's something like that I think that's that's really mad for for the community to go we support of the Northern Pass they mean like level girls like I know this one election looks place murder that reasons like I didn't know that one okay no I think it's yeah was like with the original course that because it's very less being less kinda like this actually yeah like felling off in the less doctor after I died from her that's very very Somalia so so so yeah I like it tomorrow was the world so I have to take it out yeah I would about one more thing before I get to the questions okay that was supposed to do anything okay one more thing so there is a lot of math going on there in every compiler organizer store and most of the tools use the same two solvers so this black boxes were including mathematical results and they're very nice because first of all they are solve enterprise like they've been written by smart people but they listed for a long time and they cover all the cases so so they weren't very nice but I think surprising really like telling a set of rules that were handwritten health problems and other problems but can be sometimes faster and and I want to talk a little bit about how math is handled my case crosses a comparison and I'm not saying this is better perhaps it's worse but I just started doing this this way because honestly a year ago I didn't know what the second servers were so I just throw that my way but perhaps it's not the best way so in my case I think that I don't buy information like I don't use passes for represent a representing a long program when you stop us so this is very similar to like actually like the way these represent so you know every operation like if I could on the stack I don't know the value it's not the class of something is in just a double so that is are so nice because they're very easy to compare for example so if I want to catch some computations I just know like like it's it's it's very like in Python at least it's like one operation to to compare two doubles if they're equal one time so it spits up a lot of computations because I cashed like like crazy the second cool thing is working with this is I have to print out form that's human readable but when I want to test it in vitam I just pop into the code it's already there so I don't need to create the contractors and whatnot so this is very very nice but but sometimes like when they are getting used to that it's you convert your eyes now the other thing is I also try to flatten and say goodbye all the forms of expressions so I think solvers also do that so I can simplify stuff but I have a very special like canonical latin form that for a human it may not be the same as well but but like a lot of math really assumes that there is this form so it's safe so the processing time is not rules I don't want to go to duty to that but for example now when I multiply something the concrete body is always as a first argument or there is a certain order of operations so if I see multiply something multiplied we always are moving like this and not the other way around so because of this like the whole math library can we have like a certain very small set of rules I've analyzed of them he doesn't have to worry discover it involve the whole yeah and he's faster in some cases the cost of generalization perhaps and then I have to invent my custom operators so anyone that worked with with the bytecode knows that she'd left happens a lot of times in the contract to I shift all the staff and move things bit by bit by quickly by and you must get out so so you know let's say that's going to be number you want to top of this center here because that's where some something is and you move it to the left or to the right right so like these operators are used a lot and I simplify like also like I simplified all the multiplications divisions first these operators so the local stuff would be way way simpler and special operator mask and shift left which is like super difficult to figure out understand and memorize but through the like please so essentially essentially this special operator that was invented that handles a lot of operations that otherwise would be dis complicated threesome expressions and I think that's another part were worried about where the compiler gets its speed because between Acastus one operator words the regular analyzers have like a huge tree of operators and they would have to figure out your single time together I'm not 100% sure I'm not like a safety specialist number like this stuff is fast so so uh that's my bad well that went way too soon now obviously yeah this is no because it's home homebrew like the code is absolutely bad so we kind of the factor that we like and yeah it's for them like all the rules or the match rules were really done a testicle on all the contracts on the maintenance so so really like it was a very quite fast and cool thing is that this kind of transparent compared to ANSI developers which are often this kind of black boxes but the code quality is so low that admins read so transparent and yeah okay the next slide is the answer to the questions hmm so I'm voting in Python and I thought doesn't have pattern matching at that size because a lot of the competitors is three pattern matching so we're trying to figure out there is this pattern in the now they sit with some other brothers so for anyone that will want to try out the code fix Python and in custom statements until and then you know best programmers know that this is not what you do usually right they don't change the language to match your purpose like if you go into the sources you will see a new operator that sexually pattern matching the colors but imagine quite them and they wanted to do that without fixing the interpreter so you just wrap around plain vanilla item three one day and you can this pattern matching in your own programs so that's that's why even really simplifies a lot of things why don't we point eight requirements for this services next week they didn't want to move Thanks so we have to wait released anyway yes so now it's a few answers finally to the questions then I will talk a little bit about about the other tools and then we have a more relaxed way I guess some people warm with impatience so yeah first of all there was a question about the national identifiers right because there is this so the way it works for anyone that's familiar solidity and and the whole like VM or the contracts use identified night runs by four bytes so you take the function name give a and you grab the first or bytes of the hash and the identifier so that every contract as dysfunctional and only those four bytes as an identifier fortunately someone with the database of 4 bytes directory called so so it's kind of you know it has all the function names and all the identifiers unfortunately it's not that good it doesn't have a lot of staff and some of the I think someone brute forced to fight collisions so you can find a lot of common passions that just have other definitions that are total rubbish so I had to build my own my own format directory especially I just grabbed all the api's that were there and I absolutely hate spray painter stamp and this was the only one situation that they had to do that so I grabbed all daily is I use them the box and they beat my own directory so if you download the sources like on the first round it will download because it's a huge by little it will download all the other formats into into your drive SQLite database so so there is anything like if you're playing with contracts and you want to have a really good library of function definitions that's that's for you so like the taste I love these transfer function transfer transfer from because success like if the modern things were completely different like that could be handled quite easily right but in case of transfer the problem is that Erie 20 tokens transfer the first second parameter is value and air system Antoine is item number or token number 90 right so it's different different names and that's quite irritating because there is no way you can figure that out from the source it requires human not so that's why the fire which provides directory like the way I know that is so weak I kind of I look for correlations so I see oh this is the function usually abuse me these are attractions and disappears because other functions and then includes which which are more similar and tries to guess based on that - that is great this would submit everything to you all right not at the same problem and I perspective I'm actually trying to view more tight title arguments I see and then yeah so okay yeah yeah I like really like this this project of frustration or interest I'm not providing the idea it's like we were so dependent like it was all the contracts published on Facebook like people will be like pitchforks right now all the contracts are on the private companies several brands that don't have easy access and not these ones so I kind yeah so again thank you and he said all that the pension doesn't work properly so I'm actually done distinguish that very well it should be approved like it could be improved they died is they're just not active kind of that there's other good thing or interesting thing that when I decompile are trying to figure out the storage Isis the storage where when they have to access arrays or or mappings it's like you know a cache of a number that's something right so when so DD or like contract once taxes are a number are a storage number two something it has to manage number two and add something right so usually I just see you know hash of this had something that's easy understandable good unfortunately in some cases like the compiler and the Machine advanced everything so it was of course a big number there and if you know the output this big number that breaks everything and breaks understanding of the contract because you just see read storage number one right super irritating so I do do a rainbow thing about that so to speak so I just for some courage like I just pretended some of that so so I reverse engineer at fashion I just have called the function reverse reverse 883 right so that's the thing Thanks yeah various other is the contract search so I can put all the data there of the inquiry another fun thing that I am the hackathon I probably will really release that sometime tomorrow next week like I actually indexed all the contracts and this instant search for contracts so we can sell contract by coordinating so it takes like a hundred milliseconds and you can say only contracts that don't check for owner who is calling them before clicking the owner instantly spite of the contract right method and it will be super fun to raise your hand when I release them because it's like you know you're like I want to write this prove that just checking just contracts owners of you know contracts one another and we know that you're responsible but if someone does it that I think okay okay so testing how I estimate whether this whole thing is valid so first of all if there's no body like don't trust 100% a doubtful that it provides that you know wants to keep them brief like no drugs but both finding parts in the contract doesn't mean that the contract is fine like again involved I'm quite sure that the approach is valid and again focused you are working on a very similar thing because formally verified so I hope one day we'll see this approach but it for my verified basis or like very very solid so folks who are really interested in that thing heading said that the way I destitute values I have a few cases so few contracts with edge cases crouton Jesus is always a must for me and it has a lot of nice edge cases and just few basic constructs that I check how they compare between various versions of the compiler and then the second thing I do again I pushed for speed a lot right so I like it's possible to become buy the whole block train with invalid one day I think right and go so cryptokeys takes eight seconds it used to be - like really imposed a speed so so for release or after every update I can just go through campus of contracts and kind of see what's changed or or see some patterns and it would not and also when there is some new stuff I can I can say oh let's throw me some contract that kind of certain pattern and that's they're so so it's kind of you know on the perfect testing mechanism but but so far it's it's been kind of successful like the idea that both standards would be to have a recompile from the decompile source right and recompile all the decompressed contracts run the whole block trading history and then see how correct it is right so the transactions return the same thing and that's it so very nicely how how you know how much of it is is correct like most of it perhaps again not on the educators but that would be super super nice mmm and yeah this is battle tested so if you get the guitar source like come online I played with some other tools it was like oh we have to download this binary and it has to be real runtime and then you ran it and there are some bars like really like the common line is a simple and it works as smoothly as possible assuming they're quite a few more time so that's that's the problem okay I won't commit all this much storage but there were a few questions about storage right so so can you repeat your question okay you know yeah actually yeah I mean I feel like superb so this is not super because I mean they're not gonna need like the numbers that are getting plugged in are fairly small so you know you know what your range there is you know if you you know if you're not you see enormous array of it and then you know maybe you this be level down yeah but then there's mappings and that things you know you could maybe see huge numbers put in or you know you know the domain doesn't have to be numbers in numbers that's enough to expose developments but I was I was wondering since you didn't thank you Matt is there no problem bathrooms because they don't pre-compute informatics or do they pre-prepared imagine that you have to expand your technique unfortunately fortunately usually the like there are mostly dead okay usually you might want to do also it's not being similarly you know they have to be completed them to die because the mapping depends on song is or whatever right but sometimes yeah I noticed some contracts for example notice storage number two they use the person from decorating just plant a left but they have some proxy contract that the college is storage that doesn't have a number inside like it's not expect number about the tree or the sentiment something has that right so so in that case I also cable I think one or two cases and the cool thing with working with this approach is actually what I did was I was I was running the decompiler and saying okay show me all the big numbers that are used the storage in cases that are not yet you know reverse engineer you know I took a look at some of them so this is very neat working in this way because you just say okay let's see what what I still didn't take into consideration right and I'm not saying that this is perfect like once for a lot of things and it's easy to extend my service when there is a new pattern you can solve that I think yeah it starts working in turn around some crazy stuff there if you go into the source code of this like that's was done right before the release like you know you don't want to imagine my mindset when I was working on that but like some crazy gangster but essentially like it's very difficult to map storage if you want to become packed properly you have to figure out this storage is no storage number two it's an already and this is the apex of the RA and this is really a structure ER I would not like very very difficult well it's kind of been solved so if you want to see like I would not even attempt to explain how it's done but what it's done and not perfect but the alleys I asked you about the open challenges to 312 well okay I will briefly mention the folding algorithm so I told you that there is this pain exponent like you have a lot of these and then you want to follow them so so it's really like a very short thing so I will try to expect algorithm because it's it is like right next time so you know how you have leaking like a deal between two files right so now the way I do it is I did called execution paths I split them into linear forms right so I do something like D but for not 42 but like 400 time right so I married that kind of a tree and then I do it deep on the trees more people trees inside and they kind of work them together so that's I dunno I I cannot really like imagine how it works exactly what's it's roughly that so so the code is super handy transparent like if you can figure out a nice way or if you can improve using some knowledge from the other from the other fields go ahead and yeah so finally a few do and now I'm getting to the ctmc so this is the edge cases first so there is not that much abstraction of don't try to make the code that is unreadable that's much I found some of the code that was super easy is big powers that obviously enforcement is some kind of security practice and some other code was used to you can block some of the money from being with robot so like that's not been good like security possibilities not removed long right like from practice and I wanted to say when it comes to CVS you know I liked when I started tracking yes I was kind of sad because he didn't work well with yet and then it hits me perhaps the CDF creator so you have to check with idiom before releasing a CDF I hope they knew by now right so so I'm not that sad anymore because I think there was this guy that had to check for that and actually I spent a lot of time some weird edge cases thinking about guy that will be doing a CDF one day even think that he's so smart and then he will solve it smoothly and then I will in my mind say to him in your face right so so I called there was this mass situation where someone trying to create this Kiev and and there was that in-your-face moment we're going smoothly so anyway that's that this is the air time and I try to not spend too much time on them because like there's you know difficult right yeah so Castro I'm giving a as a cooler because they're doing awesome thing and very few people know about them so you Larry if you had the chance yeah that's that's Ari so they like the holy cities about programs in the society created 13 years ago in a mystical Valley and they did very soon our staff does way much better in delays i co2 for my oven and it works for way more difficult started smart contracts so for java programs right and yet and for for cryptographic libraries and and i hope that they get the grants or not 3d 3d push that into into our space second thing is concepts library so it's not everything on fire I love the guys their website looks like crap but it's really good underneath so in theory like it has about some technology underneath like similar in spirit they just use more declarative languages so so like if you want to work with like there are very good guys material I mentioned Authority like perseverance period and very nice penny laughs so I guess most of us know here okay laughs and promote verification and and stuff that was done around maker like the stuff that is symbolic execution and the stuff that they are doing kind of kind of similar in spirit against so if you get small in execution it will be easier to get what Caleb's enjoy although I still don't get it fully semantics are fails bits again now shops will be queried because it's like I put all the stuff there and should be there is a theme from bigquery that is very much into blocked any material and they are very easy to eat so if you want to play with required are people from Google that that's really you know that and there are two cool volcanics polymers proxy for and by Alex Lee like a lot of cool data analytics and whatnot very open to go to cooperation and it works I'm actually talking to box count and there may be integration so they may show sources from eating over there because I think like the problem with eater scan is that they there are no he was on a diffuser that that don't have the function the content resources and gather sector scrape from them better decompile sources and of levels the ground because other books and explorers can also show sources for Oregon's highly trained security I can see the t-shirts here yeah thanks a lot for the convention heading into the very article but also like very good part and also very good project and yeah that's why I think I think that's released next week so anyone can production so I want to say like a few words like what's what's my approach with the project what are the next steps so really like I mean over the last year to a separate outfit so to speak so I just wanted you know I was frustrated not knowing what the contracts do it was filled with anger like a lot of anger just put into this finally together now and there was no business purpose there there was nothing outside you know I did of course some time to just go deep and see how how far I can go with that attendees and all that like I kind of accomplished in this aspect so I hope that the community will use all of this knowledge that can help other projects really with with with adding some some better stuff to the blockchain and yeah that's why I'm super open about the MIT license anyone using the algorithm month but for me the purpose of the whole project is accomplished already and you know I'm happy to see a broad here and I'm happy to open you know answer any questions and just help out over again and yeah I hope that someone will reuse the sources so yeah thank you [Applause]

Automatic transcript — names and jargon may be misspelled.