The CBC Casper Roadmap by Vlad Zamfir (Devcon5)

Transcript

We're going to talk today about the CBC Casper roadmap and it's going to be a little bit less action-packed than the normal Devcon talk. Um so here is my little outline. I'm going to I'm going to be talking about the roadmap as a research roadmap as opposed to an implementation roadmap or like um roadmap for developers. I'm going to talk about the relationship between my roadmap and the Ethereum roadmaps. I'm going to talk about our past and future work cuz somehow the roadmap is made up of all the stuff we've done and all the stuff we're going to do or planning to do.

And then I'm going to talk about and then I'm going to give some resources and announcements. So, CBC Casper roadmap is a is like I was saying, it's a research and architecture roadmap. The outputs of this roadmap are research and specifications. You know, we don't like the the goal of the roadmap is to produce architecture, to produce, you know, research in the form of distributed systems, computer science. Um, 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 matches the specifications, you'll get

all the benefits of the architecture. So, somehow the CBC 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 then any way that you implement the architecture will inherit the properties of the architecture. So, um you know, if there's like if we prove that that this architecture has a property, then any of the many ways that you can 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 then from the

features or the properties of these protocols. Um they are um But but you know, we're we are going to um So so we're kind of independent from the engineering effort. So if we ended architecture and then engineering kind of happens after. Um 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 we're going to provide support even though it's not the road map to implement it. If the road map is to come up with the architectures and and to the to do the research.

Um it's a research road map. It's all about building correct by construction consensus protocols. We uh 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 dis to dis to develop these protocols. So we really formally state the design requirements and abstractly state protocol statements.

Um 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. Um and so you know, we 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 in not just any consensus protocols, we want scalable proof of stake consensus protocols that have the same network overhead as Nakamoto consensus. You know, we want to be able to have blockchains that work on an internet scale that don't have uh crazy overhead like a traditional consensus protocol.

Um and but I actually have the same overhead as Nakamoto consensus or comparable to the overhead of current Ethereum. Um 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, non-triviality, and liveness. And also a bunch of other requirements like for example being able to make this ideal um theoretically optimal overhead trade-off. And also we're interested in scalability uh in you know through sharding and basically uh which we understand entirely inside a consensus protocol framework.

Um where you know if you if you went to the sharding workshop yesterday, um that was all about that. So I'm not going to really touch on it now. Um so we have a really deeply formalistic approach to protocol design. We are formal from the very start. We never engage in um trial and error in the normal kind of development fashion. We we don't implement stuff until we know for sure that it's correct. We do a lot of math before this a single line of code.

There's a ton of math before this a single line of code. Um it's a deeply deeply formalistic process and it takes a 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 it's correct by construction process. And it's also guaranteed 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.

Uh and and and that is like one of the big appeals I think of the road map is that the it's the is 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. Um So that's the basic that's the basic idea like what it is. It's a research roadmap. It doesn't tell you too much, but before I go into the items of the roadmap we're going to talk about the relationship between the CBC Casper roadmap and the Ethereum roadmaps. So in some ways we're completely independent of the Ethereum roadmaps.

You know, we're a research roadmap. The Ethereum roadmaps are roadmaps for deployment on Ethereum mainnet. Um but you know, some ways you know, you know, CBC Casper research has you know, made its way into Ethereum 2.0. Um Um and maybe it'll make its way into Ethereum 3.0. Question mark because it's not really clear yet what Ethereum 3.0 is. Um one of the things that is probably most famous that came out of CBC Casper research is the latest message driven ghost fork choice rule that is featured in the beacon chain.

Um another thing is Vitalik made a proposal to add the CBC Casper finality mechanism to the beacon chain. Um so somehow the CBC Casper research flow even the research roadmap flows into Ethereum 2.0 research at least a little bit. Um in some ways uh you know, so in some ways actually the Ethereum 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, um that's our goal. We want to build protocols that people really want to implement because of their simplicity, elegance, utility, properties etc.

Um so we have but the Ethereum roadmaps are not in any way blocked on the CBC Casper roadmaps. You know, there there's no no one's waiting for us to finish our research before implementing protocols. Um so they're they're really they're they're really are in some ways very independent of us. Great. So now I'm going to talk about CBC Casper, the CBC Casper roadmap in terms of, you know, what have actually we done so far and you know, what are we going to do in the future? Before I start, I'm just going to mention that um the CBC the the Casper research started before the split between CBC Casper and Casper FFG.

Casper research started off as proof of stake research into, you know, economically secure proof of stake where we can have like a equilibrium to follow the protocol that's really robust, where we have where we we use security deposits in order to make uh the equilibrium as robust as possible so that we can have penalties to to make it so that that equilibrium is not just an epsilon equilibrium, but like a a a very robust equilibrium. And then basically what happens is um 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 them to incentivize, like a specific protocol.

And so the CBC Casper roadmap really represents the distributed systems research that is going to be incentivized in proof of stake. It doesn't represent proof of 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 proof of stake research that came before it. So you need proof of stake research and then distributed system research where Vitalik and I split off into different protocols, the Casper FFG versus Casper CBC. Um and so this is going to be about distributed systems. This is a a distributed systems roadmap. You're not going to see anything about proof of stake incentives here. Not because it's not in like some other roadmap, it's just that CBC Casper is specifically a

distributed systems roadmap. So basically what is the roadmap? Well, any roadmap is basically everything you've done already and everything you're planning to do in the future. Um it's kind of like a map though like over time, like you know what you're supposed to accomplish to get to your goals. Um and so I'm going to talk about all the past work that we've done. Uh 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 all work ends up leading to a milestone that is like especially in research uh that is like something that you can present right.

So the first the first thing that really kicked off CBC Casper research was well beyond just me hearing about and learning about CBC protocol design is the CBC Casper message type. This is something Greg Meredith and I came up with in August 2016 uh when we were trying to come up with you know just the preliminary infrastructures so we can state a CBC consensus problem. In August month later um came up with for the first time this safe and non-trivial binary consensus protocol which I presented at Devcon in Shanghai in Shanghai.

Um it um you know used this idea of an ideal adversary to argue about security uh which now we we replaced with the idea of safety oracle um and but it but it was like you know the a real milestone like a safe non-trivial consensus protocol. It's like a real real real milestone. June 2017 so a couple a few months later LMD Ghost was first specified. This happened um when Carl who just spoke asked me how we're ever going to turn from binary consensus to blockchain consensus. He was like frustrated and concerned. Carl and I were working together at the time on this on the binary consensus protocol.

And I was like I just gave it a try and somehow um Oh. Sorry. I'm looking over here at the next slide. So, actually before the before the fork choice rule came up, Yoichi did a formal verification of the safety of the binary consensus protocol. Um in March 2017. And then in June, the latest message-driven ghost made its first appearance as a specification, um you know, when Carl asked me this question and I and I went and adapted the binary consensus protocol to the latest message-driven ghost protocol with very very minor change.

Then, in July 2017 at the IC3 Ethereum boot camp, uh the LMD ghost was first implemented. I worked together with John Levy to to implement it. I did most of the work, but he was definitely there and contributing. Um In November 2017, we came up with our first atomic cross-shard fork choice proposal that guarantees that, you know, um cross-shard communications are are are are are atomic. It's like super important property. Um and uh this was actually the first um sharding solution that ever came across CBC Casper research is this atomic cross-shard uh solution with merge blocks, which are blocks that exist on

two chains at once, and they're in the chains of both both of them. So, they have to kind of synchronize exactly at that height. And then later, um quite a quite a lot later, uh we came up with the uh cross-shard message um model which which has um the ability to send a message and not have it be received right away, but have it received just in some time. You know, and then and this is much more friendly to prevent or blocks from being orphaned. It's it's a much more realistic cross-shard communication model, and still we have atomicity, although a slightly different notion.

It's more like atomicity at finality than atomicity just in the fork choice rule. The way that the merge block The the merge block thing any four-choice rule any moment you have this atomicity property. With this one, there's a there's a time when you're when sent but not yet received where the atomicity is not really there, but at finality it's guaranteed to be there. Like you can never finalize a send without the receive being eventually finalized. You can never um you know, have a finalized not sent and a finalized receive. It would just be a violation of the protocol that kind of I mean the protocol guarantees that that won't happen. So, like if you follow the protocol, that that's just impossible.

Um in August of 2018, we came up with the first correct and complete safety oracle decision detector. And this is a an Ethereum Stanford like math Olympics workshop. I don't really know what I don't know remember what it's called. Um Greg Price came up with this who isn't in in the community, but he's you know, he he comes to these hackathon kind of like you know, math hacking events. Um and we had a long history of struggling for a very long time before this this this one specification for detecting safety um especially because especially in the cases of all the cases of equiv- equivocations, you know, of like who sees what equivocations because it gets

complicated when different validators see different equivocations and when you have to reason about the proof while they're equivocating. So, it turns out that this was this was a really challenging thing and we had a real professional mathematician like math Olympian solve it. Um September 2018, we did the first implementation of the cross-shard message uh system. And here's this GIF 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 atomicity of these communications between the two shards.

Um in October 2018, we did our first specification of um sorry, for implementation. I I don't know when the specification happened, I guess. Uh of the multi-level shard hierarchy with message routing and shard balancing. So, this is like taking it to the next level, right? Rather than just having two shards that communicate a little bit in between them, we want to have many shards that do routing. And we want to not have a fixed shard hierarchy, we want to have a the ability to change shards. This is an example of a two-shard system with a root shard and a child shard changing positions. In some way, there's no such thing as a root shard and a child shard anymore, there's only root blocks and and child blocks. At every moment in the fork choice rule, maybe one of them is the root.

But I mean, 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 in the moment that moment in the fork choice, the parent has said, "Look, I'm I'm not the root anymore." And then the child hasn't picked that up yet. And so, they're both they're both the children of the root. Actually, there is no root for that one moment. But then when the child eventually receives that message, which they have to do because of the nature of the fork choice rule, um you know, the child becomes the parent. And then and and and with single message hops like this that are atomic, you can implement routing, which guarantees with the same atomicity property that we can go from one shard to another through any number of shards. This uses routing protocol as this uses like a routing

routing table system. The and the the tables get updated as the shards change position. Because I mean, if the shards were at fixed position, you kind of have static routing tables. You have to just do source routing, calculate from the source exactly what the route's going to be. But because the shards 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. Um in November 2018 at Eth Devcon, I I I released this uh minimal CBC Casper protocol paper, which described abstractly a family of consensus protocols uh really really formally.

Um and this is kind of represented a very general abstraction of uh what we had done before with like the binary consensus protocol or the blockchain consensus protocol. Or we had a whole bunch of other ones like a integer consensus protocol. Um And and and this kind of really abstracted them and formalized it in a way and wrote when we wrote the proofs down in incredible detail. Just way too much detail. Um and then um next month we had the first formal CBC Casper light client specification. Which won't see the light of day until today actually.

Um and this is kind of cool because originally the CBC Casper specification it uh has message nesting instead of message linking and so the messages just get really big. And that's not really practical people don't like to see that even though from the point of view of like the semantics in the math like it's still a non-trivial safe whatever because that's this protocol. Um so we have light client specification as of November 20 20 2018. Number 20 February 2019 another one of these um Ethereum Stanford Math Olympic hack things.

I wish I knew what they were called. Uh we came up with Daniel Kane with working with Greg Price who came up with the original complete correct safety detector slash decision detector. Um came up with the with an efficient Oracle making decisions. Which is a big deal because that other one is computationally quite inefficient. Uh and this is also like yeah quite heavy lifting that was done. Um in May 2019 the first two liveness strategies based on the leaders for CBC Casper were specified by researchers at the Casper Labs team.

Um actually Daniel Kane who was on contract with them and Andreas Spackeler. Um they were both produced in almost immediate sequence like within like a week of each other. It's like a leader based CBC Casper liveness strategy where a leader synchronizes everyone and guarantees that they go through the same states and in order to make decisions. Uh also the same month but towards the end um came up with the first liveness strategy based on fault rejection for CBC Casper, which is uh quite a different strategy.

It 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 a lightning strategy. Um then at the IC3 Ethereum 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-shard messages was at the 2018 2018 IC3 Ethereum bootcamp. And this is where Aditya came onto the CBC Casper team and like immediately started writing proofs and he really helped with the sharding stuff and has been helping with it ever since. Um so and then the implementation happened obviously after the specification. And that was I guess like June 2018 or something like that.

So, now in June 2019, we came up with like the efficient efficient algorithms for LMD Ghost, uh updating the safety detector, uh and you know, other other kind of efficiency stuff to do with with Casper. In July 2019, um Sebastian Zaini came up with the first asynchronous probabilistic liveness strategy for CBC Casper, um which is you know, it's it's probabilistic and it uses the common coin model where basically everyone's flipping coins and then eventually they all flip the same coin and it ends up being live.

Uh um um the first partial synchrony thing uh first first partial synchrony specification for CBC Casper um I came up with in July 2019 um and and this was um also based on fault detection, but now instead of faults being perfectly reliably detectable as in synchrony, they're not and so it's it's quite a lot more complicated. And then the um Oh, we got the first formal verification of um safety and non-triviality of the full and light clients, the abstract ones.

Um this is done by runtime verification including um a bunch of people who you're going to see listed later, so I don't want to I'll just save a little time here. The We also had the same same same month of first formal verification of efficient safety safety Oracle detection by Riya Nakamura who is here also. And also we had in the same month the first partially synchronous specifications for the leader protocols that Daniel Kane basically pioneered.

And that's kind of all the major roadmaps, maybe milestones on the roadmap, 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 maybe have noticed that I haven't published in, you know, you haven't seen yet. So we need to, you know, we need to some some of the stuff needs to be formalized, that's abstracted, verified. You know, 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 where like you're paranoid absolutely sure under any circumstance that is correct with all of it. We also have to, you know, abstract it and so we can have like the

results that we have in the most general terms possible so that we're they're as useful as possible for providing most general architecture that which which basically provides the guarantees to the most possible implementations. And we also have to do a lot of documentation and peer review of 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. Um Here's some more past work, you know, validator rotation, load balancing, sharding client strategies. These are these are things that are not done but which are necessary for the scalable proof of stake or scalable distributed system thing.

You know, also and and uh 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 formalities, completeness, etc. that we're used to and that we expect. Um we also have like just future work that is just hasn't really been started that much yet. Um abstraction of 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 that we can have the most general infrastructure possible.

Um we have to verify all of our liveness proofs, you know, both by hand and formally to the to the much bigger more extent than we have already. And we want to talk about performance. You know, we I 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. Um 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 thinking about mining. I was

thinking about the clients and how they just have to download like one header per block or very little information. Um you know, we have we have a in CBC Casper we have this requirement that the that the protocol fault that the fault tolerance thresholds of the protocol are not in the consensus protocol, but they're client and validator side. And so we have to give strategies for clients or give at least some best practices for clients to for choosing these thresholds because not all thresholds are going to be equally good uh or equally useful. Um so you know, this is like an just a whole bunch of stuff that needs to be done. There's probably more future work that it that isn't listed here. But but but if this if this is all done, then and all the stuff that we already claimed is done as so far is done, then

actually we're pretty pretty close to having a scalable distributed uh consensus protocol that has um all of the security and overhead properties that we want. Um and also liveness. Um which is super important property that uh is shockingly difficult to provide. Basically, you 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. It means that 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 we're collaborating with Runtime Verification to abstract and verify our protocols. Um it's pretty exciting collaboration. And you know, they're really amazing at this work. Um they have a paper that's being released right now. Um and and here you can see that the main contributors on the CBC on the Runtime Verification on this research. And they they basically did a machine a proof in in Coq of the safety and non-triviality properties of the um abstract consensus protocol for the full node and the light node.

And here is the paper. Um give you a moment if you want to take a photo of that. Um um there it is. This is the paper. Um this is Coq proofs. It goes in detail about the formal verification of these light and full client protocols. These are abstract. They only have safety and non-triviality. They're not live at this level of specification. And you can also check out the Coq proofs here. This is like a GitHub link to the actual proofs if you're interested in that. Uh Ryo Nakamura, like I mentioned, had uh has this formal verification of the decision detector.

Uh I I I didn't make a 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. Uh Casper Labs is implementing the CBC a CBC Casper blockchain uh for production. You know, it's quite different than a research road map. Um and they've, you know, they have like a GitHub that you can follow and it's quite active. And they they came up with this paper, which also released today, um is gives this leader-based liveness strategy for partial synchronous networks.

Um and uh you know, it's it's basically it gives I think both the liveness strategy and the finality criteria. Um and here is the QR the QR code for that paper. Um the Ethereum Foundation continues to support our work. Sometimes I have to say this. People get confused. You know, we're still very much being supported by the Ethereum Foundation in our research both directly and indirectly through grants.

Um I have a paper which I was planning on releasing today, but which unfortunately I haven't been able to finish, but I broke my back trying and I'm going to try to finish it super soon for all of you to see. And this is basically a abstract kind of in similar to the minimal consensus protocol paper style, but which also has liveness properties in a synchronous network. It's a it's really really it's a it's quite a cool paper. It does it gives formal problem statements abs for the consensus problem and goes through the correct by construction process uh to 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 it kind of justifies a lot of the like the minimal CBC Casper paper and this one with the liveliness. Um so finally, uh you know, right after this I'm hoping we will or some of us, you know, anyone who's contributed to CBC Casper research hopefully meet us right out here and we'll have like a little uh conversation about CBC Casper research if you have you have any questions that you want answered. Um please come and talk to us. Hopefully, it won't be just me and the other researchers will come too. Uh but, you know, let's stop the event. Um we're going to 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 to contributors. So, I know there's some of you here. Give away to contributors first and then I'll and then I'll do a first come first serve after. Um so, the first come first serve 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 it.