Directions in Smart Contract Research A Selection - Philip Daian

[Music] all right hope everyone's doing good today we're going to talk about writing secure writing secure and correct smart contracts so in particular I'm going to talk about some directions and some problems we've been thinking about in academia and I'll also try to tie it into an industry perspective for those of you who are smart contract practitioners alright so let's start out with who is IC 3 IC 3 is sort of a research hub centered around the universities you see they're mostly Cornell University also UI UC Berkeley Cornell Tech and the Technion we've got 12 faculty at the last count and we're adding more all the time in the last month we've added at least two or three faculty and we've got many many students at all levels of education so before I start I'd like to give a special thanks to the etherium foundation for inviting us here and putting in all the work to bring us together and also to our industry partners at chain digital asset and IBM thank you guys very much for your continued support of smart contract research will also be announcing more partners in the coming weeks and we'd love to have you guys as a partner I know there are a lot of companies here who are interested in the correctness and performance of crypto currencies blog chains and smart contracts so if that's you please feel free to check out our website at an its e3 organ contact us alright so here is the work that IC 3 is doing as far as we see it there are five Grand Challenges in smart contract performance sorry smart contracts and crypto currencies one of them is scaling in performance the second one is correctness third one is confidentiality the fourth one is authenticated data so getting data sources into these systems and the last one is safety and compliance which you've heard a little bit about today so this talk I'm gonna be focusing on correctness and its relationship to security and how we write your secure and correct smart contracts so this is intended to be a high level overview we're not trying to be comprehensive here there's a lot of work we're not gonna mention we're also going to provide some suggestions for practitioners since there are many of you guys in the room writing smart contracts and I'm gonna draw frequent parallels to safety critical software whether they be in planes cars power grids or other infrastructure systems and software like that all right so we all know this problem pretty well by now as a community the problem is you have this software bug it leads to money being lost or stolen and then people who write and participate in the smart contracts cry so there are some things about this challenge that are definitely unique to the cryptocurrency and smart contract ecosystem one of those is that security is more closely tied to code correctness than anywhere else so you have this sort of problem that any issue in correctness which leads to a fault or software bug may be directly monetizable by an attacker and these attackers can also anonymously monetize these exploits untraceable we've also got a unique adversarial environment here so everything that runs on these systems from the miners to the node network to the actors that participate in the contracts could potentially be adversarial and if it's not bad enough already we're looking at public code so in your car or in an airplane you don't have access to the code that's running to try to test it for exploits but on smart contracts all code is public on the blockchain all right so how do we start tackling this pretty difficult problem as far as we see it there are three prongs here that will help us sort of stick a fork in this problem with smart contract correctness and security the first one is formal verification and specification the second one is escape hatches or otherwise known as kill switches and the last one is bug bounties so getting right into it we're going to talk about formal verification here so formal verification is probably the hottest topic of these three in the community right now there are several talks going on about it at this event and it's a really exciting space to be in so what do we like about formal verification well first of all I think specification is a great virtue so by rigorously and mathematically specifying what you're building it helps you understand the systems that you're making on a deeper level also specifying the lower levels this rigorously things like the EVM and the languages that we're using helps authors of higher level systems know exactly what guarantees they can expect from these systems so specifications are great and the more rigorous these specifications are the better we can start to stat start to tackle the problem of writing correct contracts English specifications are pretty common in the field these are definitely not enough they admit ambiguity you want an example of this check out the ISO c11 standard which has a whole committee whose job it is to argue about whether certain programs do or do not conform to the standard formal specifications can also go further in serving as criterias for Forks so the question of when to fork these systems could be answered by when the implementation of the system differs from its specification in which case you have a very clear bug obviously specifications also give you these other side benefits they can help us find bugs and they can help us generate tools that we use to analyze our contracts all right so let's talk a little bit about the work that's being done here both of these slides are gonna have later talks on them so I'll be brief one of them is this tool called Oriente out of the university of singapore i believe and what they did is they took the semantics of the EVM that was very nicely laid out in the etherium yellow paper which i think is an excellent document and a great way to sort of set the standard for the rigor that we expect from these systems and they built some tools on top of it to analyze the block chain to try to discover bugs in smart contracts running in the wild so I highly suggest you read the paper I love the work that this team did I think it's not perfect I do think that there are many false positives that sort of come with their approach that we can further refine and get rid of as these tools evolve so if you want to talk more about this work you can ask questions at the presentation that's coming up later in the event or you can find me afterwards all right here is another great example dr. christian right weasoner I hope I pronounced that right with a y3 sort of back-end for formal verification in solidity so here you can see a very simple funds contract and a specification over this contract that was presented at the ic3 etherion boot camp earlier and this contract allows you to withdraw a certain amount of shares and comes with the specification that the number of shares preserves the balance of the contract so that was the wrong direction so here's another contract that satisfies this specification and this sort of helps us illustrate that writing complete specifications is pretty difficult so if you're a trained developer you're sitting here looking at a set of specifications just like writing buggy code there could be something that you miss now this is not intended to say that that this work was intended to catch these sort of cases this is obviously a trivial example but the general point is anywhere you look in the formal verification space writing these specifications is extremely difficult so the gaps in this work specification is hard some properties can't be specified at all I'm thinking specifically about properties of incentives game theoretical properties and higher-level properties of smart contracts that are pretty much impossible to specify often when you have a proof of these kinds of things you are trusting the tools that outputted the proof which is not an ideal situation because these tools are very hard to audit and they require significant expertise we don't even really know how to audit them in general a key takeaway I'd like you to get from this is that any good tool must use some sort of semantics that is a definition of of the lower levels of the language and the infrastructure on which they operate so when you're trying to evaluate one of these tools ask yourself what semantics are they using how is it audited and what guarantees do we have that that system will actually conform to those semantics right now to really formally verify complex systems we need experts we need multiple PhDs it's not an easy problem and there are also some famous incompleteness & undecidability results that may suggest that gaps in these logics could require more work to achieve a robust system all right so escape hatches this comes out of the need of not always being able to verify our contracts so what we need here is something they figured out very early on in safety critical systems which is we need to put a human in the loop at some point it's true that the promise of these systems involves in many cases taking the humans out of the loop and I think in many cases that can be achieved but we shouldn't necessarily take that as an absolute if verification or bounties or the other two prongs of the approaches fail it's important to have some sort of failsafe or backup mechanism there are a lot of parallels to legacy contract law here so there are a lot of lessons to be learned from how people have done this previously in contracts and also parallels to safety critical systems so I'll pose the question to the audience would you write a nuclear power plant software that has no kill switch in it probably not and I wouldn't want a multi hundred million dollar contract not to have one either so we've been doing some work on this and I see three by Bill merino here I highly suggest you read the paper for more information since I don't have much time to discuss it and what we did here bill was a lawyer by trade and got a master's in computer science and he looked at parallels between smart contracts and legacy contract laws so he looked at all of these concepts of termination rescission and modification that are codified in the law that have been designed to solve problems that have come up in historical precedents and he wrote little etherium libraries sort of mirroring these concepts in traditional contract law so if you're writing a high-volume smart contract I highly suggest you take a look so this is again not problem-free we've got a bunch of gaps in this approach how do we verify that the escape hatch code is correct what layer do we put the escape hatches in do we want escape hatches in the EVM which would inherently be sort of less general since you'd have a specific set of hatches or do we want to put them in the compiler which lets us save some generality by deferring the problem to the language or do we want to just say contracts use well audited libraries of escape hatches that you can modify as you see fit giving us that full generality so it's an open question there's also a lot of potential for abuse and escape hatches so a bad actor could perhaps trigger an escape hatch in a case where it's profitable for them even if it doesn't follow the intent of the escape hatch that's something we always sort of need to keep in mind okay so can you think of a badly made escape hatch there is there have definitely been contracts before that have intended to provide a mechanism for users to remove funds that have then been abused to drain all of the funds out of the system I won't mention specifics but it's on line six six six of the contract that I'm talking about it's also worth noting that that Forks of the system in general can be viewed as an escape hatch whenever there is a catastrophic failure involving multiple aspects of the system you sort of get the social consensus based escape hatch that comes with the back end architecture of these systems all right the last prong of our three three-pronged fork bug bounties so we believe bug bounties are very important because the incentivization structure of developing exploits is pretty broken without bounties so what do we mean by this insecurity traditionally we say it's never impossible to exploit a system it can only be expensive and when you have a cost of exploiting a system that's actually much lower than the amount that's to be gained from exploiting it an exploit and an attack will pretty much inevitably surface so in order to fix these sort of issues the general security community has recognized the value of providing bounties to incentivize people to defend the system financially rather than only financially incentivizing attackers without them defenders are really only motivated by ego or maybe goodwill which as we've seen in the past are not really powerful motivators to do the type of work that's required for a full security audit so the good about bug bounties we have the poor man's formal verification or as we like to call it decentralized censorship resistant anti fragile incentive compatible crowd-sourced verification you can tell that one to your managers and I'm sure they'll be glad to fund your escape hatch development all right so we got some cool work going on in this space some of my favorite work is the idea of using these prediction markets that we're developing as sort of Canaries for one an exploit is about to happen because attackers will naturally be incentivized to to reveal this by taking a position on the prediction markets in that direction so that's sort of the more fringe work that's going on we also have work that directly addresses these issues in a more traditional way so there's a blog post by Simone de la riviere again I hope I'm pronouncing that right on medium called asset cards which I highly suggest you take a look at that details one potential approach for escape hatches there's also escape hatches mentioned in the etherium best practices for smart contracts documentation and there's a user called doubt challenge on medium who's posted a series of really small contracts that contain common patterns and ask the community to try to break these contracts in order to reveal underlying language flaws or issues in our coding practices that we haven't really yet thought of there's a lot more work going on in this space if you google escape sorry bug bounties if you're my bounty smart contracts you'll come up with a ton of stuff so there's a common problem in in academia and in general that you have all of these great solutions to the escape hatch problem and all these great proposals and you consider the problem solved and I would urge you guys to avoid that line of thinking because there are still gaps in this in this bug bounty approach so with prediction markets there's always the question of how to avoid bad incentives and how to prevent incentivizing attackers and bad actors from actually deploying their attacks on the main end and profiting there's also the hard problem of how to create trustless bounties with trustless payout we don't want to leak these exploits to the test net because once you leak the exploit to the test net you've removed the incentive for defenders and attackers can take that exploit and deploy it on the main net we also don't want to trust contract authors to pay out because that significantly harms the attackers incentive to report the the bug if they think it's a really profitable bug and the contract authors may just invoke a kill switch or fix it before they have the chance to get paid there's also the very very hard problem of how do we define conditions for bug bounties how do we know when an exploit is a valid claim of a bounty we have a bunch of academic solutions here sealed glass proofs we have a paper about that on our website that basically involves using trusted hardware to deliver a proof of an exploit without revealing the exploit itself SGX also leverages trusted hardware maybe zero knowledge proof could be useful here etc bug bounties are also hard to do for subtle issues things that I talked about before gain theoretical issues or fundamental flaws in the architecture of your contracts so like our other two prongs they're not a silver bullet also I urge you not to forget traditional software engineering test fuzzing static dynamic analysis phase deployment upgrades smaller test contracts these are all very valuable things I don't think I need to talk about them pretty obvious how to use them and I highly suggest you cover all of these bases if you're writing a high value contract alright so takeaways we've got lots of work still to do here the ecosystem definitely will develop good formal tools we have a number of talks on this think about humans in the loops when you're writing your smart contracts and use bug bounties as a stopgap for verification and incentive fixes thank you guys for listening and if you want to interact with us further please check out our website at India c3 org check out our publications and we are always looking for industry collaborations and partners we'd love to work with you to solve the open research problems in the space so definitely contact us or find me somewhere if you have questions about anything I've said here all right thank you very much [Applause] [Music]