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