J1 SAY 12 Everett Hildebrandt KWASM Overview and path to KeWASM

I'm Everett Hilton Brandt right there on the screen I'm from the University of Illinois right now I'm working with two different companies on formal specification using the K framework a past project I did was the KA VM which is the K specification of the EVM here I'm going to talk about K wasum but really actually this will be more talk about K because I figure most people don't know what K is and then towards the end I'll talk about applying it to Wasson so let's dive right in and talk about what K is and also if you have questions about K throughout the presentation I think it's better to ask them early because then the later slides will make more sense so this is an overview of my talk first the the meat of it will be this section one introduction to K and then I'll talk a bit about chaos and design issues that I've run into while I've been making chaos on essentially and then I'll talk about using chaos amande have this pseudo demo thing which will really just be me clicking through slides and then I'll talk a little bit about future directions which will be how to expand this to ke wasum and what other things we can get out of K once we have a fully fleshed-out Khaosan so what is the vision of k k did not start out as anything to do with block chains at all in fact the main guy leading K the K efforts didn't even know what a block chain was and it took many meetings of me explaining why this happens and then this happens and consensus is achieved or something like that to him before he even understood it but basically it's this idea that programming language tools should be language independent so you know you might make a new language called D or something well D actually exists and then you can't reuse the debugger that you wrote for C as a debugger for D actually in this case you could because D has compatibility with C but but anyway the point is that you you want to write the tools once and then you want to apply them to all the languages instead of writing a new debugger for every language so the idea is you separate the development of PL software into two tasks the first task is to develop and to design and develop the actual programming language itself in terms of specifying it so there you would have a programming language expert who builds the specification of the programming language gives execution semantics may be typing semantics to it and they don't worry at all about developing tools for the language they just worry about developing the language itself and then the second task is all the tooling around the round of programming language so you know these are some common tools that every programming language should have like a parser you have to be able to read in programs an interpreter a debugger compiler a model checker and a program verifier I listed these particular tools here because these are all tools Kay gives you except for the compiler that one's in progress these are all tools K gives you once you have specified the programming language in the K language see right down your specification of your programming language and K and then you get a parser and interpreter a debugger a model checker and a program verifier out of it so you can ask me some more questions about that maybe offline about those specific tools but yeah this is the basic idea separate the tooling and the programming language so that every tool you build can be applied to every programming language you build and here's kind of a picture of this so there in the center you have your formal language definition which is given in terms of syntax and semantics and then derived you get all these tools around the side so let's see if this works test case generation and compilers are kind of more in the vision phase right now while compiler is in the in-progress phase and test case generation is still in the vision phase any questions about the cave ISM okay we have the semantics of many programming languages I've listed some of them here but there's many many more you can just go to the K framework github organization and look at and there's some that aren't maintained by the K framework github organization but we I mean realistically we do the maintenance of a lot of the big ones so we have C we've had C for a long time we use that for detecting undefined behavior which we've used for verifying code that runs on like I see use in in cars and modern cars that you don't want I see you to have undefined behavior otherwise your car might like to start accelerating or something in Java we can detect race conditions using a tool called Java mop so we have the Java semantics and then we can detect race conditions evm we've used to verify smart contracts LLVM we have actually done compiler validation from LLVM to x86 because via the semantics of both and then we can translate programs between the two and then we can show thereby similar using K JavaScript we have found so we formalized JavaScript and then I shouldn't say we it was another member of the team and he mostly did it alone but he formalized JavaScript and he found that the test suite for JavaScript actually didn't test something like 14 features of the spec and all 14 feature all 14 of those features the browser's had different implementations and so we've submitted those as bugs essentially and they got fixed and tests were added and you know the world was a better place and then p4 I thought maybe some people here would be interested in that one because it's a Software Defined Networking language where you can kind of layout how you want data to flow through your your network of switches or something but then we can do data layer verification about you know whether packets will be delivered or will be dropped or stuff like that so there's many other languages go ahead and take a look at our K framework github organization to get an idea of all the languages we have semantics for okay so now I'm going to dive into what a K specification looks like to kind of get people warmed up with that so this is stolen from a programming language called IMP which we use as kind of a dummy language to show just simple imperative programming language constructs so you use this extended BNF style grammar so here we're saying we're declaring a new sort called X and we're saying that all integers are in sort X and we're saying that IDs which are just like names like a B or a B as one string are also sort X and then we're saying that we can bracket X with parentheses right here and we're saying that we can multiply X and add X and notice here instead of using the bar we use this caret right there and the caret makes it so that this operator will bind tighter than this operator I'll show you an example of what that means here in a second and then we say okay here's the sort statement and one statement we support is variable assignment so you can say something like X is set equal to some expression like 3 times 2 or 3 times y we can also sequence statements using the semicolon operator and then you can return an X so this is just a dummy language it's not so far I haven't given any semantics and at this point if this is all you wrote down all you would be able to do is parse programs like this so this would be completely uninterpreted it would just be parsed correctly essentially so a colon equals 3 times 2 and then this is an example of this precedence thing basically by using this precedence thing it will parse this as 2 times a all plus 5 instead of as 2 times a plus 5 and then return be so simple that's the parsing part of K and let's get more into the semantics part instead of just the syntax so you need to tell K about the structure that your execution runtime kind of has so in the case of EVM this structure consists of the network state it consists of the byte stack it consists of the local memory all these sorts of things in the case of M it just consists of two very simple things we have well three simple things the case L is kind of special it's included in all K definitions basically you don't have to but the fact oh it is so the K cell will contain the initial parsed program initially and then throughout execution it'll contain the remainder of the program that's left to execute basically so it'll contain the frag the continuation of the program the environment cell binds variable names to their locations in the store so you'll say X is located at location three in the store and then the store cell will bind locations in the store to their actual values so it'll say the environment will tell you X is located at location 3 and then the store will say location 3 is storing the value 5 so this is you know the standard kind of pointer the environment kind of acts as the pointers and then the store acts as the actual memory okay and then here we're just telling K initialize this with an empty map at the beginning of execution and we're telling K put the program in this cell at the beginning of execution wherever you put that dollar sign PGM and actually program there should say statement not not program another mistake you tell this sort okay okay so the basis of what K what you do in K is you define essentially a transition a transition system which executes programs in the programming language now you're looking so you just build a model of the programming language as a transition system so here's two example rules here's a variable lookup so if at the front of the case cell what you have is a variable of sort ID and in the environment you have that variable that same variable pointing at this store location and in the store you have that store location pointing at this value then replace the variable in the K cell with the value so here we're doing a big complicated pattern matching thing and it may look like this dot dot is MIA lighting details about the rule but that's actually K syntax so this is saying and I don't care what's in the rest these are called structural frames I don't care what's in the rest of the environment I don't care what's in the rest of the store I don't care what's in the rest of the K cell or what happens after this I'm just focusing this part of the case all which is right at the beginning so if at the beginning of the case I'll I'm trying to do a variable lookup do the variable lookup by looking in the environment and then the store for the correct value and then put the value on the case I'll replace the variable with the correct value does this make sense okay and then variable assignment is kind of the other rule that goes and modifies the store so that you can update you know X is now pointed at something else so if at the front of the case L I have that X is set equal to some integer and in the environment I have that X is pointing at this store location and the store location is currently pointing at V then replace V with the integer this integer here and replace this statement with the empty statement so we get rid of the statement and we do the replacement in memory and now the memory has been updated with the correct value does this make sense okay so one nice thing here that K lets you do is you can split specify multiple rewrites because you called rewrites that have to happen at the same time and it will essentially just kind of pull these rewrites to the top if if we didn't allow that you would have to write the entire configuration twice with the rewrite arrow between the two configurations but you can kind of localize where you're doing the rewriting with K which is one thing that's makes writing these specifications a little more compact okay so do these rules make sense and there's many more rules that go into the IMP language definition and I'm not showing them here but I'll kind of explain them as they're used in this example reduction I'm about to do okay so we'll start off with this program that I showed before a is equal to 3 times 2 B is equal to 2 times a plus 5 returned B and this is the initial configuration you'll get it's not quite accurate I'm kind of glossing over some things here but I'm pretending that the environment already has the keys in it I'm pretending the store already has the memory locations in it so we're gonna say a is stored at memory location 0 which is initialized to 0 and B is that memory location 1 which is initialized to 0 as well and initially the program is this so first we look at this rule this variable assignment rule so you'll see here that the semicolon is what's separating this first statement from here to here and in this slide I've put this symbol right here that's one of the rules I haven't showed you but basically it goes through and takes the semicolons and turns them into this K operator which is built which ships with K which says essentially focus on this part of the computation and store this one for later essentially as what this is saying so we're focused on this a colon equals 6 so a colon equals 6 a becomes this X while X becomes this a I should say this integer becomes 6 and then we look up okay what does a pointed at is pointed at 0 what is 0 pointed at 0 is pointed at 0 so this V is this zero and then we update it to I so the next slide this will go away because this is saying take it to dot which is the empty and this will be 6 and boom it does okay so that's the execution of that single rule in this particular configuration okay the next thing we do and once again I've alighted some details here but basically K will tell you there's some other rules that tell it ok look at this expression for variables and pull the variables out to the front and put holes where they were so that we can kind of focus in on the variables so here I've put a hole where that variable was and I've pulled that variable out to the front so now we're focused on this variable right here so here we're saying focus on a forget about this for a second and here we look at the variable lookup rule so a is the variable and we're going to say okay a is pointed at 0 again that's right there and then this is telling us could get the value no that's at 6 and we're gonna replace a with that value which is what this is saying to do well is replace with that value and then there's another rule that says once this becomes an integer take it and put it back in the hole over here so we do we put it back in the hole so now we can actually evaluate this because it's all concrete so we can actually say okay what is 2 times 6 plus 5 and we do that and that we get B is equal to 17 followed by return B so does this execution so far make sense the next thing we do is once again this variable assignment rule I'm not going to bore you by explaining it all again but you can see there's the 17 and the B is equal to 17 goes away and then I'm not going to show the returned because it's not interesting I just put it there for completeness okay so does K kind of make a little bit of sense here all right and we've used this you know language to build you know really big programming languages like C and Java which are huge languages and here there's there's only three cells in this configuration the C configuration has something like several hundred cells I don't remember the exact number the EDM configuration has over 70 cells so they get pretty big and case scales pretty well to these these sides of programming languages okay so now I'm going to talk about chaos and design and I'm gonna admit that the dis sections a little less developed because I'm still in pretty early phases of making the Khaosan implementation here's where the original wasum spec is available at is that this this github it's fairly unambiguous I think it's really well written it's a very good spec at least better than the yellow paper and it's it has this kind of procedural description that you can use to make an implementation and then it also gives a kind of more formal small step semantics so because k is a small step semantics framework it's really easy to just mechanically translate the more formal notation into the K implementation pretty directly here's an example rule from the specification so this is the rule for a loop so you have a loop I'm gonna actually click this so you have a loop with these instructions essentially and basically the way that wasum works is you kind of put a label on the stack saying like okay this is what the loop was and then you execute the loop and then when you get back to the front of if you get back to the front of the loop without breaking out of it then you execute the loop again so you kind of put these these labels on the stack in front of this label right here with the Curly's and and you kind of put the label in there so that you can kind of remember oh this is where you need to go back to once you're done executing this chunk of code so basically if you have this loop it's going to execute the instructions here first which is just the instructions that came from here and then once it's done executing these instructions it's going to jump to this code here which you notice is the same as this code here so it's going to re-execute the loop again and it will only stop executing this loop using this scheme basically if you have a break in there that breaks out of the loop execution so it breaks out of the labels okay so here's that rule again and now I'm going to show it to you in K now this is all the same information is here but it's presented a little bit differently because and I'll discuss this on the next slide I actually went with a slightly different design decision than the Oise inspected in terms of how to write down these rules basically so here here's your loop with your type we don't really have to worry about that and the instructions right here and then basically it says okay execute those instructions and then when you're done if you don't have a break execute this loop here we have our loop and there's our type there's our instructions so loop type instructions and we're gonna say okay first execute these instructions we're saying focus on these instructions first and then go to the label with the empty type which is what this is zero here represents is the empty type and in the parentheses put loop type instructions end and then here instead of putting the instructions here so the thing about the thing about the wasum spec is that it mixes the instruction stack with the actual value stack you can like push the values onto it and then you put instructions on it and yeah if one of the instructions is like an add instruction it like consumes the two values that are underneath it and produces a new value and puts it on the stack in the K wasum spec I actually have separate stacks for the values and the instructions specifically the case L is the stack for the instructions and the stack cell is the stack for values and because of that I kind of in stead of having this one stack right here which is like the next instructions to execute in the wasum spec I separate it out and I say okay here's the next instructions to execute which are just the instructions and here's this the current stack state which I store off so it actually ends up I would argue making a bunch of the other opcode definitions like break and call a lot cleaner in the case pack than they are in the wazoo spec so I think I'm gonna make a poor request I haven't yet because I it's just in the last week did I come across this but a pull request in the waz inspect maybe suggesting this this cleanup but anyway there's you can see pretty much all the same information here that you have here except this spec is executable as opposed to the wasman spec which is just text on paper yeah and then this is where I'm talking about this one or two stacks thing so basically because you have this stack with values and instructions in it you have to when you do a break off code you have to search through the stack okay where is the next label that I could break to so you search to it and then when you get to that label it tells you how many values from the stack to keep back so you have to go back up to the top of the stack grab those values and then once again go back down to where that label is and put those values in place at that label and in the semantics it has like a whole little section about this this metal level context operator just to be able to explain this concisely and compactly because instead because in chaos and I'm using these two stacks I could just access both cells directly at the same time leave the stack intact without having to kind of scroll through it and look for the label I leave that stack intact and the instruction stack is what I'm scrolling through and I can just forget about all the things that I've scrolled through so far so a little more efficient - I don't know what the actual interpreter is doing for this but I assumed it was following the spec pretty closely but I'm not sure either way the wasum the Khaosan implementation i think is a little bit cleaner than the wasum specification so I know we'll see we'll see if it we'll see if it works out okay another thing that I and I thought was an interesting design choices so you know I was like okay I'm gonna make the Khaosan semantics right so I I get the old Camel interpreter and I fire it up and I'm like okay I want to push some things onto the stack great and I go to push some things onto the stack and it won't let me because you have to define a module first right so you define a module that has your function that pushes things onto the stack and does stuff with that and that all sounds like not really necessary to me it'd be nice if I could just start pushing things onto the stack and doing operations on it so the Khaosan is kind of designed a little bit more incrementally so this right here is a valid khaosan program it can just execute program fragments which i think is kind of a nice thing for beginners who just want to start playing around with it really quickly instead of like the oh camel version which you have to actually make a valid module and then call a function in the module and then see its effects it no it's just a little bit or the there's some online one that I tried as well that also had that problem so there's another design choice I made so early-stage benefits of K wasum I've discovered one bug in the spec that I filed and they fixed so far I have a couple other bugs written down that well I think they're bugs but we'll see what it is so this is just a benefit of any formalization of anything you're going to find bugs basically I've maybe come up with a clear presentation of the control flow semantics at this point I'll have to kind of wait a little bit to make sure that it ends up working with the rest of the semantics being finished and I have an interpreter now that allows experimenting directly with kind of program fragments instead of having to make an entire valid was a module at a time you can just kind of use a little program fragments at the time so these are kind of early-stage benefits all right so now I'm gonna do the pseudo demo are there any questions about the what I've talked about so far okay so pseudo demo time these are the steps you would have to take first to be able to do this you clone the repository change into the directory make depp's downloads the correct version of k and builds it for you make build will actually take the specification and build the reference interpreter as well as the symbolic execution engine for you [Music] so k wasum is the main runner for k wasum this little file so you can do chaos and help and it will tell you all the things you can do so there's a run command a debug command there will eventually be approved command but I want to wait until I've proved some things first before offering up and then there's also a test command but that's more for my continuous integration testing servers so you probably won't need that okay so this is the program that I'm gonna do this little pseudo demo on and the one I showed before and basically you would just say k waz and run program 1 dot lost and this is what it would generate it would say ok the K cell is empty so execution has finished and the stack ends with a single element of type I 32 value 9 which makes sense because you're adding 4 and 5 here ok so pretty straightforward to just K walls and run that and then maybe K walls and debug would also be interesting to some people because this is really good for when you're developing a semantics and something's not really going how you expect and you're like why is it not going how I expect well then you just load it in the debugger and it will show you the step that things are going wrong at so k waz them to debug program 1 dot lost and then it loads up this debugger this prompt here and you can say s or step 2 take one step and then you can say P or peak-to-peak at the current state so the current state is okay I'm about to execute this off code I've forgotten about this part of the program for now and the stack is empty and then we're going to take another step we're going to peek again and it has actually Hugh did that opcode and this is the rest of the program right here that it needs to execute that makes sense and then we're gonna take another step in peak and notice here it did it took this space operator which separates opcodes and turned it into the focus on this part operator so now we're focused on the five and now I'm gonna tail it to take ten steps and it only actually ends up taking four steps until it reaches a final state which means that no more execution can happen and that final state is the same final state we got when we did this kay walls and run it's the same final state here that you get here does it make sense okay so you get this debugger I didn't write this debugger it's just you know because we have to see semantics you can debug C programs now with this debugger we have the Java semantics you can do both Java programs so it's language it's a language of dependent debugger okay future directions I don't know how I'm doing on time I'm probably a little short okay so that's okay you guys can get coffee earlier take a nap I don't know so the semantics are really early-stage still just this week I figured out all the control flow stuff and knee and the the issue I was talking about the one stack versus two stacks thing earlier so I think control flow should be largely done at this point and I have on paper how I'm going to do the frames and local semantics so that will enable me to do call and return off codes there's a couple bitwise operators that haven't been done yet I haven't done anything floating point because I figured that's not an awesome so I don't really need to focus on that at first and anyone in verification will tell you floating point sex I haven't done tables memories or modules but I don't foresee those being particularly challenging and they'll just be kind of you know grinding it out type of things and then eventually we want to you know take the K wasum semantics and 4ke wasn't from that really the only difference as Alex was saying earlier is that we have this gas metering contract and some other system contracts so one thing that might be interesting is we could give a direct semantics to gas metering which is what I think Alex was calling runtime metering before and if we give that direct semantics and k2 gas meeting we might be able to verify that the gas metering contract actually does the same thing as the direct semantics for gas metering which would be cool because the direct semantics will probably be more human readable but the gas metering approach is more performant and has other benefits including being able to run on a normal Watson interpreter instead of having to have a specialized that you want an interpreter so maybe that's a future direction we could go that's that's kind of what I'm leaning towards right now once the walls in spec is done and then the other future direction is of course verification so right now we have a bunch of verified EVM contracts on this github repo so a runtime verification is the company kind of driving Kay framework development and this is the repository that has a bunch of our verified EVM code so we'd like to add a bunch of verified ke wasum code as well or he was encode as well to to kind of give back to the community if you will okay so benefits of the key approach you know many tools already exist so you know you don't have to write a verification engine for your e wasum because we have one and this verification engine is fairly powerful and it's automated it's not an interactive which some people see as a drawback some as a benefit so you know it's it's up to your perspective and then also just making an executable specification that's you know essentially a clone of the wasum specification is clearing up issues with the current walsim specification which is the same thing that happened when we made KVM as they were kind of I found some issues with the yellow paper as well and we talk to people about when we I think filed some issues I'm not sure also with with like kgs for example we found issues with the specification and with the test sets and that's when I talked any questions [Applause]