[Music]
I'd like to introduce our next speaker
by just saying that he is going to be
speaking on Casper and there are many
different approaches to Casper proof of
stake and um because I really wanted to
um give lad zier a special introduction
I think we should all chant Casper
Casper Casper Casper Casper Casper
Casper come on up
[Applause]
Vlad super
dumb okay great I'm I'm miked up
already uh White
clicker all right
let's just test the
clicker
great all right um all right are we
ready to go time's rolling okay time to
go uh so I'm going to present to you
basically my research on uh correct by
Construction Casper um you know which
I've done over the last few months with
a lot of thank with a lot of help and
kind of got in from Greg Meredith I
can't see him right now through all the
glaring lights but I thought I'd give
him a shout out right away so um so I'm
going to cover some background knowledge
for about consensus protocols and then
I'm going to talk about and like cover
my research for for Casper and then I'll
kind of relate it to the previous
literature and talk about future work so
there's a lot to get through I'm going
to do it really fast uh so for here's my
little there a table of contents who
cares right uh so what are consensus
protocols consensus protocols basically
are something that nodes Ed to make the
same decision about something this is
like the kind of traditional definition
of consensus protocols that really
um has it concept of decision as like at
its core um and a consensus Proto and
having consensus basically means that we
have the protocol in a state where uh
all of the protocol following noes are
guaranteed to make the same decision um
and and basically these protocol
following nodes are the protocol is
called safe if they're if when they make
a decision uh they will always make the
same decision it's called uh it's called
live if
uh there it's definitely the case that
they will make a decision eventually in
some in some in some in some kind of
finite amount of time like you can like
guarantee like prove that they will make
a decision um so so those are like some
basic concepts of livess and safety that
and so let's let's review them quickly
again so safety is the property that
when knows decide they all decide the
same thing liveness is the property that
nodes will eventually decide um
asynchronous networks are are basically
this like Topic in and cons protocols
that uh is not really related to
asynchronous like calls and asynchronous
Computing it just has to do with the
fact that we don't have timing
assumptions on the network um which
basically means that Communications can
arrive in any causally consistent order
like any order where like you know if a
message be that like is causally uh you
know is caused by a message a like can't
arrive like before message a that's like
the only kind of the only kind of
ordering that's imposed on network
messages is the ordering that's imposed
by the causation of the protocol State
updates um and usually with asynchronous
networks we we assume that the network
that the messages get arrive event
arrive eventually but we just we can't
ever say in what order um so
asynchronous consensus is kind of
difficult and we kind of know this
because of this flp impossibility result
which says that like in an asynchronous
Network you can't actually be live and
safe and in the presence of one fault or
more basically if if any of these um
Communications can fail you can you can
kind of show that in an asynchronous
Network um you you can't be both
guarantee that everyone will make the
same decision and that we'll be able to
make a decision in a finite amount of
time and and the reason for this uh
we're we're going to we're going to see
through the course of this of of this
talk um uh but but this this kind of
gets at the point that a syn a
synchronous consensus is really
challenging because um the the lack of
network assumptions makes it really hard
for us to justify why the protocol would
move forward from a state where we don't
know what to decide to a state where we
would know how to decide there needed to
be some messages that flow that H uh for
that to happen but if uh some messages
might not actually make it then we can
show that actually we can't prove that
that there's a guarantee that in a
finite amount of time uh this kind of
decision will be made safely uh and now
we just talk a little bit about
Byzantine fall cont Byzantine faults
you've probably heard of Byzantine fault
tolerance um it's all the rage these
days uh any basically normally what we
say is that any node that isn't
following the protocol is Byzantine uh
and we normally also say that nods
behave in arbitrary
ways um we also have results that
basically kind of also say that this is
kind of hard stuff like B there's are
like limits to what can be done normally
there's like two results one of them is
that in an asynchronous Network you
can't have more than a third
Byzantine fault tolerance and in a in
you know where you have like safety
right where I we have this property that
if nodes decide they will all decide the
same thing uh and we have a similar
result for synchronous networks where
like you can't tolerate half the nodes
being faulty and also have all the nodes
that are following the protocol be
guaranteed to make the same decision uh
so I'm kind of just asking you to like
accept this at this point because we've
got to go and get through the rest of
the presentation uh so so so now I'm
going to describe basically this is like
correct by construction approach that
I'm that I've been taking for uh my
Casper research especially in the last
couple of months uh basically there's
like an outline and then I'm going to
describe my data structures and give
some definitions and then give the
correct by construction binary uh
decision a decision thing one thing I
should have mentioned at the top of the
talk is that like the the title of my
talk is like slightly different than
advertised so what what what I'm really
going to be presenting is a correct by
Construction
asynchronous Casper consensus protocol
that agrees on a bit so like it agrees
on like zero or one uh and it's and it's
going to be Byzantine fault tolerant and
and correct by construction so no no
network assumptions we can tolerate like
Byzantine Behavior Uh but we only we
only agree on a bit
um and still I think that's worth
presenting uh so basically so here's
kind of the the approach that I'm taking
um rather than thinking about the safety
of decisions I'm I'm going to I'm going
to think about estimates right so
estimates are these things that kind of
uh are sometimes defined in some
consensus protocols but are always
defined really in like the blockchain
world an estimate is like a non-f
finalized decision it's like a uh it's
like a a proposal for a decision like
when we talk about traditional consensus
protocols all of the decisions that
we're talking about are like what we
call in blockchain World finality right
like finalized decisions that will never
get reverted where these nodes like
commit to this value and will'll never
ever ever change their minds because
like that's what the protocol says and
like that's the definition of consensus
oh my God we're running out of time so
we use estimates and uh you know so we
and and they mean finality so basically
we're going to Define uh a notion of
safety on estimates b b and and
basically what we're going to do is try
to and we're going to construct an
adversary which will try to change an
estimate for a particular node with a
particular view who has an estimate uh
in order and if that adversary succeeds
then that estimate will be uh be unsafe
because in that particular uh Network
context for example uh it's possible for
that estimate to change uh and and and
basically um uh the the reason why we're
doing this is because an estimate is
kind of a very P personal thing whereas
the sa and the safety of an estimate
meaning like oh my estimate can't change
is a is it's much easier to determine on
a local view than the safety of a
consensus protocol which has to do with
the decisions that different nodes make
across the network um and so I think
it's just easier to reason about so and
and if we have this result which you
know I'm going to show that we do or I
may I'll show somewhere that we do even
if I don't show you today uh that if
nodes calculate that their estimates are
safe uh then they both will have the
same
estimate um so and and this is actually
going to guarantee our correct decision
rule basically nodes are going to
calculate if the estimate is safe and if
it's safe then they can decide and
that's going to be like the correct by
construction approach where uh the the
the decisions are all going to be the
same I.E we're going to have SA safety
because the only time when people are
going to decide is after they've run
this ideal adversary and saw that their
estimate can't be changed and if like my
estimate can't be changed then I'm like
it's cool for me to make this decision
because I know uh that that that'll be
fine so now let's go into like the real
like kind of formal model and like the
technical kind of more the more
technical part of the talk so basically
um this is the main data structure that
we're going to be dealing with these
bets are they have three things an
estimate a justification and a sender
the estimate is basically a bit in this
case because we're just doing binary
consensus the justification is a set of
bets or the empty set and the uh sender
is like you know a validator so
validators are some fixed set they have
weights the weights have this
tiebreaking property which means that
any two subsets of the validators have
different weights so that like I don't
get ties ties are an annoying Edge case
um so we have this other data structure
called a view and a view is just a set
of bets so we have bets which are have
estimates justifications which are sets
of bets and senders
we have uh we have weights on the
validators names for the validators and
Views and these are all of the data
structures that we will use to talk to
Define everything that I'm going to like
talk about for the course of this talk
and that everything everything that's
like defined in the correct by
construction like approach um and it's
worth noting that the BET structure is a
dag uh and you can represent it kind of
like this where I'm going to line up
validators right so so the the the
number on the Node is the estimate of
the bet the edges correspond to which
bets are in the justification and the
kind of vertical alignment along these
along these letters corresponds to like
which validator made that bet here
validator one made two bets one with
estimate zero one with estimate one
validator two similarly and they've got
all these justifications pointing
everywhere it's great so now we're going
to start going some definitions where
we're just going to define a whole bunch
of stuff that we're used to talking
about sometimes um sometimes there going
be new stuff in terms of like this data
structure that we just have that that I
just defined and which basically is like
the model that everything is going to
sit on um so um a bet is a is a
dependency of another bet if it's in the
justification or if it's in the
dependency of anything in the
justification um it's a recursive
definition but there's a really pretty
picture the red bet is in the dependency
of the blue bets basically because it is
uh Upstream from them in the in these
arrows um so equivocation is something
that we sometimes talk about in
consensus protocols I have a formal
definition here of what it means for two
bets to be an equivocation basically
they have the same sender they're not
the same bet and neither of them are the
dependency of the other so basically
they represent kind of uh a bet made
with a justification that like ignored
the fact that they previously had made a
bet there's no way to make two bets and
have neither of them be in the ad
justication of the other without kind of
intentionally leaving out something that
you knew because you can't be ignorant
of the fact that you made a bet really
uh so here are some examples of
equivocations the colored bets are
equivocations um the two red ones you
know and the two blue ones they don't
include each other in their dependencies
there's no like there's no you know
Arrow saying that the one knows about
the zero or that like the one up there
knows about the other one um so these
are equivocations and equivocations
correspond to something important when
we when we talk about Byzantine faults
and kind of our ideal adversary um so
the latest bet is another definition
basically because we have this
dependency relation it kind of defines
like a causally after what we can also
have is like from a particular view we
can say oh these some certain bets are
the latest here some drawings right
these these bets they don't have any
nodes uh with an arrow point uh pointing
out there's no arrows pointing out of
these uh out of these bets into another
bet from the same validator so they're
so like those two bets on the left are
the latest nodes latest bets from
validator one um not that they're an
equivocation uh validator 2 validator 3
also have some latest bets there it kind
of has an intuitive thing right it's
like the latest bet that we've observed
from them and they have we have these
like little arrows to help us find the
way um so an bet is invalid if the
estimate of the bet is not the maximum
weight estimate given the view and their
justification so the justification is a
set of bets it's got a view and it's got
some latest bets in there and you can
wait uh you know every validator has a
wait every validator has a latest bet
and I'm going to say okay look if these
validators have an estimate one and the
latest bet those validators have an
estimate zero but these ones have more
weight then like my bet having all that
stuff into justification uh would only
be valid if my estimate was one
basically we're running like a majority
kind of election here when we have only
the uh only valid bets around people are
always going to choose the major the
maximum weight estimates uh so then we
have this definition of Byzantine
validator so this is something where
normally people would Define Byzantine
validator oh it doesn't follow the
protocol but here what we're going to do
is Define our goal is to Define
everything in terms of the data
structure that we set out initially
right um we haven't even said what the
protocol is exactly so it's saying that
it's not part of the protocol doesn't
really make sense and we want to make it
correct by construction Byzantine fault
tolerance so we can't really use the
definition of oh if you're not following
the protocol then you're Byzantine
because we haven't even constructed the
protocol yet right uh so what we're
going to say is that NOS or Byzantine if
they either produce an invalid bet or
equivocate and this is great because in
terms of our little data structure then
like either you're like a sequential
node that's always producing valid bets
or you've done some craziness and you're
lying basically you're they like telling
what some node one thing telling another
node the other thing uh or you're
producing invalid bets and and and those
are something we can identify in our bet
structure and is like bad right uh and I
lied about my definition of of invalid
earlier you actually have to include
exclude the Byzantine nodes in your
calculation here so like you know if a
bet has if a if a node has two latest
bets you just like drop their weight to
zero uh if a node made an invalid bet
you drop their weight to zero um here
are some invalid bets there's like not
majority estimates given the weights
that were observed below uh I'm just
going to power through because we've got
a lot to cover um so basically an an
estimate is safe in a
view uh uh
basically if
um there there is no possible future of
an of the view which means like
additions of bets to that view where the
estimate is changed um in a particular
context in this case we're just talking
about an asynchronous Network so so an
estimate is safe in an asynchronous
network if no matter what valid bets you
added no matter what Communications
occur the majority estimate just won't
change so all possible futures of this
state of the protocol in just only
asynchronous conditions I.E like any
causally consistent sequence of of
message passing is cool uh um there's
there the estimate is the same or there
is no possible future where the estimate
is different then it's then it's safe
but this is kind of uh not a
constructive definition so that won't do
for our correct by construction kind of
thing what we need to do instead is
calculate safety by producing this
adversary that tries to kind of make the
network condition happen um that changes
the estimate so here's an example of an
an adversary that like shows this bet
from from validator 3 to validator 2 in
order to induce validator 2 to produce a
new bet because now validator 2 sees a
different max weight estimate uh and
that changes the overall max weight
estimate that we see from the The View
as a whole so like that first view was
like not safe um and and basically we
have a slight issue when we're trying to
calculate this this this this adversary
because we have side effects uh so so
what we're going to do is actually have
a lower bound and ignore ignore the side
effects basically because the side
effects if they help the attacker the
attacker can can go with and if they
don't the attacker will ignore so this
attacker is stronger than normal so if
this attacker fails then definitely your
thing is safe um uh uh so basically the
way that to con do the constru
construction for uh the ideal the ideal
attacker for an asynchronous network is
basically to only allow bets that have
the uh the the don't have the victim
estimate in there to travel and only
allow bets that don't have victim the
victim is estimate in there to be made
so the the adversary just like stops all
bets that disagree with his estimate
from traveling across the network um and
like that's the kind of Ideal Network
adversary for an asynchronous network uh
and then the decision rule in
asynchronous network is oh once I
calculate that my estimate can't change
under this ideal adversary I decide and
that's correct by construction because
um you know the the there's no way um
for two NOS in the same in the in the in
in the network to disagree about whether
there's a possible future of that
Network where they have different
estimates um because they're they're
they're because they're both modeling
this asynchronous network it's a little
bit of a subtle argument basically
because uh if they have different
estimate then one of them has to be
later than the other which meant that
the first one has to have a possible
future that changes it one of the
estimates to the other um but we're
really running out of time uh uh so with
equivocation uh we also do this thing
where only The Bets with the wrong the
wrong fly around but you also get some
additional flexibility about where you
can add bets cuz you don't have to only
add them on the end latest bets right
you can add bets anywhere because like
equivocate equivocating validators are
crazy they just they just add bets
wherever right um so but but it's like
the same type of idea where like if
we're safe in that equivocating
environment then like we decide okay we
can stop and it's like a correct by
construction decision function of like
when to stop participating the consens
I.E when to make this final decision
right so this is very related to like
finality and that whole discussion right
so I'm going to try to quickly relate
this to existing research basically the
only stuff that I've talked about here
has been expost kind of safety measure
where we don't actually look we didn't
talk about liveness at all uh and so we
don't violate FP impossibility at all we
have vistine fault tolerance and safety
and asynchronicity we don't have
liveness that's great um and basically
we can see why we don't have liveness
because like if we if we if we don't so
like if we if we don't have safety at a
particular point then we cannot prove
that we will advance to a point where we
do have safety in the context of this um
adversary because that adversary by the
virtue of the fact that we said we don't
have safety is able to change our
estimate and therefore
um
uh uh we can actually become safe from a
position where we aren't safe in a way
that's provable uh and so like we
haven't violated IP at all um so
basically uh we it was cool that we did
it only this expost measurement of sa
rather than reasoning about liveness at
all because that's normally not usually
what happens so like there exist views
in this expost world where you have
extremely high levels of fault tolerance
where like all but one node could be
faulty and your estimate still won't
change because like any of these faults
will be detected by everyone and those
weights of those nodes will drop to zero
but so it's very very safe but there's
like no way to actually get to that
point if all nodes but one are Byzantine
because they'll presumably not
participate in the network behavior that
was required to create that kind of
system uh so it's not l we don't
actually have a guarantee that we'll get
there from a point where we don't have
it to this like point where we're safe
uh so uh I think it provides kind of an
interesting view into business default
tolerance in general and I hope we can
extend this Research into live livess
and also toine everything in terms of
the same data structures right because
these bets being passed around really do
basically map exactly on to the kinds of
restraints on the network that we
normally have so we have a whole bunch
of future work right so what I just said
liveness um I want to make a
conservative attacker that the minimum
izes the amount of equivocation that
needs to happen by weight uh this will
improve the uh computational complexity
of stopping in uh in a bantine fault
context we need to move from consent on
a bit to consent on the evm we need to
do validator rotation we need to add
economics um so we can like run it in
public and we need to do like complexity
and performance optimization and
basically you know improve like the
theory the specification the
documentation the implementation by the
way I do have an implementation of the
correct by like correct by construction
thing I mean mostly I have the ideal
adversary implemented in like python for
equivocating faults so like that's cool
in asynchronous network um my time is
almost up and my slides are done thanks
for listening excellent thank you lad
good
job