[Music]
wow a lot of fans in the audience yeah
hello everybody hi everybody yeah today
we'll talk about uh FK Choice compliance
and how we approached it and to start
let's understand uh first why FK Choice
compliance is important uh the FK Choice
rule is the part of etherum protocols
that that decides on the head of the
canonical chain uh that is the chain
that is the chain that you use to
confirm your transactions that is the
chain that will be eventually finalized
uh by the protocol and uh a noncompliant
with the FTR speack implementation can
cause uh different security issues such
as confirming your transaction with the
chain that your local node pretends to
to say that this chain is canonical but
the chain is effectively not canonical
and it's not canonical to the
observation of uh the majority notes in
the network um in some situations uh
this uh non-compliant implementation can
cause uh Network splits uh which can
affect validator voting uh participate
valer voting rate uh in a bad way and uh
in the worst case scenario it could
delay
finality um in Ideal World uh
every every implement mentation is
formally verified to be compliant with
the for CH spec but we cannot expect
this to happen because it is quite
challenging and costly and our approach
to the compliance is to extensively test
every implementation against the FK
Choice
spec uh so now a bit uh about the folk
Choice rule itself so imagine there is a
node state that is computed from the
messages that are coming from the
network such as blogs votes and others
and the folk Choice rule algorithm is
executed over this state in in the
following three steps so at the first
step there is a filtering function that
uh selects blocks that are candidate for
head we call them viable for head blocks
at the Second
Step uh validator votes are used to
compute uh weights of sub trees uh which
contains those uh wable blocks and uh at
the last step uh the algorithm
recursively goes uh down to the heaviest
sub tree until the leaf block is found
and that Lea block uh will be the head
so the algorithm doesn't look uh um
quite doesn't look complex it's Rel
relatively
simple but uh the complexities here uh
coming from the different place uh there
are many many inter notd interacting in
the network and they produce many
messages blocks and votes uh that
results in a huge variety of States over
which the folk Choice algorithm is
evaluated and every client
implementations use uses their own
optimization in order to compute the
state fast and uh in order to uh run the
FTR rule so those makes those two things
makes the the F compliance incredibly
complicated uh and now over to Alex on
how do we fight those
complexities uh so our goal is to reveal
difference between Fork Choice
specification and implementations and we
need a lot of interesting test scenarios
but generating lots of really
interesting scenarios is a challenging
problem and so to overcome that we
developed a strategy which based on the
following principle differential testing
property based testing modelbased
testing and final ingredient fing and
randomization and okay about
differential property testing for Choice
spec is
executable so we can compare
implementation Behavior against
specification directly and this is why
differential testing and we want to
check that uh every implementation
calculates the head of canonical chain
correctly but it does not mean that so
if the check the head is correct it does
not mean that protocol state is correct
too and so we can check additional
properties uh to reveal more buxs with
using essentially the same test
seed and uh here is the example of how
the property checks can be really
helpful uh on the left side there is a
buy implementation that for some reason
just missed one vote uh and uh the head
in in both cases in case of
implementation and specification is the
Block C so this V this Miss vote Miss
did not affect uh the had computation uh
and if the test case would just compare
the head uh and uh the the client this
bu implementation uh running this test
case uh would pass it
successfully and uh directly comparing
the weight of Block C in this case uh
would help us to reveal bug much easier
because otherwise we would need to
create a test that uh in which run in
which this bug implementation would
would lead us to uh the different uh
block to be the head like for instance
Block B so is just uh like less test can
can reveal more boxs that's uh the short
uh description so uh yeah what we
haven't yet mentioned is that our
compliance uh Tool uh leverages on the
already existing folk Choice testing
framework uh there is the consensus in
the consensus specs there is the fork
Choice testing uh format there are
manually written uh Fork Choice tests
and clients already run them those are
integrated uh and yeah the the clients
already uh check some of the properties
so the differential property based
testing is already in place and what we
we do with uh our in our compliance tool
is just add one more property uh which
uh is to check weights of viable for hat
blocks okay so we want to check that for
Choice uh Ro is executed correctly but
just covering various execution pass is
not enough because um the through
executed on many nodes and they're
interacting and building blocks using
the rule and so we actually what we want
is to capture this
interactions but we do not uh enumerate
all possible scenarios and so we use
modelbased
approach um our models basically allows
us to focus on the aspects that are
interesting abstract away from other
stuff and we have three models here FFG
checkpoint three shapes block three
shapes and also filter block three
predicates coverage model and each
models for example we have 10 blocks and
we have various trees constructed of of
these 10 blocks and so we basically want
to generate a test Vector for each of
these three shape and if we are able to
to do that then we have 100% coverage of
our model and for our three models we
currently uh optained a thousand of
solutions but in practice it can be
arbitrarily larger so it can be a
million models no problem yeah so to
give you like more intuition behind how
this uh model based generation Works
let's consider the F ofg check points
model uh this model is parameterized by
two main parameters uh which are uh of
EPO and number of Super majority links
and here is the example of a couple of
solutions that satisfy uh this model
with four EPO and two super majority
links and uh on the on the if you look
at the top uh deok number four uh in
this case will be finalized according to
FFG checkpoint to to to to the finality
Gadget rules and uh in the SEC in the in
the second case which is on the bottom
the e book number two will be finalized
so basically uh when we do the test
generation we ask the constraint solver
to find all
possible uh combinations of Justified
and finalized points given the um some
certain model inputs and uh we also run
uh this these models uh with uh
different inputs like uh you can run it
like with 10 EPO and five Super majority
links with 10 ooks and four super
majority links and so on and this is
gives us a lot of uh a lot of uh
solutions to further work with uh in our
generation okay so now we have uh many
model Solutions and everyone can be
turned into a test Vector but that can
be done in different ways for example
validators can vote for different blocks
but as a result we can have the same
shape
and and so we use randomization to
instantiate these model Solutions
basically flipping a
coin and uh after we have a test Suite
of test vectors we can additionally do
fing um it's important because our
models actually assume that all events
arrive in time which is
unrealistically but we can easily
overcome it by shuffling uh duplication
of messages and dropping some messages
and also by mutating
messages we will also plan to implement
in future coverage guided fing of
implementations and this uh randomized
instantiation and fing allows us to
increase the number of tests in by
orders of
magnitude yeah here is the example of
how the randomization is used uh as Alex
mentioned we have these model Solutions
and we use them to uh produce uh like
various test vectors and on the top
there is just a model uh which which
says that basically there is a block
that has two children the client has
nothing to do with this model it cannot
run uh this model because uh to to to
make it a real test Vector to make it we
have to make it a real blockchain that
follows the ethereum protocol rules and
uh we use consensus spec uh specs for
for doing this for making a these blocks
turn into uh making this uh block
dependency to turn it into real blocks
and real votes and in this case the
model does not answer you to many many
questions that the protocol need to you
know to to to create an instance of a
blockchain those questions such as like
uh which validators are voting for which
block every single slot uh where where
is the maybe there is an empty slot
between those blocks
uh which is the total number of
validators participating at Moment In
Time whether the message is like some
message is invalid or not and so forth
and for every case for every possible
case here uh to answer such questions to
to decide on such uh things we flip a
coin so we have like a every every test
generator run there is a combination of
model solutions that we use and a
randomness seed and uh running the same
uh combination of model Solutions with
different Randomness seed can yield a
different uh test Vector what matters
here is that this test Vector will be
completely different uh from the FK
Choice point of view so like in this uh
example there are the had TS a different
so but the model is the
same so we have implemented the initial
phase of the strategy and this work was
supported by a grant from eum foundation
and but from consensus and so we have a
test generator we have a PR in consensus
spec repository we have generated three
test Suites to Tiny and small uh the
test Suites for initial adoption and we
also the main standard test Suite which
contains about 13,000 of test which I
believe is enough for initial
phase yeah and so we did the as a
prototype we did the integration of this
tool in taku as I mentioned before uh
there there is already uh the F choice
test and clients already know how to run
them so this integration was relatively
straightforward we added the new
property check that mentioned before uh
found some issues a couple of them are
related to optimizations I'll cover this
uh on the next slide and we found four
Edge case uh four edge cases uh where
where TECO is not kind of like compliant
to the spec but these edge cases are
very very unlikely to happen on any any
test net uh including the main net and
uh uh the fact that we found those edge
cases uh shows us how powerful this tool
is with only 13,000 tests just imagine
what would it be like uh if we have like
a thousand uh 100 100,000 tests or a
million tests and we're looking forward
to have this tool in to have this uh
suit integrated with other uh consens
layer clients to find issues in them as
well so let's look at test Suite details
so we have uh test groups inside test
suits for example block three focuses on
trees of various shapes and block weight
we try to produce block trees where
weights are different distant from each
other we also have a shuffling group and
uh test group which focus on a test s
invalid messages and combinations of
filter B three predicates and overall we
have about 13,000 of tests right
now okay uh so we have problems and one
pro uh problems is that advanced
mutation are challenging to implement
for example if you change a block we
need to rec compul recalculate its cash
and descendant blocks and attestations
should be recalculated too and this uh
takes time so test generation is slow
currently it takes about 10 seconds per
second we have investigated the reasons
for that and okay one reason is that
fork Choice Ru is expressed using python
which is an interpreted language and
it's low we but that's not the only
source of the problem because there are
also some slow spec components they are
optimized actually but there are still a
room for
improvement and this uh slow test
generation limits uh the Practical size
which we can
achieve yeah as I mentioned before there
are some optimizations that uh cause
some test fail uh and those
optimizations are that we have faced
with are related to uh dos protection so
some AR stations some old attestations
that are not going to affect the uh folk
Choice decision are discarded in Teo for
instance and in other clients as well
and different clients use different her
istics to discard such attestations and
here we have another problem uh is that
the uh the two the the cute cannot be
designed to uh to avoid all those uh
failures and uh diff and because of
different clients has different
optimizations and different her ristics
there will be different subset of tests
that are failing and uh we have like
just 13,000 tests but imagine if we have
a million tests and you have like uh I
don't know thousand of tests failing and
you have to ensure
that you have to real you have to
understand whether those are uh because
of such optimizations and this is legit
case or whe this is a real bug so this
is something to work with the client
developers
on and as a Next Step as a next low step
we want to integrate this test you into
other consens clients here we engage
other client developers to to help us
with and yeah yeah okay so one of the
most important things to do is to speed
up test generation and okay one thing
that we want to do is to transpile
specification to C or to n rust other
compiled language and of course there a
problem that a transpired code there can
be a bu into the translation
but uh since we are translating function
to function it's actually much easier to
test each function individually
individually and another approach uh
another important thing is that to
optimize all components we have already
experimented with faster implementation
so we as a result we expect uh that our
test should run uh test should be
generated at least 10 times faster and
also an important thing is to implement
coverage guided fast testing of client
implementation and for this reason we
it's critical to have fast test
Generation Um so if you want to talk
about this topic reaches out you can
also find us on E andd Discord here is
the core code which uh links you to a
page uh with the references uh to the
work we did there is a description of
the test and methodology there is a uh
link to the pr to this pack which
introduces the test generator for this
suit and also there is the pr uh that uh
PR to te that integrates the Su into Teo
thank you very much thank you thank you
very much Alex and mik all
right great to see you got a lot of
support from the audience that's
fantastic now I wish I could say I
understood the topic of the content but
I didn't but I'm sure the audience
because they're asking lots of questions
I'm very honest about it you know uh
please upvote your questions which are
most popular and we're going to look at
the screen and take a run through the
questions right at the top do you run
Fork Choice tests covering nonf
finalization with multiple Forks who'd
like to take this question I I love this
question because I before this talk an
hour before this talk I was thinking
about having this test in suit because
if you have if you've been at the dep
Lance presentation who was presenting on
the non-f finality and how can it kill
ethereum this is very important for
clients to have this kind of testing
suit uh we haven't think thought about
this much but I think it is doable uh
and yeah I'm I'm very happy to discuss
this um and try to make something uh and
try to make a suit that would test nonf
finality and let clients do their
optimizations and uh check them by just
running this on the computer excellent
from one one question can change
everything right uh now the question at
the top this test generator Rock so
another round of applause for creating
such a wonderful test
generator again if you want to give
feedback before you go into the Q&A
there's a little box for speaker
feedback please go and write it there so
the speakers can take take a look at
that but well done to both of you let's
go to the next few questions do you plan
to set up a dashboard to show test
results from different CL clients like
Hive who wouldd like to take this um
I'll take this I we don't have such
dashboard for other CL tests we have a
plenty of Cl tests that are uh run by
clients and yeah I haven't thought
thought about it we haven't thought
about it so probably not because yeah if
it will be useful we can but maybe not
okay all right let's go straight to the
next one what does it mean for the fork
Choice spec to be executable go ahead
yeah I'll take one okay so um it's
expressed as a python code so it's
basically a number of functions and some
functions prescribe how to react to
events or messages arriving from Network
it's on block on attestation on on a
tester session and some others there's
also time tick and finally you have a
method to get head so this is just by PL
python code you can run it all right
let's go right to the next one we got
three questions left I think we got
enough time the randomizing weights
model can take an arbitrary tree as
model question mark how about FFG
information who would like to answer
this one I can yeah
so uh the Tre block tree model is just
one of the models uh and there was just
an example so with randomization and uh
we also have the F ofg checkpoints model
that gives the all all possible uh
combinations of Justified and finalized
checkpoints given the model input so it
was in the presentation as well so we
have a model for that it is also this
information also used by the test
generator all right thank you for
answering that I'm going to mark it as
answered last two are attestations only
on chain coming from blocks uh no no uh
we have both cases so we have uh get a
two station from blocks also produce
them separately very um I can expand on
this we have actually have three uh
possible cases for this one is that just
in pure onchain attestation the other
one is uh pure Network attestation that
the attestation that is not included in
any Block in any block and the third
case is both it is in the block it is on
chain and it is coming from the network
as well and this is all decided by the
randomization so we flip a coin and
decide which station uh would will be in
which state all right thank you for
answering that you're looking at me like
I understand the answer I don't but the
audience I can tell from the audience is
nodding and I'm just nodding along with
them U okay we got uh one vter okay we
got 51 seconds let's do it if the model
is written to test the spec
implementation how do you guarantee the
model correctness okay the model uh does
not have to be correct because we
execute python specs directly so we use
it just to produce interest in test
vectors and yeah we are using spec code
to produce the text vectors but finally
we have a special procedure to run the
generated test
using um the python spec and check the
everything is okay very good and I
believe I can help you answer do you
execute the python spec directly yes you
do ladies and Gentlemen let's give our
two speakers a wonderful Round of
Applause to Alex and mik thank thank you
gentlemen thank you thank you very much