A Brief Introduction to K, KEVM, and KWasm

Transcript

okay next up we have ever net Hilden brauch who works as a formal modelling verification engineer at rum time verification and will he will be talking about ke ke V m and K wasps everyone make sure it works yeah there's my title slide Ricard has been helping me a lot on the Khaosan semantics so I'm going to be talking about well K briefly at first and then kV I'm very briefly and then K wasum and then actually also talk a little bit about how we do formal verification because there's actually

surprising not an interest in that here which was very pleasant for me Ricard is over at Chalmers University he's not here and I'm at runtime verification Inc and also at the University of Illinois urbana-champaign so there's our overview of the talk so this is the k vision and the idea of k is that you should write down the semantics of your language once and get all the tools derived from it correct by construction from that so this is kind of a going to be a programming languages formal methods talk currently we have the semantics of a lot of big languages C C++ is in progress Java JavaScript solidity is in progress we have Python EVM LLVM x86 the list goes on and each of the tools that

we derive for it come from the same semantics so you can be sure that they all agree on how to interpret that particular language so currently we have the interpreter parser deductive program verifier model checkers symbolic execution engine semantic debugger and the compiler and test case generation tools are more kind of in the vision or prototyping phase and so this is just kind of reiterating what the last slide said but gives you some links or some citations for where you can look at some of these semantics or some of the tools and this list is by no means exhaustive so a case specification of a programming language comes in three parts you first have to specify the syntax of your programming language so we can build a parser for programs in your language and

then you have to specify the runtime configuration or the runtime state of your programming language which actually just it's d sugared into more syntax declarations and then you have to define the transition system which makes a small step operational semantics for your programming language and we call those rules so here's an example of a syntax it's kind of in this ebn F style and then we derive the parser for you from this so using this we can parse a program that looks like this just a is set to 3 times 2 and B is set to 2 times a plus 5 return B but there isn't any semantics of this programming language yet because all we've given you is a parser so all we can do is parse it and say yeah parsed worked out here's an AST next you have to tell us about the

runtime structure of your language so you want to set up some sort of some sort of state that you can access and you can store things in so you can do your executions so think you know for C this would be like the C runtime or something like that the K cell in this example for this little dummy programming language for this talk will contain the continuation or the remainder of the program to be executed the environment cell contains bindings of you know this variable stored at this memory location and then the store cell will contain bindings from this store location so like this location and RAM goes to some number and like 3 or something like that so here are some example rules or transitions in the transition system so a variable lookup

is one that says okay if the next part of the program that I have to process is just a variable X then go to the environment and look up where X is pointing out in the store in the environment this SX location then go to the SX location in the store and grab the value V and then replace the variable X and the K cell with the value V so you can see there's a little rewrite arrow that says actually do the update variable assignment says if I'm assigning to the variable X some integer I then once again go through the environment go to the store find the current value throw it away and replace it with a new value for the variable so originally I had a big long example execution but I'm just going to go through one step here because kind of a

short time so here's our variable assignment rule again and this is maybe our current configuration so in our current configuration we're going to set a to 6 and and the rest of the computation is kind of behind it on the K cell but our current environment has a pointing at location zero be pointing at location one and in location 0 we have the value 0 and in location 1 we have the value 0 as well and so if we apply this rule this variable assignment rule will see that X is getting bound to a is getting bound to 6 and so then if we look up you know X points at SX ok so a is pointing at location 0 and location 0 is currently pointing at value 0 so the update that will happen is now in the store at location 0 we're pointing at 6

so now the variable X has been assigned to our the variable a has been assigned to value 6 so kind of really brief don't expect you to fully understand it but if you have more questions grab me after the talk ok so really even briefer here's KVM it's an implementation of the EDM in K it passes all the VM tests and all the tests in the directory blockchain tests last general state test for some like 40,000 tests there we are almost as performant as the CVP aetherium implementation which is pretty impressive if you think about you know this is an interpreter derived from a formal specification and the jello paper is derived directly from the KVM repository so it's like a our version of the yellow paper so you can use it as

well as the yellow paper as a specification of the EBM in terms of verification because that's what everyone is interested in is the verification we use KVM commercially at run time verification to do smart contract verification and audits it was been used by DAP hubs successfully to verify the make a lot of the maker contracts so single collateral die core contracts and now they're working on the multi collateral die and they have done a lot of work they've made this K lab interface on top of K which makes it easier to use K so if you want to do any verification I would really recommend looking at that and you can look at some examples of some of our verified smart contracts at this repository here ok on to K wasum because that is the future so

k wasum the webassembly is we're thinking of you know replacing the EVM with webassembly because it's you know a little better design and kind of has other use cases outside of blockchain so all these things are really nice about web assembly the spec itself is fairly unambiguous so it's really nice compared to the EVM spec which kind of you have to jump back and forth through different parts of it and you look at this symbol and you're like oh the symbol isn't telling me anything about what it means so it's kind of hard to read but the wasman spec is a lot easier to read here's an example of a rule in the woz in spec which is the looping rule so you know I don't expect you to be able to read it but just trust me it's nicer than the EVM one and then

here's a translation of that woz and rule into the into K basically and then the thing I want to point out here is you know there's some shuffling around of where the different things show up but basically all the same data is there so we're able to do pretty much you know one to the wasman spec presents things in this nice kind of operational small step semantic style so we can pretty much do a one-to-one translation from the waz inspect to the K spec which is really nice there is a design difference between the woz and spec in the case speck in the waz inspect they mix the instruction stack and the value stack so it's all just one stack that you're operating on and in the case spec we separate it out so we have a stack which is our value stack and we have the K

cell which is our instruction stack or continuation if you're curious about why that is I mean it does make the semantics nicer but I can show you specifically why it makes it nicer after the talk another thing is that we gave Kay woz and semantics incrementally so we can actually execute fragments of programs I launched up some various wasum interpreters and online woz and you know try woz and now type of things and basically every time you want to try woz and you have to make a full module or something like that and that was kind of annoying to me I just wanted to do like push push add or something like that so so here's an example of a program that you can execute with chaos and but a normal woz and interpreter won't execute so that's kind of exciting I guess and then here's a list of things

to be done we're skipping the floating-point stuff because he wasn't doesn't care about floating-point so yozma is specifically cable is specifically wasum with floating-point and other non-determinism removed and some metering and stuff like that added we haven't done tables yet and we haven't done full module semantics yet and here k ewaz them you know it strips out the floating-point stuff but it just adds this meter which is actually still expressible within wasum because they had this functionality called host functions so and talk about that later as well okay so everyone seems interested in the prove er I just want to remind everyone the prover is not the only tool you get out of K but that is kind of the most fun tool I guess and so I wanted to show

this proof system this is these are the inference rules that the prove our uses to do logical deduction and proofs about your programs most of the rules are kind of what you would expect we have reflexivity in the top left corner which just says you know if you're trying to prove that a or each is a then you know it's just provable transitivity let's you kind of string together each ability proofs to make larger reach ability proofs but there's kind of this interesting thing here on the right-hand side of transitivity where we have this this see these this set of circularity x' which are like co inductive hypotheses and basically once we take a step up on the upper left-hand side then on the right-hand side we can use our co inductive hypothesis as axioms so this is how we can do reasoning about loop

invariants and and things like this so you can see the C moves from being underneath the the prove turnstile to being on the left-hand side in the set of axioms we're allowed to use on the top right we have the axiom rule which basically just says like you know we have some body of axioms somewhere that tells us what we can do how we can take a single step of execution and in our case this is just our symbolic execution engine and that means that you know we can prove that that reach ability happens and then the rest of the rules are kind of you know just stuff that you need to have the circularity rule together with the transitivity one is really the most interesting bit of it which lets you do this Co inductive reasoning about loops that could go on forever so we have soundness theorem for

it and it's relatively complete meaning that for any non terminal for any terminating program you know either it will sorry for for non terminating programs we can prove anything about them anything is true for terminating programs either it will reach and we will be able to prove it or it won't reach we'll be able to show the counter example trace yeah and then the circularity and transitivity are the interesting bits okay so their capability logic prove accepts proof claims in the same format as axioms from the operational semantics the operational semantics rules are interpreted as axioms that can be used to discharge these proof claims on success the current approval will just print out sharp true which isn't you know that's good I guess you can see the

sharp trio and be like okay I'm happy but on failure it kind of just prints out this big giant symbolic counter example with all the end states that it wasn't able to prove reach the target goal which is really a bit annoying so that's why I would recommend looking at this K lab tool which lets you actually see the entire execution graph that happens to get you to those symbolic counter examples the proof search is fully automated so you don't have to sit there and tell it you know take a step try to do case analysis take another step split on this split on this boolean expression or something like that it's all just fully automated which is good and bad it's good because it means that you don't have to write down the tactic it's bad because it means you get no

control over the prover but you know trade offs here's an example of a proof and you can see it looks just like a normal rule this is a proof in wasum that if you do push push ad so the in in wasum you say push by saying Const so this is push the value X to the stack push the value Y to the stack and then add the two numbers up and basically this proof is just saying that if you push push ad then what will happen is in the stack on the stack cell you see there the addition will happen so it's not a very exciting proof but already you can see we have to have some preconditions like here we have to say okay X is greater than 0 Y is greater than 0 so this is kind of sensible preconditions and then you also have to

say that the addition won't overflow so x + y x + int Y which is the unbounded integer addition will not leave the bounds of whatever I type is which can be I 32 or I 64 so this is how you would you know do a proof in wasum you would you'd first write down what you think the transition should be and then it would say hey here's a counter example maybe there was an overflow or something like that then you add a precondition saying okay what if there is no overflow then does a proof go through so it makes you specify so this is just a specification and the proof is actually just you know running the Java back-end on it and letting it try to find either a counterexample or it will be able you know prove it but what you end up

with is a specification of your contract that says you know these are the conditions where everything goes right and then you'd want to take these conditions and negate them and make a proof that when things go wrong to go wrong in the right way or something like that so that's usually how we do proofs we have signed like a failure case in a success case okay I guess actually no questions because no no questions but there's some citations for you if you want this good question if you want if there would be any questions okay so how about I have a question so I'd like to ask about cost and sort of who your

target market is so who would be a good sort of customer for your services yeah so a formal verification is expensive because it takes a lot of person hours to be able to do it so really the the good we have some lighter weight tools which we can apply to your contracts we can do kind of traditional security audits too which are a lot less expensive so you know right test for you find corner cases and bugs anti-patterns whatever but in terms of actual full formal verification really good targets would be you know contracts that are deploying contracts for their customers and you know you want to make sure that the contracts you're deploying for your customers aren't going to mess up and then you have a bunch of angry customers because there's a bug in every single one of them or something or maybe a

distributed exchange you're sending money out other contracts you want to make sure that nothing malicious like they'll burn a bunch of gas or something like that will happen so basically any contracts that are dealing with a lot of money really what it boils down to is look at how many dollars you will lose if that line of code messes up and then decide you know should I spend that many dollars making sure that that line of code won't messed up it's basically what it boils down to great thank you