J1 RF 02 Casey Detrio fuzzing

I'm Casey I've helped a lot with the theorem jess team so last year getting theorem Jessup to byzantium compatibility where Byzantium was the most recent fork and I also helped a lot with was testing so using fuzz testing to find all the consensus bugs before Byzantium was activated and I'm not going to talk well the point isn't to talk about formal verification more the point is to sort of get the the options between unit testing and all the way to formal verification I'm not expert in formal verification but without further ado excuse me [Laughter] well you're just missing a video that's fine the so the EVM is a stack machine and every bug that we find or whether it's a bug in the client or bug in the contract the point is that the stack machine is not working as intended and if you don't know what a stack machine is then this video would have showed you but the the three gets pushed onto the stack this blue circle is the stack so the three gets pushed first then the two gets pushed on top then the program counter moves over to the ad and the two gets popped off the three gets popped off they get added by the interpreter the result is five the five gets pushed back onto the stack and then it gets returned so hopefully you understand what a stack is now might be a little important later so the two types of bugs were trying to find bugs and clients and bugs and contracts so let's talk about bugs in clients first the so consensus bugs means that one client is correct and another one is not correct the other one has a bug it's not really a big deal to the average user it's only a concern that keeps you awake at night if you're either a client developer or an exchange operator because well if your exchange operator you know it could potentially be used to steal either from you and if you're a client developer then you'll have to wake up in the middle of the night if one of these bugs is found and this happened in and Thanksgiving 2016 and so the next time around Thanksgiving 2016 or some denial-of-service there are some do s Hart Forks Spears dragon and Chantry and whistle and before those releases they're the clients were not fuzz tested so we wanted to try to prevent the same thing from happening for the next fork and so we started we started fuzzing the type of bug that fuzz testing can not detect is when it's the same bug in all the clients if you have an executable specification like ke VM then you could potentially detect it because it's sort of you know one correct a correct reference reference implementation so that you can you can fuzz test against but without that if all the clients were incorrect then that is like the worst thing you know that you can imagine I mean so a concensus bug there's actually not that bad because at least you know about it right when it happens but an implementation bug that's present in all the clients that's a horrible nightmare because you may not know until you know days later that it happened and we've never had one of these except prior to the launch of the main that and that even that scent is only hypothetical if death was the only client bugs and contracts you have you know bugs and in contract code if you know the solidity person writing the solidity made a mistake or bugs in compiler code if the people who wrote the solidity compiler made a mistake so types of testing unit testing everybody probably understands you have to hand you have to write your test cases one by one and this was we spent a lot of time doing this for Byzantium you know thinking thinking hard Oh what cut types of edge cases can we create what you know weird sequences of op codes you know would be unexpected and and might be untested and you know everybody working on Byzantium sort of tried to think up test cases and then once we thought we had thought of them all then it was sort of okay let's go on and and you know get ready to activate the the fork fuzz testing these unit tests are automatically generated so you can run the your fuzz tester for a week or for a month depending how much time you have and and see if you find any any bugs you can also formally verify stuff get into that later an important one that is often overlooked as the the integration testing so a couple failures of integration testing the Wi-Fi crap attack it was formally verified it was mathematically proven to be secure but there was still a vulnerability because the assumptions that under which it was formally verified did not match up with the the actual production environment could do a hypothetical example for the you know the parity the second parity wallet bug yeah maybe it's secure if you do everything right but if you forget to call in it wallet then it's not yeah so like I said the for Byzantium we did a lot of unit testing there are called state tests and blockchain tests and they're run by a multi-client black box test runner called hive one thing we were worried about before the activation of Byzantium was the block difficulty formula because the way the clients ran these unit tests is that they could only accept a unit test where the block numbers started at zero which meant we couldn't actually test the difficulty formula unless each client maintainer implemented a custom unit test Runner which very few of them did or almost none of them did so we just crossed our fingers that there was no you know bug in the difficulty formula or rather the implementation of the formula in each client and luckily there wasn't so better than unit testing is fuzz testing you you blast it with a lot of different inputs fuzz testing has found a lot of bugs and in a lot of projects but there's of course there's multiple kinds of fuzz testing so the common fuzzing like these you know books here and Firefox and Explorer or flash etc majority of those are found for it with common fuzzing so it's just an input trying to find a crash with with the theorem clients I don't think we we didn't find a single all we did find a couple of crashes but we found even more bugs where the input didn't cause a crash so if we were just doing common fuzzing then we wouldn't have found these consensus bugs so how we find them is with differential fuzzing or equivalence testing so we you know one executes one contract we generate a contract run it on guess around parity running on CPP aetherium if there's any difference then it's a consensus book so how do we generate these contracts we have two ways one is with heuristics based or targeted fuzzing you manually write your own custom test generation logic so you have to be clever and you have to say oh well maybe if we do like a call call stop I mean so it's similar to the mental process when your handwriting unit tests except you just write that in code and then sort of add some probabilities to get a bunch of random combinations then the the other way is coverage driven so you instrument the the code base and and the the first coverage driven fuss tester AFL it was a big advance because prior to that the best you know the fuzz testers that found the most bugs were the ones that had the most clever you know heuristics for generating these test cases but coverage driven it works out of the box on any piece of software that can whose code coverage can be instrumented and it automatically discovers the the tricky inputs that you know that developers would you know come up with but it but it comes up with them automatically and it works out of the box on you know any piece of software that you apply it to some caveats about fuzz testing you're not going to find all the bugs you because you never know if you found all the code paths so just to be clear the difference between code coverage and code paths code coverage is the usual metric you'll see on like github coveralls you know you have 89% code coverage okay we got 100% code coverage if you have a hundred percent code coverage does that mean you have no bugs no it just means you're hitting every line in the code it doesn't mean that you're hitting every possible path between lines in the code so if you hit every possible path between lines then yeah then in theory there are no bugs but you don't know the total number of paths unless you formally verify it so and also you may not discover paths that even a very specific end place okay so the the fuss testers we use are a custom version of of Lib buzzer which is a LLVM thing so yeah Guido Rankin created that EBM lab which are a head of security Martin's Wendy had started and test eath which Dmitri maintains it has a one of these custom test case generators with with heuristics so this is the code that generates a random you know I stick once a byte code that that should be correct so we run that and we compare the traces between each client so here this is a trace and this you can see here that this thing on the on the far side is the stack and it grows with each with each push so here's you know here's FB being pushed on the stack here's a zero being pushed on the stack CB being pushed on the stack - DD so forth until boom these two exclamation points mean that parody got a different result than death and C post and CPP through him and and Pi aetherium and the difference was this last number on the stack where all the other clients got a zero but parody got an FB and that was actually the the first Byzantium consensus bug so that's EVM lab it's using our custom written test case generator then we also have the coverage driven client fuzzer which uses code coverage to automatically discover interesting inputs so the coverage driven one inserts these coverage statements like plus helper ad coverage so in every you know conditional every branch and that's how it measures the code coverage at least for the go code yeah so one thing I did with the width of us testing was get all the traces aligned for coming from each different client and it was a lot of work and I was afraid it was gonna be a waste of time because some estimates were that you know oh you know how much would you bet that there's gonna be a bug in you know a consensus bug in Byzantium you know after it's released or even even before it's really is but you know as we were leading up to it and some estimates for like maybe thirty percent chance that you know that there's a consensus bug and we put all this work into the fuzz tester getting the you know the traces to be standardized because and then we ended up finding one two three four five six seven seven eight you know consensus bugs not just one and I so it's an fortunate that you know developers can't break correct code on the first try but but I was glad that all the work on the fuzz tester you know didn't turn out to be a waste of time so moving on to property based testing and towards a you know towards formal verification property based testing your journey random inputs and your testing that whatever property you're right so regular fuzz testing is your testing that it doesn't crash or that all the outputs are the same with traditional property based testing you you have to write a custom test generator and more recently you know there are projects that include a coverage driven tester and generator so you don't have to do that but we did all this work on fuzz testing the the EVM so we start wondering well how can we post test contracts idea you execute and instruments at EVM measure the path coverage over the bytecode and and then what do you check well when you're testing the clients you can just easily check okay make sure that all the clients have the same output when you're testing a contract it's not so clear what you're supposed to test another option if I mean if you write multiple versions of your contract then you can you know check that all of them are equivalent okay so that's one one you know relatively easy way out because I mean if you have to write your preconditions your post conditions your invariance um it's not so obvious what those should be but you kind of have to do that if you want a fuzz test so the question is if I you know I mean and there it's basically equivalent to a specification so if I have to write a specification in order to fuzz test it then why shouldn't I just you know go ahead and do formal verification well good question maybe you should many tools for formal verification use symbolic execution and so what they do is they they transform a program into you know this giant boolean formula and brute force it to check that there's no you know no way to falsify that that formula against the the preconditions the the invariance that you have specified you don't have to write it an old camel or Haskell you can formally very verify Python code and indeed some of the tools for verifying bbm bbm code is written in Python so Aliante with a Yenta you can you can verify certain properties because they have pre-written the specifications for you so they've written the the properties or the invariance to guarantee that there's no call SEC def ulnar ability that there's no reentry vulnerability that there's no timestamp dependency and you can see that in the when you you know when you run Oriente you know you get the the green check mark yeah there's no call stacked up the others no reentry yeah there's no timestamp dependency and so you're just digging into the oen take code you can see how it imports z3 and and uses z3 to you know power the this process of you know guaranteeing that you know those things can happen with ke vm you write your own custom properties you know for your applications but and you have to you have to specify those properties the hard part is that the specification is in a pretty low-level language so here's an example you know specification I think this is just like you know the first part you know above the fold and and below that maybe it's even more complicated but yeah so if you want to formally verify something you have to write a bunch of stuff like this you know describing what your application should and should not do so needless to say it's not the easiest thing in the world it doesn't really the things that work out of the box are just the you know the generic specifications that are pre-written for you okay but if you have to write your own specification and that's you know it's like a whole new you know a whole new ballgame and it might be just as difficult you know to you know to write a correct implementation in the first place and if they're I mean yeah you know there might be a bug in the verifier if you're gonna put you know a billion dollars in in the contract then maybe yeah use multiple formal verifiers and hope there's hope they don't all have the same bug so another type of formal verification is so why three was the initial one in solidity they removed why three now it's now they've added a similar thing it's called an SMT checker in these invariants are little they're easier to write because you can just write them and you know in solidity and they look like you know a search that you're that you're used to if you write unit tests but they won't catch bugs in the but if there's a bug in the solidity compiler then then you won't you you won't know so it could still in practice being correct and you know be vulnerable to losing money but you won't know so people talk about you know a formal formal spec of the EBM the main one we have now is ke BM the yellow paper is it's semi formal because it's not executable you can't actually use it in any of these you know mechanical proving tools whereas ke BM you can and I cannot see that okay here we go this is not my laptop I just go over here try okay summary um if you don't write a full specification at least write some asserts and if you don't write the asserts if you don't write any asserts then write a couple implementations come find me if you wouldn't tell me I was wrong or have any questions [Applause]