we're gonna talk today about the CDC
Casper roadmap and there's gonna be a
little bit less action-packed than the
normal Def Con talk so here's my little
outline we're gonna be talking about the
roadmap as a research roadmap as opposed
to an implementation roadmap or like
roadmap for developers I'm gonna talk
about the relationship between my
roadmap and the theorem roadmaps I'm
gonna talk about our past and future
work because to some how the roadmap is
made up of all the stuff we've done and
all the stuff I'm going to do or
planning to do and then I'm gonna talk
about and I'm gonna give some resources
and announcements so CBC Casper roadmap
is I was saying it's a research and
architecture roadmap the outputs of this
roadmap or research the specifications
you know we don't like the goal of the
roadmap is to produce architecture to
produce you know research in the form of
distributed systems computer science
like theoretical computer science you
know and but also to produce
specifications which serve as abstract
descriptions of protocols which if you
can if you implement anything that match
the specifications you'll get all the
benefits of the architecture so somehow
the CVC Casper roadmap produces
architecture and research and then it's
up to engineers to implement the
architecture in a way that works for
them and any way that implement the
architecture will inherit the properties
of the architecture so you know if
there's like if we prove that its
architecture has a property then any of
the many ways it can be implemented will
benefit from that property and so you
know the CBC Casper research doesn't
produce complete protocol specifications
it produces architecture level
specifications which are which is for
which it's guaranteed that any
implementation that matches the
architecture will benefit from the from
from from the men from the features or
the
these protocols they are you know we are
gonna so we're kind of independent from
the engineering effort so if we ended
architecture and then engineering and it
happens after but you know doesn't mean
we don't provide support to software
developers and help them interpret the
architecture or you know we're gonna
provide support even though it's not the
roadmap to implement it if the roadmap
is to come up with the architectures and
then to do the research it's a research
roadmap it's all about building correct
by construction consensus verticals we
correct by construction engineering is
about designing your systems in a way
that is guaranteed by the process you
design them to be correct it's it's
about not the correctness it's about the
process that is used to just to just to
develop these protocols so we really
formally state the design requirements
and abstractly state protocol statements
and then we refine them in order to
derive from the problem statements a
solution to the problem that is
guaranteed by the way that it was
derived to be correct and so you know we
state the design requirements and then
we kind of will derive a solution to
satisfy them directly from the design
requirements which are in terms of
abstract protocol specifications so and
specifically we're interested not just
any cuz it's protocols we want scaleable
probes take this protocol to have the
same network overhead as Nakamoto
consensus you know we want to be able to
have lock chains that work on the
internet scale that don't have crazy
overhead like a traditional consensus
protocol and but I actually have the
same overhead as Nakamoto consensus or
comparable to the overhead of current
aetherium so basically we want to be
able to make to meet all the normal
requirements all the traditional
requirements of a consensus protocol
like safety and on triviality and
liveness
and also a bunch of other requirements
like for example being able to make this
ideal theoretically optimal overhead
trade-off and also we're interested in
scalability
in you-know-who starting and basically
which we understand entirely inside a
consensus protocol Fremont
where you know if you went to the
sharding workshop yesterday that was all
about that
so I'm not gonna really touch on it now
so we have a really deeply formalistic
approach to protocol design we are
formal from the very start we never
engage in trial and error in the normal
kind of development fashion we don't
implement stuff until we know for sure
that it's correct we do a lot of math
before there's a single line of code
there's ton of math before there's a
single line of code it's a deeply deeply
formalistic process and it takes quite a
lot of time to produce a specification
this way especially if you mean like a
complete specification but it's
guaranteed to be correct because of the
process by which it was derived it's you
know it's correct by construction
process and it's also given to you to
have a certain aesthetic appeal that is
like common in mathematics where you
kind of only make the minimum most
natural choices and nothing more and
everything is kind of natural and
elegant and everything is symmetric and
you know it has like this nice math math
feeling that you get from looking at any
well any good field of math and and that
is like one of the big appeal to think
of the road map is that it's the
aesthetic appeal is very very high
because everything is like derived from
math objects in a way that's very
careful and it doesn't involve weird
arbitrary choices except for to the
minimum possible so that's the basic
that's the basic idea like what it is
the research roadmap that doesn't tell
you too much but before I go into the
items of the road map we're going to
talk about the relationship between the
CDC Casper roadmap and the etherion
roadmaps so in some ways were completely
independent of the theorem road maps you
know we're a research road map the
theorem the road maps are a real mess
for deployment on a theory maintenance
but you know some ways you know you know
CBC Casper Research has you know made
its way into aetherium 2.0
and maybe it'll make its way into 33.0
question mark because it's not really
clear yet what if they're in 3.0 is one
of the things that is probably the most
painless that came out Susie Casper
research is the latest message driven
ghost poor choice rule that is featured
in the you can chain
another thing is south canara puzzle to
add the CBC Casper finality mechanism to
the beacon chain so somehow the CBC cast
for research flow if when the research
roadmap closed into 30 2.0 research at
least a little bit in some ways you know
so in some ways actually the theorem
roadmaps are not really independent of
the CBC Casper roadmap at least as long
as we continue to produce stuff that
they want to implement and you know
that's our goal we want to build
protocols people really want to
implement because of their simplicity
elegance utility properties etc so we
have but the theorem roadmaps are not in
any way blocked on the CBC Casper
roadmaps you know there's there's no no
one's waiting for us to finish our
research before implementing protocols
so they're they're really they're really
are in some ways very independent of us
great so now I'm going to talk about
Phoebe see Casper the CBC Casper roadmap
in terms of you know what have actually
we done so far
and you know what are we gonna do in the
future before I start I'm just gonna
mention that the CBC the Casper research
started before the split between CBC
Casper and Casper FFG Pass Pro research
started off as pre mistake research into
you know economically secure for mistake
where we can have like a equilibrium to
follow the protocol that's really robust
where we have where we use security
deposit in order to make equilibrium as
robust as possible so we can have
penalties to make it to that that
equilibrium is not just an epsilon
equilibrium but like a a very robust
equilibrium and then basically what
happens is at some point after you do
the incentivization research you realize
you have to have some specific thing
you're telling them to that you want to
incentivize like a specific protocol and
so the CBC Casper roadmap really
represents the distributed systems
that is going to be incentivized Dhruva
state it doesn't represent prove a stake
research it just represents consensus
protocol research like distributed
systems research although absolutely the
product requirements in cbc Casper are
driven entirely and determined entirely
by the approve the state research became
before so approve snake research and
then distribute the system research
rabbit Alec and I split off into
different protocols the caste graph of G
versus Casper CBC and so this is gonna
be about distributed systems this is a
distributed systems roadmap you're not
going to see anything about we're
mistaken incentives here not because
it's not in like some other roadmap
it's just that CBC Casper is
specifically a distributed systems
program so basically what is the road
map well any road map is basically
everything you've done already and
everything you're planning to do in the
future
it's kind of like a map though like over
time you know what you're supposed to
accomplish to get to your goals and so
I'm gonna talk about all the past work
that we've done this is this is going to
be the milestones like important
milestones there's lots of struggling
behind the scenes that isn't listed here
lots of just a ton of work that isn't in
here because you know just not a little
work ends up leading to a milestone that
is like especially in research that is
like something that you can present
right so the first the first thing that
really kicked off CDC Casper research
was well beyond just me hearing about
and I'm learning about CB CBC protocol
design is the CBC Casper message type
this is something Greg Meredith and I
came up with in August 2016 when we were
trying to come up with you know just the
preliminary infrastructure so that we
can state a CBC consensus problem in
August just month later came up with for
the first time this safe and non-trivial
binary consensus protocol which I
presented at DEFCON in Shanghai in
Shanghai it you know use this idea of an
ideal adversary to argue about security
which you now we replace with this idea
of safety Oracle
and but but it was like you know the
real milestone like a safe non-trivial
it says this vertical he's like a real
real my real muscle June 2017 so a
couple a few months later
lmd ghost was first specified this
happened when Karla who just spoke asked
me how we're ever going to turn from
binary consensus to watching consensus
he was like frustrated and concerned
Carl and I were working together at the
time on this on the binary extension
protocol and I was like I just gave it a
try and somehow oh sorry I'm looking
over here at the next slide so actually
before the before the for choice rule
came up yo'ii she did a formal
verification of the safety of the binary
consensus protocol in March 2017 and
then in June the latest message driven
ghost made his first appearance as a
specification you know when Carl asked
me this question I know and I went and
adapted the binary cousins protocol to
the latest message urban ghost Protocol
with very very minor change then in July
2017 at the ic3 therian boot camp the
LNG ghost was first implemented I worked
together with John levy to implement it
I did most of the work but he was
definitely there and contributing in
November 2017 we came up with our first
atomic cross charred pork choice
proposal that guarantees that you know
cross our communications our our our
atomic it's like super important
property and this was actually the first
charting solution that ever came across
the UC Kasper research is this atomic
cross yard solution with merge blocks
which are blocks that exist on two
chains it wants in there and the chains
of both both of them so they have the
kind of synchronized exactly at that
height and later quite quite a lot later
we came up with the cross shard message
model which which has the ability to
send a message and not have it be
received right away but have we received
just in some time you know and this is
much more
friendly to prevent or blossoming
orphaned it's it's a much more realistic
cross communication model and still we
have atomicity although a slightly
different notion it's more like a de
missing a finality then Adam is City
just in the fourth choice rule the way
that the merge block will the merge
blocking any portraits will at any
moment you have this atomicity property
with this one isn't there's a time when
you just went sent but not yet received
where the atomicity is not really there
but at finality it's guaranteed to be
there like you can ever finalize ascend
without the receive being eventually
finalized you can never you know have a
finalized not sent and a finalized
receipt it would just be a violation of
the protocol there that kind of I mean
the protocol guarantees it that won't
happen so like if you follow the
protocol that that's just impossible in
August of 2018 we came up with the first
correct and complete safety Oracle
decision detector and this is an
experience inferred like math Olympics
workshop I don't really know what I
don't know remember what it's called
Greg price came up with this who isn't
in in the community but he's you know he
comes to these a hackathon kind of like
you're not hacking events and we have a
long history of struggling for a very
long time before this Vista this one
specification for detecting safety
especially because especially in the
cases of all the cases of
equivocations you know of like who sees
white equivocations it gets complicated
one different validator see different
equivocations and when you have to
reason about the proof while they're
equivocating so it turns out this was
this was a really challenging thing and
we had a real professional mathematician
like math olympian solve it September
2018 we did the first implementation of
the cross guard message system and
here's this gift that we have it's
really beautiful of the system and
basically what's happening in the bottom
is that blocks are being orphaned in
order to guarantee the out of Missa tee
of these communications between the two
charts in October 2018 we did our first
specification of very for implementation
I don't know when the specification
happened I guess of the multi-level
chart hierarchy with message routing and
shard balancing so this is like taking
it to the next level
having two shards that communicate a
little bit in between them we want to
have many shards that do routing and we
want to have a fixed shard hierarchy we
want to have a the ability to change
charts this is an example of a 2 shard
system with a root shard and the child
shard changing positions in some way
there's no such thing as a
child starter anymore there's only route
blocks in the and child blocks at every
moment in the fourth choice rule maybe
one of them is the root but it may be at
some moments there's both of them are
the root like you see when they're when
they're when they're sideways like that
that's like at the moment that moment in
the fork choice the parent has said look
I'm not the root anymore and then the
child hadn't picked that up yet and so
they're both they're both the children
actually there is no root for that one
moment but then when the child
eventually receives that message that
they have to do because of the nature of
the fork choice rule you know the child
becomes the parent and then and and with
single message hops like this that are
atomic you can implement Rabi though
it's guarantees with the same atomicity
property that we can go from one shard
to another through any number of stars
this uses routing protocol as is used
like a routing routing table system that
and this is the tables get updated as
the chars change position I mean if the
stars are a fixed position you kind of
have static routing tables you have just
do source routing calculate from the
source exactly what the routes gonna be
but because the charts are moving and
the shards over here may not know about
the changes in the shard shape over
there we need to have a dynamic routing
table system in this in this solution in
November 2018 at last DEFCON III
released this minimal CBC Casper
protocol paper which described
abstractly a family of consensus
protocols of really really formally and
this is kind of represented a very
general abstraction of what we had done
before with like the binary consensus
protocol or the watching as per core we
had a whole bunch of other ones I got
integer consensus protocol and and this
kind of really abstracted them and
formalized it in a way and wrote and
when we wrote the proofs down in
incredible detail it's way too much
detail and then next month we had the
first formal CBC Kasper light client
specification which won't see the light
of day until today actually and this is
kind of
because originally the CDC Casper
specification it has message nesting
instead of message linking and so the
messages just get really big and that's
not really practical you all don't like
to see that even though than the point
of view of like the semantics in the
math like it's still a non-trivial save
whatever consensus protocol so we have a
like client specification as of November
28 28 20 18 over 20 February 20 19 one
of these etherium stanford math will
impact things I wish I knew what they
were called we came out with Daniel
Caine with working with Greg price who
came up with the original complete
correct safety detector decision
detector came up with an efficient
Oracle making decisions which is a big
deal because that other one is
computationally quite inefficient and
this is also like yeah quite heavy
lifting that was done in May 2019 the
first to live in strategies based on the
leaders for CBC Casper were specified by
researchers at the Casper labs team
actually Daniel Cain who was on contract
with them and andreas Bechtler did they
were both produced in almost immediate
sequence like within like a week of each
other as like a leader based CDC has
provided a strategy where leader
synchronizes everyone and guarantees
that they go through the same states in
order to make decisions also the same
month but towards the end I came up with
the first line of strategy based on
fault rejection for CBC Casper which is
quite a different strategy has to do
with you know validators detecting
whether each other are faulty and using
information about the faults in order to
come up with a alignment strategy then
the IC 3 during bootcamp in 2019 we came
up with and did oh I forgot
I remember now sorry I should have
mentioned so the sharding specification
for the cross hard messages was at the
2018
2018 IC 3 etherion bootcamp and this is
where Aditya came on to the CBC casper
team and like immediately started
writing proofs and he really helped with
the charting stuff who's been helping
with it ever since so and then the
implementation happen obviously after
the specification and that was I guess
I'd like June 2018 or something like
that so now June 2019 we came up with
like me efficient efficient algorithms
for L&D coast updating the safety
detector and you know other other kind
of efficiency stuff to do with with
Casper in july 2019 sebastian zany came
up with the first asynchronous
probabilistic liveness strategy for CBC
Kasper which is you know it's
probabilistic and then it uses a common
calling model or basically everyone's
flipping coins and then eventually they
all float the same coin and ends up
being live the first partial synchrony
thing first of all first partial
synchrony specification for CBC Kasper I
came up with in july 2019 and and this
was also based on fault detection but
now instead of faults being perfectly
reliably detectable as in synchrony
they're not and so it's quite a lot more
complicated and then the oh we got the
first formal verification of safety and
on triviality of the full and light
client for the abstract one this is done
by runtime verification loading a bunch
of people who you're gonna see listed
later so I don't know just a little time
here the we also had the same same and
same month of first formal verification
of efficient safety safety Oracle
detection by Maria Nakamura who was here
also and also we had in the same month
the first partially synchronous
specifications for the leader protocols
that Daniel came basically pioneered and
that's kind of all the major roadmaps
maybe even milestones on the roadmap and
maybe if not all almost all until today
but we have a lot of future work we have
to continue a lot of stuff that we were
doing a lot of stuff that we've done you
may be to notice that I haven't
published in you know you haven't seen
yet so we need to you know means some
some of this stuff needs to be
formalized that's abstracted verified
you
it's not really clear if all of this is
you know like we haven't really done the
kinds of verification that we love to
have we're like you're paranoid
absolutely sure under any circumstance
that it's correct with all of it we also
have to you know abstract it and so you
have like the results that we have in
the most general terms possible so that
where they're as useful as possible for
providing the most general architecture
in Beckman which which basically
provides the guarantees the most
possible implementations and we also
have to do a lot of documentation and
peer review of past work you know you
know I claim we've done but you guys
can't really tell at this point really
not that much here's some more past work
you know validator rotation
load-balancing charting client
strategies these are these are things
that are not done but which are
necessary for the scalable proof of
steak or scalable distributed system
think you know also is and you know I
would say that we have we have I mean we
have solutions to some extent but it's
not fully you know at the level of
formality completeness etc that were
used to in that we expect we also have
like just future work that is just
hasn't really been started that much yet
abstraction all the liveness stuff you
know right now we have like a few
specific live protocols we don't really
have that much of general infrastructure
for generating live consensus protocols
but we'd like to abstract all of our
liveness research so we could have the
most general in structure possible we
have to verify all of our liveness
proofs
you know both by hand and formally to
the much bigger and more extent than we
have already and we want to talk about
performance you know we mentioned
earlier that like we want to have the
same network overhead as nakamoto
consensus and you know there's there's
all sorts of other considerations for
performance like for example the latency
to finality the latency to inclusion in
the first block which under normal
execution is later finalized you know
the number of like operations per second
that you need to do like in terms of
signature verification and like compute
there's as well as like the the overhead
the
message overhead which is kind of what I
was referring to and I'm thinking about
the overhead of Nakamoto consensus I
wasn't about mining there's thing about
the clients and how they just have to
download like one header per block or
very little information you know we have
Club we have a CBC Casper we have this
requirement that it at the protocol
fault that the fault tolerance
thresholds of the protocol are not in
the consensus protocol but their client
and validator side and so we have to
give strategies for clients or give at
least some best practices for clients
for choosing these thresholds because
not all thresholds are going to be
equally good or equally useful so you
know this is like Anna just a whole
bunch of stuff that needs to be done
there's probably more future work that
isn't listed here but but but if this if
this is all done then and all the stuff
that we've already claimed is done so
far as done thank you we're pretty
pretty close to having a scalable
distributed consensus protocol that has
all of the security and overhead
properties that we want and also of
libels which is super important property
that is shockingly difficult to provide
basically have to prove that if you
exhaust you basically have to prove that
there is no way to execute the protocol
that doesn't eventually lead to the
decision easily you have to kind of
exhaust every single possible state
transition to the protocol until you're
forced to make it to make a decision and
that turns out to be quite a difficult
thing to argue so we have some announces
announcements and resources to share so
we're collaborating with runtime
verification to abstract and verify our
protocols it's pretty exciting
collaboration and you know they're
really amazing and at this work they
have a paper that's being released right
now and and here you see that the main
contributors on the CVC on the and
runtime verification on this research
and they they basically did a mission
she a proof in talk of the safety and on
triviality properties of the abstract
consensus protocol for the full node and
the light node and here is the paper
give you a moment if you want to take a
photo of that there it is this is the
paper
this is proofs it goes in detail
about the form of verification of these
light and Pope client protocols these
they're abstract they only have safety
and on triviality they're not live at
this level of specification anyone will
check out the proofs here this is
like a github link to the actual proofs
if you're interested in that Ryo
Nakamura like I mentioned had has a
formal verification of the decision
detector III didn't make a QR code for
this that's kind of dumb I'm sorry go
check him out on Twitter look for this
tweet click on that link maybe see him
after and get it get it from him sorry
about the lack of QR code I don't know
what happened
Kasper labs is implementing the CBC a
CBC Kasper blockchain for production you
know quite different than a research
roadmap and they've you know they have
like a github that you can follow and is
quite active and they they came up with
this paper which also released today is
gives this leader based liveness
strategy for partial synchronous
networks and you know it's it's
basically it gives I think both
alignment strategy and the finality
criteria and here is the QR code the QR
code for that paper
the theorem foundation continues to
support our work sometimes I have to say
this people get confused you know still
very much being supported by the theorem
foundation in our research both directly
and indirectly through grants I have a
paper which I was planning on enough
releasing today but which unfortunately
I haven't been able to finish but I've
broke my back trying and I'm gonna try
to finish it super soon for all of you
to see and this is basically a abstract
kind of similar to the minimum consensus
for paper style but which also has
liveness properties in a synchronous
network it's a it's really really it's a
creates quite a cool paper it does it
gives formal problem statements absences
problem and goes through the correct by
construction process to show kind of how
the protocol can be derived from the
problem statements in a way that is
guaranteed to be correct and and they
kind of justifies a lot of the like the
minimal CDC Kasper paper and this one
with the liveness
so finally you know right after this I'm
hoping we will or some of us you know
anyone who's contributed to CBC Kasper
research will hopefully meet us right up
here and we'll have like a little
conversation about Susie Kasper research
if you have you have any questions that
you want answered please come and talk
to us hopefully it won't be just me and
other researchers will come to but you
know it's tough to them we're gonna do
an asking anything on online soon also I
have t-shirts limited-edition t-shirts
that I'm giving away not to everyone
please first I have to give away two
contributors so I know there's some of
you here give it away to contributors
first and then I'll and then I'll do
first-come first-serve after so the
first-come first-served will be tomorrow
but for now if you're a contributor and
you want a shirt come get it thank you
so much really appreciate
you