foreign
[Music]
thank you for making it today
um
as the title says I'll be presenting on
our work on formally specifying and
formally verifying the distributed
validator technology protocol
and the way I'm going to do so is by
answering to four key questions
why do we need a distributed validator
in the first place why do we need to
formally specify and formally verify the
distributed by data technology protocol
how does our formula specification look
like and
finally what they've actually achieved
so far and what is left to do but before
diving into answering to these questions
some do acknowledgments this work has
been carried out by consensus r d
as I received a grant co-founded by the
ethereum foundation oval and SSV Network
also I'm here presenting the work but
this was done together with tanaitran
who is one of my colleagues in the
distributed system formal verification
team at consensus everybody I think so
at least I can start answering to the
first quick questions
why do we need a distributable validator
now if you are here before the talk by
Colin Eisen you may already know about
why but I'll briefly go over it actually
the way I go over it it will be by
answering to another question
what can go wrong with an ethereumable
data
well there are two things at least that
can go wrong with an ethereum validator
the first one is that your ethereum no
ethereum validator might fail and let's
see what this means
now you know you have your slots in some
of the slots you have to propose another
you are a tester and your ethereum
validator is working what this means is
that it produces blocks you get you get
Rewards produces attestations you get
Rewards
but now suppose that your node fails but
what's going to happen is you start
missing uh your duties so if you miss
the blog you don't receive rewards if
you miss an attestation you don't
receive the rules you also get penalized
what this means basically with what can
happen with a node failure is that you
Minister rewards and you also can incorp
penalties
the second thing that can go wrong
is that the validator key might be
compromised and let's see what this
means assuming your Assyrian validator
with your validator signing key now in
malicious note is somehow able to steal
it what these Mauritius Now can do can
actually produce for example two
at the station slashable attestation
sign with your validator signing key and
package all of this into a slash improve
signed with a malicious note signing key
and propose a block submit it to the
network what's going to happen is that
of course you're going to get slashed
and some of your funds get actually
um
kind of transfer to the malicious note
so
while this while the malicious note
doesn't have the withdrawal key they can
still somehow get some of your funds and
this is very bad it's bad for you as a
Staker it's bad for the network because
it means that Malaysians get can get
more and more power more and more stake
and we don't want this a way to fix this
is not a straightforward as one might
think just thinking about the first
issue which is if you want the simplest
one might think well let's just run more
than one ethereum validator and well we
know from the early day of the big
contain this is perfect recipe for
getting yourself slash too yeah we know
we don't can't do that this is why by
the female Foundation
car and come up with the concept of
distributed by data technology protocol
which is um
simplified here so what you need
essentially is you need a coordination
layer between the different nodes you
need this coordination layer because you
need to ensure that
whatever attestations are submitted
potentially by more than one no they are
not slashable and this relies on a
consensus protocol that so basically
have a middleware between the beacon
notes and the remote signer and this
middleware which is called distributable
editor client runs underneath a
consensus protocol plus another layer on
top that ensures that we must ensure
that you never get slashed this is a
protocol that allows basically splitting
the distributed validator signing key
into different key shares and it's a
remote signer as its own key share so
none of the remote signer as the full
key this is what uh ensures protection
and against uh a little signing key
staining
okay now we know why it's important well
why do we need to formally specify and
verify such a protocol
we have removed any single point of
failure and so we have higher resiliency
however you know there is no such a
thing as a free lunch
we have increased the complexity of the
system now we have a distributed system
in place of a single piece of code
and so we have higher senses of bugs
and this is where firmware verification
can really help us
and to give you an idea of how it can
really help us I want just to draw a
comparison to testing
and the key concept here is that formal
verification is exhaustive and testing
is not
to give you an idea with formal
verification we can consider networks of
any size you pick a number we can deal
with it you can do that with testing yep
only small Network sizes
and it's very important when it comes to
Byzantine Behavior because with formal
verification we can really consider any
any Byzantine Behavior Uh with testing
even with fuzzing you have already you
can only consider limited set of
Byzantine behaviors perhaps you know it
doesn't respond but
you can't really exhaustively consider
all of them also if you want to make
sure that a property is insured well
and and this property actually does in
thought so there is a bug in the
protocol well with formal verification
it can be detected
with testing maybe yes maybe no it
depends uh it's not exhaustive so you
might get lucky
moreover if a property is actually true
well with phone notification we can
prove that is true when we're testing we
cannot do it because
again it's not exhaustive so
this is the benefit this is why formal
verification is very well suited for
this protocol
now I want to give you an idea of what
formal verification consists of you have
a formal specification which essentially
is a mathematical definition of how the
protocol is supposed to behave which
says basically when you receive message
X you need to send message y
then you have a property definition
which is a mathematical definition of
the properties
that the protocol is expecting to
guarantee something like never commit a
slashable offense
although this is kind of packaged
together in a formal proof
which is a mathematical proof that the
protocol specification ensures the
properties now what we do we take this a
step further
and we work with machine checkable
proofs it means that our proofs are very
checked by a computer
and this provides higher guarantee that
the proofs actually correct
okay now we know why we need to do that
and now we can have a look how the
specification actually looks like
now the specification is not a piece
it's not a single piece it's modular
we need to specify the different things
we need to specify how the single node
you know the DVC the middle layer
behaves
but you also need to specify how the
Byzantine node behaves and actually what
we need to do is specify what it cannot
do so there are things the percent I
know it cannot do cannot for Signature
also it cannot change the state of
another node so all these things need to
be coded in the specification we also
have a specification for the consensus
protocol this is because the DVT
protocol is agnostic of the consensus
protocol used and so what we need to do
we need to specify the behavior that we
expect from the consensus protocol
we also need to specify how the network
is supposed to behave for example which
sequencing of messages in my event I'll
go over on this one in more detail later
and all of this is put together is
linked together in the distributed
validator specification
what we have actually we also have an
actually uh executable reference
implementation that implements the
single node specification
and all of this is written for this
project in Daphne
which is a programming language
um it says a python JavaScript like
syntax
and it's a formally verification aware
language and so I'm going to go over
with the spec by starting from the
bottom has been a bit say vague abstract
I want to give you some practical code
to look at so I start from the
executable reference implementation what
I want to show here this is the method
that is called
when the consensus protocol decides on a
new attestation what I want to show here
is that
um the code is pretty easy I would say
to understand it's a really I think that
any developer would be able to read it
um it's really a mix of JavaScript and
python you have some form of some
statements that are required for formal
verification those are the top if you
are just interested in say look in the
reference implementation and having your
own implementation you can just ignore
them there are also some specific syntax
like this one at the bottom which is
kind of the equivalent in some sense of
exception propagation in in some of the
common languages but aside from this is
pretty simple and this is one of the
reason we have chosen definitely for
this project to
to to to to basically make it easier as
easy as possible to for the developer
development Community to really use and
this product protocol but now let's go
up how does the actual specification
looks like so what the specification
does really defines how the system
transition from one state to the next
and the system State includes the state
of all the various nodes uh the state of
the network the state of the adversary
the state of the consensus so all these
things is encapsulated in the
in different fields so let's say of the
system state
now the transition says well on a given
event which can be a new set of Duties
time to execute the next Duty message I
received you move from one state to the
next slide from the yellow state to the
Green State
one very important characteristic of the
way this specification is written which
is commonly also to our Kelly plus way
of writing specification in TNA plus we
allow non-deterministic Behavior now
what you have on the and explain why
this is important what you have on the
left hand side is not really
non-deterministic but close to it so
what can happen is that from one state
you might have more than one event that
can move you to two different states so
so for example a node might receive a
message from node 2 or perhaps on Note
3. and this this is what allows to
capture
okay Network asynchrony so and this is
one of the important differences to
testing we can really reason on any
possible sequences of messages any that
you can imagine this is coded in
the other
point I want to make is really about the
non-deterministic behavior so from one
state the same event can get you to two
different states and now why this can
happen mainly because of that adversary
so if you have a given state
the adversity can behave in multiple
ways on an event and this is a what
allows us to capture this
while I speak about this I want to draw
a comparison to model checking which is
a different technique and with model
checking you have the problem of State
explosion and it's very it will take
it's very hard for model Checker to
really
being able to check a property
considering Byzantine Behavior because
it will take a lot of time and with
formal verification takes a lot of time
to put together the proof but once the
proof is put together it's quite quick
to be run through
now looking I want to show a bit code
again how actually the formal
specification is Brittany Daphne
um let's let's focus on the top top of
the slide so let's assume you have this
transition from the yellow state to the
green and purple State when the gray
event is received the way we code it we
essentially have a function that takes a
source date an event and the destination
State and returns a Boolean
now the way that the transition is
encoded is that the function if the
function returns true on a given Source
event and destination state it means
that the system can transition from
source to destination given the event if
it returns Force there is no such
transition so in this example for
example is true for a yellow gray green
and purple but not false for any other
combination
and this is you can see at the bottom is
coded in this is how it's coded in
definitely now this is essentially a
simplification of this
um but it's it's a um this is expressed
using first order logic you know this is
something we don't see often in standard
uh programming languages but
it's not much of a stretch to say
what you can see here
this is essentially an end of different
state transition and here we have the
state transition for the honest node and
you can see here we say basically this
much true for hollowness nodes that's
what the photo does
and then we put this in a coin end with
the state transition for Network
adversary and consensus
you know what you can see here is this
exists is what gives us the
non-determinism because we're saying
this function returns true as long as
there exists a set of messages received
messages sent and decided value says
that they satisfy all the various
constraints and the end expression at
the bottom
now before going into what we actually
achieved I need to make sort of
disclosure uh
that are part of this say system that
needs to be trusted so these are the
parts that need to be trusted and um and
these are the parts that actually we
don't trust now if you look at this it
seems the area it's quite of the trusted
and non-trusted but you know the error
doesn't really represent the value of
complexity also it's not really a
problem of formal verification it's a
sort of existential problem you
you need to assume how the adversary
will behave in your system even if you
just buy software you do you write tests
whatever you do you need to assume that
you have a consensus that or a library
that works correctly you have a network
you assume how the network will behave
um saying things for properties you
assume that you have a set of properties
that are those that you are really
interested into
so
this it's it's just something that yes a
formal verification doesn't doesn't
solve but it solves a good chunk of
problems in ensuring that well your
single node as it is specified will does
we guarantee those properties
also there are things one can do to
increase the chances that the trusted
path is correct
one is to keep the trusted specification
as simple as possible
one is to have a peer review
uh also for the tool it's important to
use formal verification tools that have
good support we use Daphne Daphne is
very active bugs get fixed very quickly
also
uh
in distribute the system usually you
have two types of properties safety
properties which say something bad will
never happen and you have liveness
property where they say something good
will eventually happen now being if you
formally prove that a specification
guarantees both it's very
it it really increases the chances that
the trusted part is correct it's quite
hard to put together a specification
guarantees both both properties it is
incorrect
so now we can go over what you actually
achieved so far and what is left to do
so
on the right hand side you have what
we've been able to prove on the left
hand side you have the assumption
to have been able to prove is that
slashable attestation signed by the
distributable data signing key the one
that is shared
they can never be created in other words
the account associated with the
distributed validator signing key can
never get slashed because of attestation
signing
and this is done under the the
assumptions you see on the left hand
side
and assumption is as again we have any
we allow for any message delay we don't
constrain this at all we had allow
messages to be lost
we also allow
the biker nodes
okay typical notes here to be actually
out of sync for this proof we don't
require them to be in sync they could be
serving completely different duties and
they prove still old and then we have
some assumption on the um number of
nodes that can that are either Byzantine
or with a compromise key to be less than
one thought and this is
um theoretical bound on consensus
protocols as well we assume that
signatures cannot be forged and they are
unique and also that you have a sound
two third
signature scheme and then these
assumptions
we've been able to prove the property
we've also been able to prove that
the reference implementation adhes to
the specification
now what this means is that it is that
if you deploy a system uh running the
reference implementation of the of the
distributable data client node what you
get is a system that ensures the
non-slashable attestation
and
so looking
that what is left to do so we put
together this proof we have the
specification we have the reference
implementation
and it's all open sourced on the on the
GitHub repo that you can see here what
is left to do is to extend the
specification and the reference
implementation to distribute the block
proposing and block header signing to
extend the funnel proof of noise lash
about the station to no slashable blocks
and then to
add the proof of liveness as I mentioned
before so proving that a distributed
validator will always eventually create
a valid attestation valid blocks and
valid header signatures
and this is all for my for me thank you
for listening
um what techniques were used to prove
that reference implementation adheres to
the specification
so
um
okay so we have used the refinement
technique so we proved through a
refinement basically yeah showing that
if there is a relationship between the
uh rest implementation State and the
specification state that and on a
transition that is maintained
how far away do you think we are from
being able to use validator pools for
either eth2 or other protocols I
probably this is a question I need to
to the fair to someone else sorry I yeah
it's
only this is about implementation so
yeah I I don't have that answer how
difficult is the learning curve to kind
of become someone who can contribute to
this uh you know formal verification
things and be able to to start working
on that
it's a
reasonably
say steep not too much though I mean
nowadays with tools like Daphne I think
it's much simpler than having to learn
something like Isabel or this
pyramid proves that are a bit not more
you say abstract syntax and
um way of proving things so things are
improving but that is that is a bit in
terms of contributing to the
specifications say or reference
implementation I think it's not my view
not as much harder as contributed to a
python
specification so it won't contribute
just to the specification you know
necessarily to the proof
how big is your team and how long have
you been working on this proof to get it
to this point now
so well uh the the theme consists of
four people
um but on this one I've been working
just myself and tanai and we've been
working on this on this uh
on the
we've been working initially in the
specification so on specifically on the
proof I say since June
roughly just for the proof there was a
bit of fixing up of the specification
before that so why Daphne and not other
languages like cocoa or Isabel as you
said yeah one of the reason is that is
for the said the fact that we think it's
easier for
developers to understand Daphne compared
to or lean or Isabel that that's
one of the of the reason also I mean you
can compile uh
if they I think or Isabel but
it
the way you write it is far more complex
yeah yeah I'm not
pretty sure like we definitely can kind
of
um use a
as a construct that is as the concept of
classes and state so it's very similar
to programming and you can have some
give some of the things unimplemented
and open for external implementation