# Panel: Formal Verification

- Channel: [Devcon](https://streameth.org/devcon)
- Date: 2018-10-07
- Duration: 25:50
- Watch: https://streameth.org/watch/yt-DrDIcirrhWM
- YouTube: https://www.youtube.com/watch?v=DrDIcirrhWM

## Description

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/3/formal-verification

Phil Daian, Everett Hildenbrandt, Yoichi Hirai, Loi Luu, & Reto Trinkler discuss Formal Verification.

Speaker(s): Phil Daian, Everett Hildenbrandt, Yoichi Hirai, Loi Luu, Reto Trinkler
Skill level: Advanced
Track: Developer Infrastructure


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 3 was held in Cancún, Mexico on Nov 1 - 4, 2017
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

so hi everyone my name is Rita twinkler I'm the chairman and co-founder together with Mona Lisa of Mellon port and Marcin advisor to the web 3 Foundation so great so let's starts with formal education so formal verification is the act of proving or disproving an algorithm with respect to an Intendant underlying algorithm so this algorithm is specified in a in a formal specification so I'd like to ask all of you what makes a good specification what makes a good specification that's a good question so I think theoretically the the answer is that the specification accurately captures the intent of the developer who wrote it making sure that's the case is obviously very difficult so I think a lot of that depends on sort of your tooling and the feedback that it provides when you're writing the specification but in general I'd say a good specification accurately reflects the intent of the developer and also encodes sort of all of the assumptions that the smart contract makes very explicitly and very clearly so that if someone were to update the smart contract later or something they would all be very nicely in the same place is going to add a little bit more I think a good specifications to be easy to understand and to be easily to for other to you know read and you know built ask a little and it's clearly you know it follows some standard as well I think in general any specification is better than what most people do which is no specification so that's probably a good place to start ideally you'd you know write a specification and then argue over that for a few days at least and then you know write your tests and then the encoding but a lot of people kind of do it maybe in the reverse order or something like that maybe they never even read a specification so please answer captures it but maybe a good specification should put contract in bigger picture what kind of game people can play on it what would be the well-paced strategy for rational players and so yeah if a specification fits into this script economic mechanic game a theoretic reasoning that something nice but the yeah this depends on the application Thanks so so what is your take on a specification kind of you know specified kind of abstractly with formal methods of mathematics Bosch versus specification implemented for example in Haskell so I mean one is kind of like a reference implementation in Haskell and the other is just kind of abstract like purely theoretical well I think that a reference implementation in Haskell is a perfectly fine specification honestly I think a lot of people when they think of a specification think of kind of just an English language document or something like that but at least in our group we focus a lot on executable specifications so I think you know a Haskell implementation you know that's a whole lot hell of a lot better than no specification once again and at least you can test it right you can you can run tests against your specification even before you go to implementing the final thing so that's that's already a huge huge advantage over an English language specification for example but certainly English language specifications are easier to write so maybe you start with that and then do the Haskell or something like that yeah I totally agree with everything that was just said and I sort of want to add that you can have good or bad specifications in any format so absolutely while it's nice to have a specification be testable and clear and readable you can have really really good at Haskell language specifications or you can have pretty bad Haskell specifications and I've even seen English language specifications that are not entirely so sort of goes more to the expertise of whoever's implementing it I think great [Music] so like could you maybe share a bit about what is like new and unique about formally verifying smart contracts blockchains kind of compared to you know safety critical hardware verification and what are the corresponding opportunities of it you know what is new and unique about formally verifying smart contracts or blockchains compared to like for example verifying hardware and what are the opportunities of it I guess smart contracts has a new sort of play semantics right so we have a concept and action at the conservative gas and solid token heater which you know doesn't exist in in you know existing system like you know critical hardware or software system so when you really formally verified I think you you need literally find new property that you want to verify that only exists in you know smart contract and also it Orion there's definitely some really nice things about smart contracts they are bounded in terms of their execution time there are generally very small simple programs at least compared to something you'd see in a safety critical system a car or an airplane or something like that and they directly handle large quantities of money so actually I'm really excited I think that I said this last year and I still strongly believe it that as a space we have an opportunity to set standards for how software is developed even beyond block chains and smart contracts because I think the users of smart contracts and block chains have a much stronger understanding and demand for this kind of technology than the users of a car or something like that so it's room torture machine has no non determined behaviors no not defined behaviors because that means consensus folks so so this possibility of different clients following different folks is a huge problem but it's really bracing for us on top of the virtual machine because that means the specification is really always deterministic that's a huge improvement over proving anything over intelligible so our cheapest Thanks pretty much agree with what people said the non determinism makes it easy to bound it gas makes it kind of nice although sometimes it's hard to reason about exactly how much gas the contract will use and basically you know what's making the most driving force behind this is the amount of money being at stake essentially as opposed to just normal programs in other settings let me move over because a course really equals to make it really hard hard for me to understand the question yeah it's it's kind of interesting how people care a little bit more about money than their lives right you have someone lose their fifty thousand endow tokens and they're clamoring for formal verification but then Toyota has an issue in their ECU's that kills 20 people and Toyota customers could not care less about the software in their car so I just think that's kind of an interesting observation on humanity it is kind of interesting yeah right so could you maybe talk a bit about the limitations and challenging challenges so for modification and maybe also like introduced the project that you're involved with and how your project kind of tries to make things easier or better so my background the interactive theorem proving is not user friendly so take class of computer science students of thirty people maybe a couple of them willing to use interactive theorem provers maybe only one of them can finish verifying a program of like 2030 times in the month also so it's kind of challenging actually verifying software using these interactive theorem provers is so challenging that I don't see much I don't see many successful applications so but for the reasons described before I believe in a theorem it might still make sense I guess you know it's really hardly to formally prove you know existing smart contract especially the complicated one because you know first of all you need like to represent them in some mathematical model that you can easily prove some property later on but you know it's really hardly to you know you know convert or transfer or you know interpret the program into the new language or the new model because of the you know compare compatibility issues right and also sometimes you cannot even explore all the possible you know outcomes or in properties of the program and you know most of the formal verification true requires you know a strong background and and you know human involved right and most of the project and companies do not have these you know people so so you know we're really like we we need like some sort of like you user-friendly developer tool so that you know you can just like run the tool with some existing smart contract and it will produce other or the headphone output for the developers Thanks yeah so I work on sort of a number of projects in the correctness space one of them is I'm advising this sort of heavier weight formal verification project called KVM I'll let Everett describe that since he's actually the lead but to speak to the broader point I think there's like a very wide range of correctness techniques that we have here both formal informal and semi formal and another one of the projects I'm on Hydra is sort of a lighter-weight approach to this where you abandon full formal guarantees for sort of low cost and easy startup which i think is a very valuable thing to a lot of companies who aren't going to be able to as Lowe said hire the right people or have the right expertise at the end of the day formal verification is still super expensive it's still hard to do and it still doesn't give you perfect guarantees so it's understandable why for a lot of people especially now that the tools are not totally mature the business case sort of isn't there so I think we need to develop a range of techniques and ask ourselves what are really our high assurance contracts here to use our full fledge techniques and how can we get the other ones to a better level of security with like the lower hanging fruit techniques you know I think I agree pretty much with what Phil's saying here and actually it makes me really happy that I see so many people just emphasizing the importance of testing and of writing specifications because just those two steps alone forced you to you know first clarify in your head what is it I'm trying to do which so many people don't even do they just sit down and start kind of clunking away at code and then second to kind of conker ties that by writing some tests and then say like is what I did actually you know implementing these these tests so the test kind of serve as a semi specification if you will or concretization of the specification regarding the KVM project that Phil mentioned you know I think it helps with the entire you know there's the entire range of verification that you can go through right you can start at testing and you can move up to some sort of runtime verification or runtime model checking up to model checking which is where you explore the whole state space of a program and then up to theorem proving where you use more advanced techniques to prove that a program is behaving correctly and K gives you tools for all of those things actually so I think you know KTM can be a useful tool in that space it doesn't have quite a nice user interface unfortunately so it suffers from that but I think it can help a lot in in all those areas Thanks so it seems like a common theme seems to be it's like too complicated so so how can we make tools and/or how can we develop approaches or more accessible to the end-user I think in the end it's not reasonable to expect the end users or users to read logical formulas or maybe K configurations are more accessible but it's hard so at the end what we want is sure that can synthesize an advisory based on the unproven goals this scenario can happen and it can play it may be not an animation but like it should look like somebody attacking you your contract that would make the problem much more easier to understand so I guess if stability is always a hard problem right and that's also like one of the motivation that why we build buoyant e the smart contract analyzer based on symbolic execution so the idea here is that you know user they do not need to understand like how authentic works they're only need like to paste the smart contract into Oyen T or into the you know web browser and they click analyze and we can just like show all the possible vulnerabilities that orientation can figure out yeah I personally think demand sort of breeds progress in this direction and we're sitting in a room of some extremely smart and talented people and we've seen some projects that really push the envelope in a number of spaces and while the tools are hard to use and there certainly could be improvements made there nothing here is sort of magic or anything like that so I think sufficiently motivated developers who are incentivized by the market to develop these tools is really what we need to push the the envelope here another thing that I think is really helpful and I'd like to especially congratulate melon port for taking this approach is to take these things out of academia and into industry and use them on real contracts with real developers who are working on the ground in solidity I think just that step could do a lot for usability and academics are not really the the greatest at writing super useable systems sometimes so more more broad participation would definitely help yeah if they're 13 that in just 30 seconds it but yeah definitely the the approach that that mellon port is taking seems to be the correct one just make the tools usable and make them have check for some some specific properties automatically certainly all the verification tools can be instantiated to do those sorts of things but you know it takes effort and takes developer time it takes people who know the tools to do that instantiation and that's not going to happen overnight so you know these lighter-weight methods like fills hydro stuff that's really gonna be the stopgap until we can have better tooling for all these you know high assurance tools so the last question from from me and then opening it up to the audience is essentially a shout out from you guys so but what would you like to see come from different ecosystem players so from from the users developers investors the project leads and researchers to make formal verification mainstream in the current ecosystem I think it's to the users responsibility to make sure that they understand the contract they are interacting with some people people are like proposing markets for audits and so on but it is not working yet so actually I have to repeat Martin I mean it's fair to say this but you have to be it a byte called learn the VM in order to make sure that you are interacting with busines brew thing it's sort of Sadie's but it's something like that currently and then yes something like audit market with reputation system something like that very gradually improve the situation but yeah now due diligence is required for all parties I believe so I see there as sort of being two pushes that need to happen one of them is bottom up the users need to really start demanding that if there are techniques available to ensure the correctness of that kind of their contracts they're either used or a good justification is provided for why they're not used We certainly have a few tools right now we've seen presentations today about quite a few of them so so users really need to start being more selective about where they put their money and well sure it's tempting to sort of buy into every single ICO and flip it for 2x or whatever that's not the kind of space that sort of incentivizes and fosters rigorous proper software development and so I think users and investors need to become more selective and and developers need to sort of enable them to do that by really going through the processes in a way that's serious and in a way that they put in a concerted effort to get the maximum assurance out of their contracts Thanks yeah kind of echoing what you said a little bit you know no amount of money as a substitute for just understanding right so at some point you just have to read and understand the bytecode and understand how EVM works and understand hustle it D compiles to EVM or whatever tool it is whatever high level programming language you're using how it compiles DBM and what the implications for security are in that setting and you know the people doing security audits they understand this really well and they like they were saying earlier you know they just read the code and read it again and read it again and read it again you know there's no substitute for just putting time and effort into you know high assurance software well I guess you know in order to make formal verification popular I think we need to adopt this first right so I mean I hope that we can have some sort of like ERC that you know that allows you know people to put you know maybe orientate half Hydra attack or you know KETV on tap into every single smart contractor has Ben you know deploy in the Italian blockchain Thanks so anyone from the audience would like to ask some questions yes maybe it's better if people with questions should come to the front that's probably a good idea for the next person so from an artist standpoint how would you like to see people who provide smart contract audits either contributing to your projects or using your projects I assume it's sort of maybe one or the other but maybe there's both for us right now does that make sense yeah I do do some smart contract audits and I would say ideally the role of these kinds of tools in the long run would be to sort of put most of that business right now out of business to an extent like at least that's my personal go with it in all my audits I always make recommendations to the team about which tools are state-of-the-art and what they should be running on their contracts certainly auditors can run these tools on the contracts as well but at the end of the day my personal opinion is that it's the responsibility of the team and the team to sort of seek help when they're not able to do something like this especially because you know most teams are would not be willing to sort of pay the hourly for an auditor to run security on their code or whatever when they could do the same thing themselves so I think the role of auditors to answer your question is to sort of inform the team about what's available and what they think could be useful for the contract and then it's absolutely the team's responsibility to follow up on that and put the time in often I think the hardest part is just the spin up time right so you you have some new tool that you're trying to bring into your tool chain and then you know it maybe takes a week or something to get it fully integrated and get it to be seamless but once you have that spin up time taken care of then you can kind of begin to make incremental progress so what I would like to see is people taking the case semantics and making extensions of it so we have already several extensions one is a small gas analysis tool that's not very feature full or very complete or sound it just kind of gives a rough estimate but it'd be nice to kind of tighten the screws on that and then there's another tool called EVM prime which is just a small extension of the EVM semantics to a higher-level language and if people wanted to hack on that that would be really cool I'm answering specifically for KTM because that's you know the project I'm working on but there's all sorts of other analysis tools you can write directly in K itself as an extension language and the hard part is the spin up time on K of course but you know there's no there's no avoiding now with a project like that so yeah just to butt in just for one second it would be really nice also if these auditors and these teams sort of complained a lot more about the tools yeah so so far most of the research focused around either talk or Krauser which are relatively smaller size and they off also it's quite similar but as more more companies start delivering the product which they promised today based on the funding the sides gonna be a lot bigger and the product will be quite diverse what would be the challenge when it comes to verifying these actual product rather than I talk in the crowd sales this quick answer because we need to sorry the question was what are the challenges for these teams that are using these tools mostly it's better without the mic actually I think yeah yeah so so yeah that's a great question so the question was about like most of the verification right now is tokens or crowd sales because that's sort of what everyone is doing and it's all the same but what about when we get more complicated contracts I personally think people are always going to sort of push the envelope and do things that are more complicated than we actually can verify and I think that's really cool to sort of feedback in but the more complicated the more experimental your contract is the more time you're going to have to take and the more you're gonna have to consult experts who really know how to write like new specifications and not just reuse those same old building blocks in the old ones I I think auditing make finding bugs in the contract is a bad game to play because you have to beat the best articles in the world so going forward if you try more complicated stuff you will need much stronger usable - otherwise um so I mean the game is not fair you have to find the old holes and a very good attacker should find only one go one poor critical vulnerability so it's very skew it's a very very skewed game so maybe a good tooling or maybe a good game like Hydra is necessary but I think we are kind of ready to that take the challenge rights and thanks very much that concludes the panel like to thank all the panelists like it's a huge honor to share the stage with some of the best researchers in the field thanks very much [Applause] you