►
From YouTube: Formal Specification and Verification of the Distributed Validator Technology protocol
Description
Visit the https://archive.devcon.org/ to gain access to the entire library of Devcon talks with the ease of filtering, playlists, personalized suggestions, decentralized access on IPFS and more.
https://archive.devcon.org/archive/watch/6/formal-specification-and-verification-of-the-distributed-validator-technology-protocol/index
In this talk, we present our work on formally specifying and verifying the Distributed Validator Technology (DVT) protocol, using the verification-ready programming language Dafny, to ensure that the DVT protocol behaves as expected. You will learn how to read the formal specification, how to use it to write your own implementation of the protocol, what properties we have formally proven to be guaranteed by the protocol and what the future directions of the DVT protocol and our work are.
Speaker(s): Roberto Saltini
Skill level: Intermediate
Track: Staking & Validator Experience
Keywords: Distributed Validator Technology,formal verification,Dafny
Follow us: https://twitter.com/efdevcon, https://twitter.com/ethereum
Learn more about devcon: https://www.devcon.org/
Learn more about ethereum: https://ethereum.org/
Devcon is the Ethereum conference for developers, researchers, thinkers, and makers.
Devcon 6 was held in Bogotá, Colombia on Oct 11 - 14, 2022.
Devcon is organized and presented by the Ethereum Foundation, with the support of our sponsors. To find out more, please visit https://ethereum.foundation/
A
A
Thank
you
for
making
it
today,
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?
A
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.
A
A
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
your
duties?
A
A
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.
A
What's
going
to
happen,
is
that
of
course,
you're
going
to
get
slashed
and
some
of
your
funds
get
actually
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.
A
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.
A
A
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.
A
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
with
testing
even
with
fuzzing
you
have
already,
you
can
only
consider
limited
set
of
Byzantine
behaviors.
A
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
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.
A
A
A
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.
A
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.
A
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.
A
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
the
code
is
pretty
easy.
A
I
would
say
to
understand
it's
a
really
I
think
that
any
developer
would
be
able
to
read
it.
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.
A
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,
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.
A
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.
A
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.
A
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.
A
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,
let's,
let's
focus
on
the
top
top
of
the
slide.
A
A
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.
A
This
is
essentially
a
simplification
of
this,
but
it's
it's
a.
This
is
expressed
using
first
order
logic.
You
know
this
is
something
we
don't
see,
often
in
standard
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.
A
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.
A
Now
before
going
into
what
we
actually
achieved,
I
need
to
make
sort
of
disclosure
that
are
part
of
this
say
system
that
needs
to
be
trusted.
So
these
are
the
parts
that
need
to
be
trusted
and-
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.
A
A
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.
A
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
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
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.
A
A
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.
A
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
number
of
nodes
that
can
that
are
either
Byzantine
or
with
a
compromise
key
to
be
less
than
one
thought,
and
this
is
theoretical
bound
on
consensus
protocols
as
well.
A
A
Now
what
this
means
is
that
it
is
that
if
you
deploy
a
system
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.
A
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.
C
A
D
A
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
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.
E
A
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
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
use
a
as
a
construct
that
is
as
the
concept
of
classes
and
state.