Enter the Hydra – An Experimental Approach to Smart Contract Security

[Music] hello everyone so today I'm gonna be announcing and releasing a new project we have at IC 3 IC 3 is sort of a cross university initiative for experimental blockchain research and systems this is joint work with Florian Trevor from Stanford and Lauren's Breidenbach from ETH Zurich Cornell Tech and IC 3 as well as myself and my advisor Ari Jules also from Cornell Tech and IC 3 all right so just a brief reminder last year I gave a talk in Def Con on smart contract security and we talked about how we sort of view this problem at IC 3 as having these three different prongs of formal verification and specification so how do we know what we are building and how can we check it escape hatches how do we recover when something goes badly wrong with the contract and bug bounties so how can we address these perverse incentives where people in the ecosystem are incentivized to attack and steal money rather than honestly report vulnerabilities so for some general security background I highly recommend checking that talk out all right umm so there's some new promise in the space in the last few years you can see sort of this Google Trends graph and this is for this new concept called crypto economics so what is crypto economics crypto economics is sort of the idea of combining cryptography to look at the past and economics to provide security guarantees that hold into the future to secure these protocols and contracts that we're all building here there's even been a crypto economic security conference this year at Berkeley for the first time and by the way blockchain at Berkeley we totally agree that the blockchain space needs more academic presence all right so is this planet hyper is this the real deal let's take a look so whereas crypto economics kind of being explored right now we have the original sort of incarnation of this in the Bitcoin system and the Nakamoto white paper and we have several new protocols that are coming out among which relevant to the etherium community is kasper and the set of protocols it encompasses that are also using the style of anonymous of sorry analysis alright so where don't we have crypto economics unfortunately there is not much crypt economics going on at the smart contract layer so we really don't have rigorous economic analyses of most of these contracts or cryptographic mechanisms to sort of guarantee the properties we're looking for and that is why today we're announcing the Hydra project you can check out the Hydra do and sort of follow along and read the paper or look at the code I highly recommend you do so if you have a laptop and the Hydra project is a smart contract development framework that gives you decentralized security and bug bounties with no humans in the loop and no trust required for payment rigorous crypto economic security guarantees that we can model and analyze and a strategy for mitigating both programmer and compiler error a little bit of a warning here the Hydra project is still in sort of the research phase we're still undergoing testing process security audits and other sort of high assurance software development processes so we have released all the code for you guys to play with and start experimenting with and give us feedback on but trusting large amounts of funds to this little baby Hydra that we've sort of spun up would probably be a mistake all right so why bounties traditionally you sort of have this limited time for software development you have two to four people take a look at it do a code review and then you ship it to the customer this new crowd security approach says basically for an unlimited time you run a little bounty and you let the community look at it with the idea being that many eyes are better than one all right so let's see this as a game since we're talking about crypto economics and take a look at what a rational attacker would do with these bounty systems all right so here is a system with no bounty an attacker finds an exploit and then they have two choices they can either attack and steal the $1 in the contract or they can disclose and get nothing so obviously they're gonna attack the contract every time this is why we need bounties all right how about traditional bounties like the kind I showed you on the previous slide well there's a problem here which is that an attacker doesn't actually know when they disclose how much money they're gonna get paid so they actually have no way to make a rational decision on whether to disclose or to attack the contract all right what would be a better game what would we sort of want out of this functionality well one thing we definitely want is we want the attacker to know sort of what the value of the bounty is so they can at least make somewhat of a rational decision and attack only if the contract value is greater than the bounty unfortunately this means you need to have very large bounties and essentially pay more than what the contract is holding which doesn't really make sense so what would we really like to see economically we'd like to see sort of this game where an attacker once they find an exploit either has the choice to disclose it for some amount or to continue trying to attack which will incur it to them some cost to eventually try to steal all of the money in the contract so in this game an attacker is gonna attack if sort of the cost they have to do to fully exploit the contract the contract value - that is greater than the bounty so what do we want to do here we want to maximize this see if we can create such a game as high as possible and sort of get the best possible economic security for our contract this this see costs after finding the first exploit to a contract is what we call an exploit gap so we say mind the gap and introduce an exploit gap what are other things we'd like out of our bounty we'd like the attacker to be able to either attack our contract or claim the bounty but not both we would like the payout to be predetermined so they can rationally make a decision on whether to take the bounty and we would like to payout to be fully trust less it's full of stories on the internet several of which we cited in our paper about hackers who complain that X company didn't pay them or they didn't pay them enough or they didn't agree with their assessment of the bug so we want to get rid of that completely by just eliminating humans from the loop and allowing the attackers to see exactly what they get all right so how do we do this there are many many ways to accomplish an exploit gap several of which we mentioned in our paper but the one we're gonna look at today is this thing we call the Hydra program which sort of takes this classical idea of an version programming and tweaks it a little bit so that rather than focusing on availability as you would like in an airplane system or a space shuttle or something like that we focus on integrity so what you do is you develop multiple copies of your contract independently and then if any of them has an error you can notice the divergence in the output of those contracts and then use sort of a governance contract to to abort your contracts and pay a bounty and do some safe recovery procedure where either the money is returned or it's sent to a trusted multi-sig etc all right so this sounds great but I heard that n version programming sucks and it's like not fully independent so what are you talking about so let's look at when we actually get this exploit gap out of our contract let's say one of the versions you do has a bug of course then you get the exploit cap because it's very easy for the governor to sort of notice this what if all of the versions you have have a bug well you might still be okay as long as it's not an identical bug our governor our governor's contract and sort of noticed a divergence between these contracts and pay the bounty sometimes though we have no gap and this is a little bit unavoidable so if all of your heads all of your n heads have the same exact bug then unfortunately you're sort of out of luck and the attacker can fully exploit the contract and break the game this might happen if you have a incredibly common mistake a universal compiler or EVM bug or a bug in your specification that sort of all your contracts implemented so it's not a perfect system but still we say let's bring back the 80s and maybe we can do something cool with this system all right let's take a look at some of the highest value losses in the etherium ecosystem over the last few years the parody multi-sig the dow a smart billions etc so here we've sort of highlighted in green the the exploits which we believe that this kind of methodology could address very easily in red which you can't tell is read sort of this bottom line the ones that we can't address because for reasons described in the paper we don't handle gas issues as well as ones that maybe could have been addressed but it's a little bit more complicated than just taking a look at it and saying yeah definitely this is okay so what I'm gonna say is five and a half out of seven is not bad and it's a great start towards achieving the sort of rigorous security that our ecosystem demands all right so a warning we got some math coming up so if you hate math you might want to tune out for about the next three minutes so this is sort of the crypto economic analysis I was telling you guys before so we want to ask sort of the question when is honest behavior incentivized so honest behavior is incentivized when the payout of the adversary for following the honest strategy that's this payouts of age over the payout of the adversary for following the malicious strategy is greater than one indicating that the honest strategy is expected to pay the adversary more than the malicious strategy so it's to sort of arrive at our analysis we model bug finding as a Poisson process so these t T variables over here sort of are random variables modeling the time either an honest player or a malicious player is going to find an exploit and this gap variable here is sort of the the size of the exploit gap we managed to achieve with our contract what does that look like well we do this analysis that involves defining an ideal functionality which you never actually have to define as a user of the Hydra framework but it sort of represents in our analysis the functionality the developers had in their mind when they created it and if you have if you have this P where we're sorry if you have this if you have the number of total heads the space of all exploits and you sort of randomly sample a bug and you can get this P which is the probability that that will apply to one of the heads then you can rigorously quantify it and even graft your exploit gap which is nice the nice thing to notice here is that this exploit gap is exponential in n which is the number of heads that you do in your contract so even if you don't have perfect independence among your heads even if bugs are somewhat correlated or likely to affect multiple heads in your system you still might create a large enough gap and enough independence to have this sort of governance contract detect the error so that's a really nice result and it kind of differs from classical inversion programming where you do something like take the average of a bunch of different programs and then one program being off could badly damage your input and sort of lose you all assurance all right so let's get back to earth if you tuned out for the math you can come back now so what are we doing so we're launching an ER c20 mountie details about that are available at our website the Hydra do we have it funded with a thousand dollars today so a thousand dollars is the reward for sort of breaking the full contract and achieving that full dollars a exploit I talked about in the first slide if you only managed to break one of our heads and are our governor's contract manages to catch your issue then you get paid 1/10 of that which today is a hundred dollars why so low well this is a research prototype and we're still sort of undergoing testing and we expect to rapidly iterate this our hope is within the next six months or so to ramp up to a 50,000 dollar bounty on the maintenance the contract that we have deployed right now is just an e rc 20 that's one-to-one peg to ether and it's running to solidity implementations one Viper implementation and one serpent implementation yes serpent and if you can manage to trigger the bounty with a serpent compiler bug or break the whole contract I'd sort of like to see that happen on chain so that should be a little bit of fun we also believe we've written the most thorough ERC 20 test suite that's currently available open source and we encourage you to check that out on our website and if you can propose additional tests that we didn't cover that would also be wonderful and the ERC 20 viper contract that we wrote has actually been merged and integrated into Viper as sort of a standard example of how to write in the RC 20 so the project has already sort of produced some real-world artifacts we also have a Monty Hall game a generalized Monty Hall where you can sort of bet on the the outcome of a Monty Hall it's in testing still we don't know how large of a bounty we're going to launch it with we wrote this contract because we expected it to be challenging and there is code and specification for that on the website and we expect it to be live soon all right I didn't do a demo because I didn't want the risk of things blowing up on me and we only have so much time so I'm going to sort of take you through a picture demo of what it looks like when you're interacting with these contracts it's very easy the address that they're deployed out in the ABI or all on our website so all you really have to do is plug them into any aetherium client or any aetherium tools and you should be able to interact with the contract like it was any other ERC 20 so here it is in my ether wallet you can see there's like a few functions that you can access there some of which are not in the original ERC 20 contracts but were added for the Hydra one example is this bounty claimed so the bounty claim flag you can look at for any token contract or other Hydra contract and it will tell you whether someone has already sort of claimed the bounty by causing that divergence that we're talking about so here it is true all right and this is what sort of a history of transactions look like you can see the contract creation there someone deposited some ether into it and then they found an exploit and that top one is actually what a bounty claim transaction looks like so here it is blown up on ether scan I don't know if you can see this the font is a little small but what it's done is it's transferred 1/10 of the ether in the contract to the person who found the bounty so this is sort of that 1/10 of that 3/8 we mentioned earlier and it's transferred the rest sort of back to this trusted multi-sig which we're currently just using the Creator contract all right and so how do you actually develop a hydro contract we have this sort of Hydra process that we're proposing which has three steps the first step is specification so this is something you always want to do for your smart contracts anyway please start doing this guy's which is to write a independent specification of what functionality you're trying to achieve in enough detail so that a programmer with no communication with you could sort of sit down and implement that correctly the second step after that is implementation so what that looks like in Hydra is you ship off that specification to a bunch of different developers and they sort of implement your contract it's worth noting that you the Hydra is sort of flexible in how you use it you don't necessarily need multiple developers you can also just compile with multiple compilers if all you want is a bounty on a compiler errors or you can deploy it sort of alongside your original contract rather than using it fully in production to just get a separate decentralized trustless bounty so while we were developing our er c20 with this process this process helped us find integer overflow bugs GRC 20 non-conformance errors that is developers incorrectly implementing a specification and the most surprising one is sort of this suicide issue that ended up winning the underhanded solidity contest or placing in the underhand solidity contest whereby you sort of suicide send money to a contract and corrupt its balance without allowing it to run it's fallback function and react this send so this suicide issue occurred in our contract because we are writing a one-to-one ether peg so the total supply function on three of our contracts would use a UN 256 to keep track of how much ether had been deposited and just return that but on our last contract the total supply was actually just returning to stop balance so if you suicide sent to that one head that was returning this stop balance and then ran total supply you'd be able to claim the bounty and you could do that either as a contract transaction or as two separate transactions on the chain and I think that's really cool because we actually were not consciously aware of this anti-pattern while we were developing the contracts and it's sort of something we realized and tested after the fact the other nice thing is all of the issues we found which we found about I would say four or five during the process of our development we're all claimable bounties and none of them were full exploits against all four of our contracts so that sort of at least informally empirically validates the approach a little bit you might be thinking well this is horribly expensive I'm gonna have to be paying a ton of gas to do this I don't want to pay five times the gas I mean it's certainly true you're definitely paying more gas with a hydro contract and with the regular contract the nice thing is that it sort of scales a little bit better than you'd expect so these dotted lines are sort of lines with a slope of one which is how you'd expect a Hydra to scale you add another head you sort of add one to the the constant factor of your costs the nice thing is that we actually scale below that slope of one because of some constant overhead that's associated with evm transaction costs and we can scale pretty significantly below it depending on what type of contract you have so the more you you sort of alter storage the closer to this slope of one you get because storage alteration is the most expensive operation our contracts are performing here all right another thing we would like to announce soon is integration with HACC this contract hack this contract is a platform that we developed a few months ago in the boot camp for the ic3 boot camp which has a bunch of examples of intentionally vulnerable and insecure solidity contracts so you can go there you put in your account for the test net we're using rinkeby right now it'll deploy you vulnerable contracts and then it's your job to sort of hack them and have the site tell you you did it right so ideally we'd like to sort of make this a hub for people trying to hack contracts and we'd like to have sort of these easy challenges which are obviously vulnerable as well as these harder challenges that we think that are secure and cannot be broken and do payout real eath in the case you do break them so that's a future direction we're working as well all right what about formal verification I've been hearing a lot about this formal verification thing doesn't it make this whole Hydra obsolete not really so it is my belief that programmers will always sort of develop past what the formal verification allows them to prove and many lower assurance contracts won't want to put in the cost to do full formal verification which can be expensive so this is sort of a lower bar approach you only need to develop your contract three four or five times whatever most of these contracts are like to three hundred lines so this is not really a substantial expense that we're talking about especially when you consider that they're holding in cases hundreds of millions or even billions of dollars in user funds so we see this as sort of a stopgap approach to formal verification with the nice property that it encourages you and sort of requires you to write a detailed specification which you can then use to formally verify your contract all right the last thing that we handle front-running so we have this problem you found a nice juicy bounty it's worth five million dollars you're excited to claim it and become the next Eve millionaire so you submit it to the chain and then someone else sees it or some script sees it or some miners sees it and sort of rebroadcast the same transaction with a higher gas cost getting mine before yours suddenly they've got the five million and you've got nothing so this sounds pretty bad and it actually gets worse if you allow this issue to persist it breaks our whole economic game because what an adversary a powerful adversary can do that has a good network connection is sort of fine and exploit and then sit on it until they see someone else has also found an exploit and then release it so they can sort of keep trying to break the full contract and withhold their exploit from the bounty process which is obviously something that we'd like to prevent so we introduced this new scheme we have a blog post on it it's called submarine commitments it's used in the Hydra project not in the current alpha prototype which is only intended for small amounts but we do have code for it and we're sort of waiting on a IP e IP 86 to be released which is what we need to deploy this and after that we will have submarine commitment enabled bounties and the nice thing is this can even be used outside of bounties all right so the research contributions here we have the first rigorous crypto economic reasoning on what used to be ad hoc security and bug bounties including how to price them we have a model for how to price these things in our paper we have an N head approach for achieving this exploit gap concept that we've introduced we've introduced software and bounty code development so put the bounty in the software development process as a first-class citizen we've sort of revived this old and sort of stale and dead and head approach for correctness and we've developed what we believe will become the most secure contract eventually on the etherium maenette because it's the only one that really has these rigorous economic guarantees of security and a really nice thing I'd like to point out here is that this kind of bounty this kind of decentralized process is not possible outside of smart contracts so this is something new enabled by these systems all right what do we want from you guys they have 20 seconds left hack the contract join the riot claim some bounties it's alpha should be easy money if you want to be spoke about tea for your token or whatever feel free to get in touch feedback on paper code is always appreciated and eventually if the community or some projects in the community that are doing really well and use the ERC 20 code can contribute to these bounties that would be incredible so yeah please give special thanks to the NSF for funding this project both through grants and through a graduate research fellowship for me thanks to our reviewers Rahul and Paul for reviewing this paper and thank you to our IC 3 industry sponsors that chain Microsoft Intel fidelity digital asset IBM and Shady Morgan for sponsoring this work and thank you all of you for listening here's the official sponsorship and disclaimer slide and that's it thank you [Applause] [Music]