K Semantic Model of Beacon Chain by Daejun Park (Devcon5)

hi my name is Lee Joon Park I'm going to talk about the K beacon chain so so far people were talking about how to and what they implement the clients and network but now I'm going to talk about a little bit different which is about how to formally verify the beacon chain especially state transition function so before we go this is our awesome team that this project we all at Iran time verification do form a verification for any safety critical systems like smart contract consensus algorithm and now we are really excited to work on this form verification of the beacon chain implementation so the K beacon chain is a an executable formal model of the beacon chain written in the formal language called K for the purpose of verifying the important properties which has called this accountable safety and plus or liveness of the beacon chain implementation how many those of you know the K language oh okay awesome so those of you don't know about the K the K is a formal language in which we actually specify the EDM semantics called ke VM which we use to verify many high-profile smart contract using that KBM specification so including the recently we verified the e 2.0 the party contract as well using that so k is kind of really like formal language you can use any formal thing in this domain so let me go to some big picture about what we where we are and what we are going to do next so we have the K Deacon chain is a formal model which actually formalize the Python former spec of the beacon chain so we faithfully formalized to whatever the the pythons back into our K formal language and that we have a de formal model and as I said the the one of the benefit of using K language is that anything is modeled in the K language is executable which means that it's not just more than the paper just you can actually execute and you run this model so you can actually even test so what you are doing what we've done so far is we write down this model we want the exactly same test the conformance test suite you run in the clients to make sure that you all agree on that so we run the same test and and and we make sure the oil Pat test passed so we were very high confident that our model actually faithfully captures whatever the spec and also implementation so I will get to that how what it looks like the KA we can change model is but so but right now we finish the akkada content model and the next thing we want to do is using that model to prove the safety and lightness groups on that model and once we've done these things we really have a high confident that your actual client implementation also satisfy this nice two properties as long as you follow the word of the spec is that any question at this point okay so now I'm going to show you how these formal model looks like so we actually decided to have release the model that very similar to the spec to minimize the potential mistakes that made we write down this phone model the reason that this because we this is important because if our formal model has some mean differences from whatever spec or implementations even if you prove these things they meant may not hold in the actual implementation unless we verify again same thing over those implementation as the what are the lighthouse as I said right so we actually have very similar formal motor that looks like almost one-to-one correspondence to the spec so I will give you some example huh looks like so here the left-hand side we have a Python spec especially for the beacon change state definition so here you can change the definition the user Python data structure there are many things here and the right-hand side is our K called K configuration which is a mathematical object of the same exact beacon change state and we have really similar structure that you can even follow the H want one line drawing the slot same it's one data and so on is force so make sure that they are very similar and make sure that you're not missing any important thing that's the one thing next thing is we have a bunch of the functions in the Python specs right so each function we have K called rules so you can think about rule as a like function the Python so in the function we have left hand side is called process app o we have like called a bunch of function in sequence and then in the K model we have same thing we these curly arrow means that it calls followed by these and followed by that so you can see also very similar the only difference is made is they have what this state is explicitly mention is here and no state mentioned that many because that state actually it's already global which can be accessed accessed which is in the next example so for example if your function access any state like state that slot in our K mode we can simply mention those slot this called configuration you just mentioned that that means you just match that so match the current state and then you can just use that whatever match there in your like function body instead of static say that slot can just mention the state slot and then if you have any if statement I like assault which can be described as our requires clothes so it pretty much very similar you can see this right so one thing is like former motor is not really like different thing or like things you can even write it from in okay as long as you know how to write our interpreter or writing the - code so that's that but the there are some exception that we are not really similar in the case that we have Python list comprehension so in this case this we have these matching target attestation which simply filtering out whatever the target is not matched and then Python using this list comprehension which is really succeed and is to read but we decided to not using these risk comprehension and similar syntax because we think that it's more eat I mean it's better to explicitly specify what's going on here using the traditional iteration approach so we have like defining filter function and filter function is simply trade each data station list and then if the targets match then it include otherwise our filtering out so this is kind of exception that the two models are a little bit different but is but essentially they are same so that is how this former model looks like and then we already have a good competence that I mean these two are very similar but you want to do more so as I said we run all the tests and make sure the whole test passed but in allusion to their was the measure the test coverage which means that how many out for me how much part of for more more that actually exercise by those tests and you know what actually your life we found it actually to some test amidst for example just program I mean same thing example I sorry this one so that is Python coverage to report where you have this list comprehension and then this this comprehension can be I mean you have a full wondered person state coverage if you've only one single test because it's single line whatever you have one test it just executed and you just it cover but but but the things that this is filtering function so you need to have at least few tests like whether filtering whether is filtering out I mean some every elements or filtering out in some other element or nothing so since we already specified that explicitly those iteration we found that existing tests only test none of them is filtered out everything is just all targets matched so we found that something isn't filtering out case is not covered so we wrote down each additional test so we found another similar the missing test and we propose and write more tests and I think which that will be including the next release so yeah we not only have a formal model but also we hope improving the test suite so that's what we have so far we have a former model which is very similar to the specification Python specification it passed all the tests so we have a very high confident that that captures whatever spec and implementation and then our next goal as I said is to now prove the safety and lightness in that model and the monster have dead we are very high confident that clients are secure I mean safe and life thank you [Applause] you