# Imandra Contracts   Formal Verification for Ethereum - Dr. Grant Passmore and Evgeny Gokhberg

- Channel: [Devcon](https://streameth.org/devcon)
- Date: 2017-10-09
- Duration: 15:26
- Topics: blockchain, smart contracts, distributed ledger, Science & Technology
- Watch: https://streameth.org/watch/yt-ejHOff-WYtw
- YouTube: https://www.youtube.com/watch?v=ejHOff-WYtw

## 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/2/imandra-contracts-formal-verification-for-ethereum

A presentation covering Imandra Contracts, Aesthetic Integration’s cloud-based formal verification system for Ethereum.

Speaker(s): Grant Passmore, Evgeny Gokhberg
Skill level: Advanced
Track: Developer Infrastructure
Keywords: cloud, evm, tools, proof, demo, finance, risk, audit, bugs, interoperability

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 2 was held in Shanghai, China on Sep 19 - 21, 2016.
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

you hello hello oh thank you very much it is an honor to be here and I have a part of me I have to second yo yo chewy your shoe ease statement that this is a dream for a formal verification engineer I mean the amount of interest in the room in this beautiful field that those of us who have you know devoted a lot of our professional and you say personal lives too it's amazing to see so much enthusiasm so I feel very fortunate to be a part of this group we're such great work and awareness is happening around formal verification static analysis and so on so I'm very excited today to launch our a mantra contracts platform which is formal verification in the cloud for smart contracts initially targeted for etherium so what powers a mantra contracts is our formal verification engine that will talk to you about call Timandra but what we've done is we've taken the etherium virtual machine and formalized it within a mantra given a full bit precise operational semantics to the instruction set of the etherium virtual machine and then from that we're able to build a stack of tools that work at many different levels powered by techniques such as symbolic execution something called principal region decomposition and ultimately both automated an interactive proof so I'll walk you through many details show some examples and then I hope we can do lots of demos because there isn't that much time but please find me if you're interested in sign up so before I get started I want to show a two minute video that give some background on what we do at aesthetic integration and really how we got here so now I will hand over to Hudson because I think he has to man the sound thank you what's plaguing today's electronic financial markets the world economy is built on a staggeringly complex tangle of algorithms competitive pressures and economic recession have contributed to increasingly opaque and unstable markets the effects of glitches and unfair advantages can be devastating cratering the confidence of investors and ultimately hurting the general public regulators and the industry have worked tirelessly to define what safe and fair markets are what's been missing is a way to analyze and regulate all of the algorithms underlying the solution is formal verification the science of correct algorithms other safety critical industries already rely on formal verification to make their algorithms say the mandra by aesthetic integration is the world's first formal verification solution for financial markets consider the building of a bridge a design flaw may be catastrophic to make it safe engineers use powerful computer aided design tools which analyze designs for safety automatically powered by latest advances in artificial intelligence computer science and mathematics a mantra brings unprecedented rigor to the electronic financial markets analyzing the safety and fairness of algorithms before they're deployed financial algorithms are unfathomably complex they can be in a virtually infinite number of possible states examining 100 1000 were even 100,000 test cases isn't enough we must consider every possible case to answer definitively what can possibly go wrong a mandra allows designers and regulators to fix breaches of safety and fairness before they affect markets let's build safer more reliable and regulatory compliance systems that all of us can trust saving everyone time and money a mandra by aesthetic integration the logic of financial risk alright thank you very much so just a bit of background we are aesthetic integration and our work before etherium and you know also worth that continues vehemently has mostly been with financial algorithms like dark pools matching logics exchange matching logics connectivity layers for instance between venues and different trading systems so we have worked with a number of top investment banks on formally verifying regulatory properties of their core infrastructure algorithms last year after DEFCON 1 something very exciting that has really been a huge catalyst for us in growth is we won something called the UBS future of Finance challenge so this was a global competition between 620 companies 52 countries and we ended up winning the whole thing and I think a major reason was we took the design of UBS is dark pool and actually analyzed it for regulatory properties showed how certain issues that were settled with the SEC could be found automatically and many related things so also at the sort of middle of the summer a little bit before we finished what is to our knowledge as the world's first formally verified dark pool design for a major investment bank where we of course in the process fixing many aspects of their system were able to prove 114 fairness and safety properties ultimately about their collection of order types and we recently closed our seed round backed by Google's chief business officer Philip Schindler which is leading to some very exciting things of getting formal verification out to the masses and democratizing this technology that has up to now been quite arcane in many ways so my co-founder Dennis he was head of the central risk trading desk at deutsche before we founded a I and my background so I did my PhD in formal verification at Edinboro a lot of what I did was around something called an smt solver called said three so I co-authored a lot of the core mathematics of Zed three nonlinear decision procedures and then went down to Cambridge as a postdoc working on safety and fairness of collision avoidance algorithms and then we realized we could apply many of these same techniques to financial algorithms so we all know the problems that are motivating formal verification being taken up in our community so I don't need to belabor those but there are some other aspects that haven't been mentioned at least that I've seen and in addition to the need for automated auditing tools around correctness fairness and safety of course mitigating subtle bugs and so on we also need fundamentally robust tools for risk management so I'm talking here for you know those of you at an investment banking where you have exposure you know imagine an investment bank goes all-in on etherium and five years from now has a hundred thousand smart contracts in a portfolio what is their exposure how do you calculate risk how do you price for instance derivatives and structured products that are expressed as ultimately athyrium by code and that's another place where we see formal verification as being utterly crucial so some of the things we're building on top of our formalized EDM in a mantra are around exactly this risk management calculating Greeks and market exposure linked directly to the semantics of the bytecode so mandra leverages a number of recent breakthroughs in formal verification smt which is powerful automated proof techniques combining SAT solvers what really powers formal verification for hardware combining those techniques with richer mathematical theories things like reasoning about arrays and bit vectors and nonlinear and linear inequalities and so on model-based automated induction plays a huge role so when you have algorithms that ultimately iterate or you know when it when expressed in a logic may be expressed as recursion you typically need to prove theorems by induction either by techniques like you know writing out inductive invariants as we saw with the work of Christian and your Chewie with y3 or with proving inductive limos that then get used for instance as rewrite rules these are all bread and butter for formal verification but we now have much more powerful tools for for instance using counter examples to help us guide the way we inductively generalize which is something you often need to do when proving theorems by induction but fundamentally what we're doing with the Amanda cloud is aiming to really democratize access to these techniques and make them usable to developers and non developers alike we all need them and need them to be easy so fundamentally you give a mantra to things a smart contract let's say expressed as a theory and byte code for instance and a property you wish to verify and a mantra will work to either give you a proof of that property or work to show you a counter example where a property fails and then there's I'll show you many ways that you can get involved in that process and interactively work with the mantra so a mantra is a programming language a mathematical logic and a reasoning engine all in one it's a formalized subset of a functional language called o camel crucially when designing a mantra you know we set out to design our dream formal verification system and one of the most important things is having first-class counter exam so in a mantra we're always working to find counter-examples to false conjectures and actually reflect those into the runtime and into the logic so that you can compute with them which is which is really crucial so there's see I really don't have much time so I want to just show you probably impossible to read but this is a little bit of a walk through of our formalized to theorem virtual machine and a mantra and the way you formalize this because a mantra is logic is also an executable programming language you actually just feel like you're writing a simulator for the virtual machine writing an interpreter defining precisely the memory model the storage model all of the instructions and how those operate on the state and then ultimately there's a top-level state transition function and then finally that's iterated right until you run out of gas or reach an exceptional halting state or you halt in a nice way so in a mantra by the way we are releasing our EVM model under a patchy 2 point 0 and so our hope is that the community will manage this port it to other systems and it can be something that evolves as the you know design of etherium evolves but what I'm showing you here now this is a very very low level interface but I've loaded into a mantra the model of the etherium virtual machine I've also loaded in some bytecode those are now in the runtime those of you who know o camel will see that this looks just like you're at a no camel top-level read eval print loop but actually everything you write in this language is also reflected into mathematics and you can then reason about it so I'm now asking a mantra here to decompose the state space of effectively the virtual machine interpreter running that piece of byte code and what's this what this is doing it's ultimately using something called symbolic execution under the hood but it's telling me the possible behaviors of this piece of bytecode with respect to the actual semantics of the instructions so this tells me that actually this piece of byte code which is for a simple name registry it only has two possible behaviors with respect to arbitrary symbolic storage and one behavior it would go tour execute at program counter 17 if it doesn't run out of gas and it would update the storage in the other behavior it's I believe would halt you just told me it would halt at eight and would not update the storage for instance so now I'm actually let me see if I could pause this for a second and we have two minutes you can't read it unfortunately but these are theorem statements about the execution of this bytecode so these are the formal specs of how this name registry should work and we're asking a mantra to prove those for us and it does which is great directly about the meaning of the bytecode so not at a higher level but really at the actual byte code that will be executed on the EVM and now we're asking it to prove some things that have mistakes and what happens is in this case we can ask him andhra to show us where it's proof attempt failed and then we can ask a mantra to also mine that for counter examples but these are very useful for understanding these what we call sub goals for understanding why something isn't true so I don't have time to go through this this is a higher level so we have a higher level language that is a subset of Madra subset of o camel that we can compile to the EVM and so one of the things we're working on is proving the correctness of that compiler with respect to the EVM semantics so hopefully we'll finish that by the end of the year but I wanted to show you these region decompositions like I did of the possible behaviors of that piece of by code we can scale this to you know very complex algorithms so this is smart contract encoding effectively the matching logic pricing function for an exchange and we asked Timandra to decompose it state space it told us there's actually only 107 different possible behaviors and now I can go through and we have this hierarchical tree representation as a Peroni diagram that's interactive you can go and experiment and see what are the different symbolic behaviors of this function with a map to its state space and we're getting on the right you can't read them unfortunately but constraints on the input that would cause a certain output and these are all expressed symbolically and so now we know even though this has an infinite state space the system itself only has 107 possible symbolic behaviors so we have a new website that launches today you can go to its wwm Andre I and it is if you click on image or contracts you can sign up and we're adding a certain number of people each week as we scale up but effectively it's a mandra now in the cloud running in google cloud with something called codenvy which uses eclipse che and number of things to spin up docker containers for you and have a mantra so I see I'm out of time but anyways we are building the stack also with a smart contract auditing API and finally thanks to our incredible team and I hope all of you will get involved and the community can can really make use of the mantra and join us at a Monterey I thank you thank you now Oh