Towards Imandra Contracts: Formal verification for Ethereum

Transcript

well thank you very much it's a pleasure to be here and grant passmore in my co-founder dennis ignite ovitch here in the audience thank you to a italic for the invitation so we're going to talk to you today about our formal verification platform and mandra and a particular something we're calling a mantra contracts which is the application of a mantra to etherium smart contracts both to analyze smart contracts reason about them be able to prove properties of them compute proofs and counter examples and then on top of that to actually do risk management so I'll tell you what I mean but for those and investment banking we mean you no compute Greeks and so on so let me start with a video that gives you

a background on what we're doing at aesthetic integration see if the sound I'll start it over here we go yes thought was the best of an issue Paris I made it alright so that gave you a bit of an

overview of what we're doing at aesthetic integration the big idea is we're bringing the hard science of formal verification techniques that are relied upon already in safety-critical industries like avionics and hardware design finally to finance so that financial algorithms things like dark pool matching logics exchange matching logics market making algorithm smart order routers the type of algorithm that is really at the heart of our global financial infrastructure so that they can actually be analyzed rigorously and reasoned about so a bit of our background so Dennis formerly was the head of the central risk trading desk at Deutsche roughly I believe nine years at Deutsche by the way we were undergrad

roommates in Texas and then as Dennis went to Wall Street I went to academia did my PhD in formal verification in particular the real loud to break geometry for reasoning about autopilot algorithms and being able to prove safety properties of autopilot algorithms in avionics in now and self-driving cars and ended up as a postdoc at Cambridge well Dennis was working at Deutsche and we realized we were working in many ways on some of the same problems he had very complex trading algorithms that constantly everyone was worried you know if we commit a line of code is this change all of a sudden going to cause us to violate a regulation and it's very hard to get right if you think of modern market

microstructure something like in exchange trading than you in the US for instance it may have upwards of 20 30 40 different order types in each of those order types effectively it's a way of packaging risk it's a programming language and as you introduce new order types it's very difficult by hand to understand what can possibly go wrong so when it comes to smart contracts really we have the same issues so if i come to you and say look I promise you know this piece of bytecode really implements fair escrow please send me your assets how do you know likewise if I say I promise this implements a swap that we've agreed upon how do you know you can't ultimately trust the result or the design of a given smart contract

without reasoning about it without proving theorems about it's possible behavior so what we've done is we've taken our mantra engine which I'll tell you about for reasoning about financial algorithms and now we've adapted it in effectively two different ways i'll tell you about one that's reasoning about a high-level language that can be compiled down to a theorem bytecode and the other that effectively is doing something called verified d compilation that takes etherium bytecode d compiles it to IML or high-level functional language that's actually a formalized subset of o camel if you know camel allows you to reason about it and push the proofs back down to be proofs about bytecode so okay that's reasoning about individual contracts but as I mentioned fundamental importance as you know a bank who's a

pioneer right now with let's say athyrium is there looking down the road three years from now what happens when they have a portfolio of 100,000 smart contracts right you have to do risk management in the large you have to compute Greeks and to do that you have to reason about the code so you must have effectively formal semantics that ultimately is mechanized for reasoning about your smart contracts so let me tell you a bit about how a mantra is used currently so our biggest focus has been something we call a mantra venues and this is using a mantra to formally analyze the matching logics behind trading venues things like stock exchanges and dark pools so you may have

heard about many glitches in the past few years for instance bats failed trading its own IPO of course famous Nasdaq Nasdaq glitch with Facebook night capital goldman sachs alphabet trading glitch these happen all the time and finance and fundamentally what's been missing is a way to reason about the algorithms in advance of their deployment so a mantra venues is now currently get use at top five global investment banks effectively to take what is classically an imprecisely described algorithm their collection of matching logic that is usually described say in some collection of PDFs you know there there is classically no formal spec of how these

things are supposed to work but it's actually taking those ambiguous sort of in precise specs making them precise in a mantra reasoning about fairness and safety properties and then using a mantra to vet their high-performance production systems to ensure that the production systems really correspond to verified specifications so there's also some exciting developments we have in the regulatory space so just to say we came out of stealth mode with this an april and the sec brought us to washington DC to the sec headquarters to teach them about a mantra for two days and some exciting developments will be announced soon on a mantra in the

regulatory space but fundamentally regulators face the same issues someone comes to them and says I'd like to add this new order type to my trading venue ensure for me that you know this is allowed and the SEC then has to process these things and you know so so does the FCA and other global regulators and it's virtually impossible to do by hand without formal verification so what is a mantra I'm going to give you very low-level demos of a mantra this is a very technical audience so i want you to see really in action and i want to talk to you a bit about the automated reasoning and mathematical logic that's under the hood but fundamentally it's three things in one it's a programming language so it's a formalized subset of o camel if you're familiar with o camel

in the ml family of languages functional language it's a mathematical logic so fundamentally every data type definition or every program they to find every function you define in a mantra is automatically transformed into an axiomatic representation that then a mantras reasoning engine reasons about so you write code and questions that you would like to ask a mantra about your code in a mantra works to produce proofs or counter examples using many different types of decision procedures and I'll talk to you more about them so that's the big idea what I just outlined effectively you give a mantra your

financial algorithm or your smart contract and ask them onto a question you know is there a potential glitch of this class or does this do some concrete form of unfair trading for instance is there some sequence of messages that could be sent to this trading venue that could allow someone to jump the queue right and ultimately you get out either that the algorithm is verified with a mathematical proof that can be independently vetted or you get a counter example so that's that's the big idea pushing pushing these questions into what are called decidable fragments so that this is automatic so let me show you a very simple example here we have on the left if you can read it a summation function just in a mantra so

you may this is just summing up the numbers from 0 to n the natural numbers and it's a program so on the right we're just computing with it right we can compute some 5 some of 100 but you may remember this possibly apocryphal story of Gauss's a six-year-old proving actually that the sum of in you know some of 0 up to n is equal to n times n plus 1 over 2 so we can not only define programs but we can write verification goals and what we've done here is we've asked Timandra tactical part of me to actually verify this statement on the left to verify we named it Gauss we asked amarjit to prove for every possible input in if n is greater than or equal to 0 then the sum of n is n

times n plus 1 over 2 so Ahmad rhythm goes and does a proof by induction and etc we can see a trace of that proof great proof by induction as you might do by hand and ultimately has to do some symbolic rewriting that proof can be exported can be verified by an open source proof checker so you don't have to trust it but now what happens more often of course is we have bugs in our code so instead here I've swapped a plus for a minus right and I'm asking a mantra instead to prove that some event is equal to something really that it's not equal to and a mantra comes back and gives me a counter example so that's a super simple example but let me show you something more complex so I believe I don't have too

much time but for instance here's an example where I'm effectively defining algebraic data types and I'm asking a moderate to compute some complex counter examples for me and again you know it comes back and always the counter examples it gives me those are valid IML they're valid o camel objects they can be reflected into the language and computed with so the same idea now can actually be scaled to reason about financial algorithms so for instance we can take the design of a dark pool which I have on the left here fairly complex matching logic this is of a global investment bank top five investment banks dark pool and now we can reason about it so by the way this is all based on publicly available information don't

worry so now for a sense i can ask a mantra yeah is the order ranking function transitive right so that's something we really care about a fairness property so i can ask them on through this question it has a model of the matching logic on the right that's also a high-performance simulator and a mantra comes back and synthesizes for me a counter example so now i have concrete values of different orders effectively that could exist in the book of this dark pool where the ranking function violates transitivity so that's the main idea proofs and counter examples so let me quickly cut to the chase for athyrium so what we've done here is we've taken a mantra and we've adapted it so that in

IML in this fragment of o campbell you can directly write smart contracts so there's many things to talk to you about how we actually do the compilation so right now we actually compile effectively your customized smart contract code via serpent we compile it first to serpent and we have different encoding mechanisms for how we encode algebraic data types recursively but now we have this smart contract let's say for a crowdfunding example and now we can ask a monitor to reason about it so for instance we just had a mantra prove that in this smart contract you effectively can't jump the queue in a certain sense and then we ask another question effectively that we will always

get our money back if we come in after a certain time out and a modular computes for us a counter example where that fails so that's the big idea I think I need to end here but we have these different modes effectively you can go IML directly to bytecode by a serpent reason about your IML or we can use our etherium to IML verified decompiler so sign up please if you'd like to join the private alpha and thank you very much okay okay oh ok well that's okay I mean if there's any questions okay yes so are

you saying we can write smart contracts in oh come in I exactly in IML so I ml it's not all evoke camel but it's you know polymorphic hemming milner fragment of o camel for instance it doesn't support exceptions so that's a that's a fundamental difference but instead of exceptions you use you know things like option types yeah but yes that is pretty awesome oh thank you but part of me it's not it's not so effectively we have a reasoning as a service API we have an online web interface and we have an open source proof checker so you can always you don't have to trust the proofs the hard part is finding the proofs you know

the easy part is checking the proofs so currently it's not open source though I'm sure we'll open source pieces of it over time do you mean use a mantra to reason about a mantra yeah yeah it's a great question so there's there's you know sort of architecture of a mantra there's some bootstrapping in a mantra that is not written in a mantra that's written in let's say raw Oh camel see but then most of a mantra actually is written in a mantra after this bootstrapping so we've actually done some self verifications I mean you know you always have these fundamental meta mathematical results

that if you want to prove ultimately consistency of your own system you effectively need to add you know something like trans finite induction up to a larger ordinal so actually a mantra is logic it's related to a logic called primitive recursive arithmetic of Scala but it's typed and but then we have transplant out induction up to an ordinal called epsilon zero so basically that means we can you know synthesized in do termination proofs of functions that you know effectively recurse in some complex ways but so what you would have to do because we already have that strong ordinal in the logic you'd have to add a transaction principle up to a bigger ordinal but you can you know so proof theorists have have isolated

effectively the ordinal analysis of theories like this so you could do it and actually try to prove soundness properties of a mandra as a whole but one of our really driving philosophies has been we always just want our proofs to be independently checkable as well so when we produce a proof object ultimately you can use a simple checker to check that proof object or if we produce a counter example it's an explicit you know value of a given type that you can run your system on so in either case you don't have to trust us but we have a lot of ideas where you know we would love to talk to members of the community who are interested a lot of ideas of effectively attaching this type of evidence directly to smart

contracts different ways that we can you know actually have an API where you can easily query what is known about this contract what's been proved about it what's been disproved also you know there are times you need to prove limos before a mantra will you know actually prove your main theorem you know happens all the time for let's say you know very deep properties and there we imagined you could have you know sort of bounties where you want to give someone you know some some number of credits if they prove this limo for you that you relied upon so there's lots of cool things I think we can do community wise flash crashes are either generated by fat fingers or like

downward spirals we're algorithms are forced to sell because other algorithms are selling and so you just get this very very quick negative spiral down like how Adam Andhra help in either of those two cases oh great question I mean fundamentally there's a number of answers so if you look at what has happened so first of all flash crashes happen a lot more often than you know we hear about in the press right these happened at a micro level happened at a micro level it is not uncommon and a lot of work has been done effectively having things like risk specialized risk gates specialized circuit breakers that are effectively you know trying to act as an arbiter to make sure that things don't get out of control so first in some of

our clients now the first thing they actually do is they use a mantra to reason about their risk a component before they go in reason let's say they have an order router before they start to reason about best execution of their routing they may use a mantra first to prove that their risk a component which is just this last piece that that it effectively won't let something crazy out the door so you can effectively incrementally verify the circuit breakers these risks gates get those safe first and then start to verify more pieces that are you know more algorithmically interesting so did that answer your question okay thank you very much

thank you