# KEVM: Overview and Progress Report

- Channel: [Devcon](https://streameth.org/devcon)
- Date: 2018-10-09
- Duration: 21:34
- Topics: Science & Technology
- Watch: https://streameth.org/watch/yt-tIq_xECoicQ
- YouTube: https://www.youtube.com/watch?v=tIq_xECoicQ

## 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/kevm-overview-and-progress-report

Since the IC3 Crypto Boot Camp, we have been extending the KEVM semantics in several directions. At the time, we only supported the VMTests from the Ethereum Test Suite, it was somewhat difficult to write properties and proofs about programs in EVM, and EVM-PRIME was a simple demonstrative toy language. This session will cover the progress so far in addressing these issues, as well as our goals and intentions for the semantics moving forward. In particular, we are focused on providing tools to ease the process of writing and proving specifications about programs written in high-level languages. Everett Hildenbrandt is a CS PhD student at University of Illinois Urbana-Champaign studying formal methods and programming languages. He is focused on improving the scalability of symbolic reasoning for applications in both distributed and physical systems. In the context of blockchain systems, he is interested in formalizing the semantics of both the underlying languages used and the consensus protocols. To this end, he recently led the KEVM project which developed an executable mathematical model of the EVM in the K Framework.

Speaker(s): Everett Hildenbrandt
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

hello everyone test test yeah I'm Everett Hilton Brandt and I should have put also my group on there but I was kind of in a rush to make the slides because it was all a little bit last-minute but you know that's how it goes and the original title was overview on progress report and then I decided yesterday that more kind of a Kay by example approach would go better here so I figured I'll put that as a subtitle but still leave the original ones so I don't offend anyone or something so we'll see okay so what is K K is this language for building programming languages in and then you get to derive a bunch of tools from it so essentially you give us the formal language definition syntax and semantics and then we derive a bunch of tools for me so ones that are more in the vision phase right now our test case generation and compiler but all of the other tools you see here we actually derived from the one semantics so that means that the tool that you're doing symbolic execution with or model checking with or deductive program verification or you're executing the test set with use all the same semantics there's only one semantics that all of them are using if there's no way for them to disagree on how the execution happens which is important when you're trying to verify the program's have the properties you think they have the Kay backend I'm not really gonna go into much depth on this but the static logic we use for matching configurations it's called matching logic there's some ongoing work on showing that this is a generalization of separation logic and the poly otic modal logics and first-order logic as well and stuff like that so well and when I say generalization I really just mean like there's embeddings into it and then also the dynamic logic is reach ability logic which is this language independent dynamic logic for reasoning about transition systems so go ahead and ask me or the other team members you guys raise your hands if you have any questions about these specific things but I'm not really going to talk about that in this presentation instead what I'm going to focus on is this K by example thing so the organization we have on github is this K framework organization for the KVM repository is a TDM semantics and all of the semantics that we maintain are developed there there are some semantics that other people maintain that aren't within our kind of organization and then directly in this repository we have this directory which has a bunch of toy languages you can kind of play with and get familiar with k so that's a good place to start okay so I'm gonna dive right in and basically this part of the presentation is just gonna be a bunch of K so I'm gonna try to teach you guys K using an example that hopefully people are familiar with which is EBM so we're gonna start off with some basic kind of functional style rules in k here we're declaring a function called chop it takes in an integer it produces an integer so the type signature of this is int int we declare here that it's a function and then we give the rule we give it semantics using this rule keyword so we say rule chop of some integer goes to the integer modulo POW 256 where this is the built in K modulus operator and that only happens if it's either less than 0 or greater than POW 256 which is 2 to the 256 otherwise it just goes to I if it's within those bounds right there so you see that these cover all the cases some other operators we define these are just a fraction of them for them you know demonstrating but for example there's this plus word operator and notice we can define the syntax right here to be in fixed directly so we can say actually something like 3 plus word 4 instead of having to say plus word of 3 & 4 for example we declare that that's a function and then we give semantics to it down here just by calling the built in plus int operator and then calling chopped on top of it notice we also give semantics to division this one has to be broken to two cases where you're dividing by 0 we're an EVM that's defined to be 0 and where you're not dividing by 0 in which case we just call chopped on the normal division okay and also feel free to ask any questions at any time it's gonna kind of ramp up in difficulty as we go so it's better to ask earlier ok so defining data structures in K this is gonna be a word stack for evm and we're gonna define it as a simple cons list so anyone in the functional programming languages will recognize this this is just something that it's a hint or at SM T solver but basically we say that we have this dot word stack right here which serves as the empty element of the cons list and then you can also cons an integer onto a word stack and that also produces a word stack so this can be thought of as a singly linked list and then here's for example word stack append given to your word stacks you can put plus plus in between them that also produces a word stack and then you know dot word stack append some word stack is just the word stack and then some word appended to a cons down to a word stack append a word stack is the word cons down to depending of the tails okay pretty pretty simple functional programming like stuff ok so then in K we have this thing called a configuration which basically specifies the state of our system and that lets us kind of tell Kay that you know there's a bunch of state sitting around that we don't have to want to have to mention all the time but we want to be able to grab it anytime we do need to mention it so here's just a fragment of the configuration the actual configuration contains 60 plus cells a cell is one of these XML like brackets like this and then in the semantics when we say configuration you also supply kind of the default value of each of the cells so this is telling us that in the case L the entire evm program is loaded that's what this dollar sign PGM it's a special symbol is loaded into the K cell at the beginning of execution and then there's a sub configuration called EVM that for example contains the VM execution state so for examples the current executing program which in the yellow paper is I underbar be the current words gap which is me us the local memory mu m and the current gas available which is mu g okay we don't just have the VM execution state we also have the network state so we have another sub configuration so what you saw above is where this dot dot is this is the network state we have a map of the active accounts essentially that map just states whether it's an empty account or an actual non-existent account and then notice we have this accounts cell which is wrapping this account cell which has multiplicity star which basically says you know you can have as many account cells as you want so you know in a realistic EVM network you can have many account cells and then in each account you have an account ID the balance the code the storage and the nonce and these are the initial values down here we also have things like the transact of the current transaction set and a couple other little network state things for instance so like I said the actual configuration contains you know sixty plus cells obviously I can't put the whole thing here and then another thing to note this multiplicity star here people have asked me about you know how can you do concurrency or parallelism or something like that that's exactly how you do it you essentially do a multiplicity star in a cell that's surrounding the case else so for example in the C semantics we have or in the C++ semantics we have we have multi-threading semantics using this multiplicity star or in the rolling case semantics that exists that's one we don't develop they also use multiplicity star for the independent processes that are evolving in parallel okay any questions that's far okay let's get on to EDM executions so before what we saw were rules that we're just defining functions essentially and that's just kind of the functional you know subset of what you can define in K but now we want to define generic tranzact transitions in the transition system so first we need to say well how to perform a single step so we introduce this next operator and in the yellow paper basically what you do is you say okay do a few simple checks to see if this is going to throw an exception like well the word stack be under overflowed will the gas limit be exceeded some other trucks like that and then if not then you execute the OP code and then afterwards you increment the program counter and then you revert the state if any of the above steps through an exception okay so here's the actual K rule right here notice here now we have the same keyword rule but we have multiple cells mentioned back up here right we have rule but we have no K cells mentioned and then we have this function attribute which basically means that anywhere in the configuration this rule can apply but this rule only can apply exactly at these parts of the configuration so what do we do when we see the next operator we replace it with this chunk of code when the program counter is P count and in the program cell the current program so that program counter is pointing to OP and we don't care about the rest of the program note that this dot dot is not me alighting details that's actually what the rule looks like this is verbatim what the rule looks like in the semantics so essentially we use this dot dot to tell K don't care we don't care what's there we just care about that one particular opcode in the program cell so yeah when we go next we say first push the call stack which basically saves a copy of the current execution state then we check is it exceptional this is is it a bad jump operator so is it going to jump to an invalid jump destination is it one of the designated invalid operators there's one of the stack underflow or overflow check if that check passes and doesn't throw an exception then we actually execute the operator which does the memory computation how much memory this is going to change also does the gas computation and also has the effect on the state of whatever this opcode is and then we increment the program counter if any of these throw an exception that exception ends up consuming the remaining of these operators until it hits this syntax right here which basically acts like an if-then-else over exceptions so if there is no exceptions we drop the call stack which essentially forgets the state that we saved up here but there is an exception we take the false branch of this if-then-else which means that we pop the call stack reverting to the previous state and propagate the exception on so this little squiggly arrow can be read as followed by essentially so if you only see a single element right here with this dot dot so this the precedence of this is that this dot dot is outside of the scope of this rewrite arrow then that means there's only a single element and then anything else in the followed by part but we're replacing the single element with several different computations to make does this make sense all right okay so EBM programs let's take a look what they look like in K EVM opcodes here are some simple expressions so we actually been up the opcodes based on their arity essentially so sub and div are binstock ops and we use somewhere else in the semantics we will automatically load the arguments based on the air D so all bins stack offs will get two arguments off the word stack and the word stack will have those arguments removed so sub just goes to - word Dave goes to / push / word and then that's followed by this hash push which is just an internal operator for actually moving the result over to the / - the word stack and then in here's some local memory operators like M load which is a and stack up so it takes one argument so M load had a specific index you go and grab the local memory from the local memory cell and then you say as word the range for the local memory starting at index and going 32 bytes so you take 32 bytes from a local memory pack it together as a word and then you push that on to the word stack because remember the local memory is actually a byte sequence it's not a word sequence here we have a bin stack up M store so M store of this value at this index it's going to take the local memory and replace it with the local memory where at that index you write 32 words prefixed with essentially the bytes of this value so you chop that value up into 32 different words if it's not enough you pad it to the width of 32 and then you write it to the local memory does this make sense okay so the rules are gonna start getting bigger and mentioning more of the configuration notice this only mentions one cell this mentions two so oh and there's one more thing notice here we have to rewrite arrows this is as opposed to a lot of languages which would require that you pull this rewrite arrow outside copy the whole configuration above and below but if essentially K does that for you it pulls rewrite arrow outside and copies you know so you'll have a K and a local man before then the rewrite arrow then a key and a local man with the right hand side of these but okay just pull those out for you so the rule can be a little more compact and readable does that make sense okay so then here's some aetherium Network op codes so S load and store they're the network storage analogues of the EM load and M store so when you s load at an index there's a moon stack up and the current executing account is the one with this ID well first we match an account so remember there's many different accounts because that multiplicity star if we match the particular one that matches the account of the the one that's currently executing and then we look in its storage for this index essentially and we then we push the value up right here and the storage and the account don't change we just push the value up there yeah so it's kind of a lot going on but once again this dot dot is not me alighting details this is actually verbatim the K rule for this operator so once again K is kind of being our allowing us to elide lots of details of the configuration that we don't need to mention for this particular rule s store right here it has once again to transition arrows one that's going on within the account and one that's going on in the case L and then we're rewriting the S store to the empty computation essentially so we're saying that the computation is done we once again match on the account ID grab the account take the storage update the index and the storage with the value and then there's this side condition here because there's a bunch of different semantics whether the key is already in the storage or not in the storage or wasn't empty or it wasn't yeah so this this this arrow right here is actually map update and it ships with K as a built in from the preload this right here is actually specific to the evm semantics because it has to write a whole word stack at a time so it writes the first element then the second element so this D sugars to a sequence of 32 of the map update operations does that make sense I guess I could give it some nicer syntax but I don't know that was an early design decision then it's hard to change later yeah ok ok so I just wanted to show an example of a bigger Network hop code so this is the call-off code it's running off the edge of the screen here but basically we define a bunch of internal operators to help with the call opcode and that's pretty straightforward to do but then these internals can be reused for the delegate call opcode or probably for the static call as well I'm not sure I'm it was awhile since I wrote this code ok so gas calculation I'm gonna run through this super quick because it looks like I'm running low on time and I want to get to the verification part the intrinsic gas calculation we tried to mirror as much as possible to style of the yellow paper so we have this function gas exact which is parametric in the fee schedule that you are executing with so you can specify different fee schedules for example I'll talk about that on the next slide so given the schedule and the opcode call the CS store gasps function from the yellow paper essentially and then this we're going to declare as a function which means we're not allowed to depend on any part of the external configuration so this gas exec operator is gonna grab all the relevant parts of the state that C s store needs to calculate its value and give it gives you a story of those values as arguments so the definition of C F store is right here once again it's a function takes three arguments produces an int and notice it doesn't depend on any part of the configuration so you know you check is the value not equal to zero and the old one is not equal to zero so this has to do with whether you're setting it for the setting or resetting it essentially and then these are different schedule constants so they're parametric in the particular schedule and then these are all sorts of other cost functions that we've implemented these mirror exactly what goes on in the yellow paper so really you can read this instead of the yellow paper if you don't like reading yellow paper and it has a lot more explanatory text around it in our repository online here's how we implement the schedules so we say that you can produce an integer if you have a schedule constant and in these brackets in a particular schedule and then here are some examples of schedule constants once again from the yellow paper g0d base g very low here's a schedule the default schedule you know it sets G zero to zero do you base the to e I p150 schedule G balance gets changed to 400 over the schedule that come before that was like homestead or something I don't quite remember so you just update for each new schedule change you just update the schedule constants for that particular schedule so there's actually a command line flag you can give the semantics to tell it which schedule to execute with okay so now I'm gonna talk about a toy verification example which is the sum to 1 sum to end example I forgot to put what the actual spec is here but it's basically that s is equal to n times n plus 1 over 2 just a classical you know Euler's form I think Oilers formula for sums or maybe you cleared or something and you say enough names you eventually get them all so in no particular language this is kind of the program that we're looking at but in EVM obviously it looks a little uglier so the proof claim this is the main claim right here I'm gonna run through this really quickly but basically we're saying the look like reach ability they look like the the rules from the definition and that's because they pretty much are the rules from the definition and basically what its gonna do is it's gonna start on the left-hand side of the rule notice we have a symbolic value here for the gas and symbolic word stack here and it's going to symbolically execute using the inference system of reach ability logic until it reaches a state that this that implies this right-hand side of the rule essentially so basically we're saying starting at any word stack we get to the same word stack but with the sum from 1 to n put on the top and our counter gets to 0 and the gas consumed is exactly this amount and then we have some preconditions basically stating that like and is greater than 0 there is an integer overflow the size of the word stack is small enough that there will want be a stack overflow and the the gas consumed is the gas available is large enough basically you know we first write down the spec up here and then we try to prove it and then the prover tells us in a not so intuitive way that it can't prove it and then we say oh what are the preconditions we have to add the reason I'm telling you that is because okay so actually with some example there's this loop in traditional logic style things you have to provide a loop invariant we generalize that a little bit and reach ability logic to the notion of a circularity and this basically says if you're starting at the loop head you can reach the end of the program and calculate the correct remaining partial sums so notice in a loop invariant if you're familiar with those you specify the behavior of a single iteration of loop here you specify the behavior from the beginning of the loop to the end of the program which is often easier to specify than the behavior of a single iteration of the loop okay so verifying a VI compliant contracts writing these specifications is actually really hard for ABI contracts because you know they're huge right so we've provided some helper functions like ABI call data and some other little ones which will let you essentially actually pass in the name of the function you want to call or the typed arguments that you want to pass that function for example instead of having to pass in sorry the hex encoded bike string for example and so here's an example usage and say maybe I call data transfer to this address this transfer value note that transfer here as a symbolic value but this is actually a constant so that's the called a to sell and then here you would use it right here this is this would be that line above instead of having to write out the byte encoded hex values here and then notice the balanced one goes to balance one - transferred miles - to balance or to loss transfer and then all these preconditions right here some of them were caught this is this examples hkg token they had a bug in it some of these were caught by the hkg auditors some weren't actually so our prove er was able to help us find some integer overflow bugs and stuff like that okay so not enough time here but basically we passed the tests almost passing large chain tests with an order of magnitude of the performance of CPP etherium which is pretty good for a formal verification framework we're working on some ABI abstraction stuff and not discussed here but come and ask me about it EVM crime which was the ic3 bootcamp project we're extending EVM with some stuff to make it easier to give semantics to Viper via compilation - EVM and we're getting pretty close on that yeah so this is the K framework overview it's not just for blockchain languages and that's [Applause] thanks Everett [Music]