Ethereum's CBC Casper consensus protocol


#1

Claim 1: CBC Casper is not Byzantine fault-tolerant because it attempts to prove correctness without considering liveness. It does not specify concrete decision-making mechanisms.

Source: https://medium.com/@muneeb/peer-review-cbc-casper-30840a98c89a

Evidence: CBC Casper paper draft

Argument: (see replies to this post)

Status: Unconfirmed


#2

Claim 2: CBC Casper does not consider other relevant, hard problems for achieving consensus in blockchains. Examples include reconciling chain forks, selecting which forks are valid, how reorganizations are detected and handled, recovering from accidental forks, and so on.

Source: https://medium.com/@muneeb/peer-review-cbc-casper-30840a98c89a

Evidence: CBC Casper paper draft

Argument: (see replies to this post)

Status: Unconfirmed


#3

Claim 3: CBC Casper deals with only one type of failure — the failure when nodes “equivocate” i.e., send self-conflicting messages. However, such failures are only a subset of faulty behavior: there are other failures that are harder to deal with that this paper does not address e.g., a malicious node that intentionally tries to prevent consensus (but does not equivocate).

Source: https://medium.com/@muneeb/peer-review-cbc-casper-30840a98c89a

Evidence: CBC Casper paper draft

Argument: (see replies to this post)

Status: Unconfirmed


#4

Elaborating on the CBC Casper peer review. Claims 1, 2, and 3 are more like statements to the incompleteness of the paper than pointing out specific flaws in the reasoning. Specifically:

Claim 1: CBC Casper is not Byzantine fault-tolerant because it attempts to prove correctness without considering liveness. It does not specify concrete decision-making mechanisms.

The examples in the paper (Section 4) show how the CBC Casper “estimator function” can be used to make decisions, but the tactic of using it this way is not discussed in the paper – i.e. a reader doesn’t have enough information to know whether or not the estimator function will be able to cause validators to consistently decide useful things, since this is not discussed in the proof.

The only time the estimator functions come up in the proof regarding decisions validators make is in the definition of “Decided_C” (Definition 3.10). The set of properties on the consensus values in the protocol that all correct validators make consistently in the absence of too many faults (Theorem 5) is not guaranteed to contain any useful properties. Referring to known results in BFT literature, the blog post shows one case where the fault threshold parameter has to be somewhat lower than the sum of all validator weights (the upper bound proven in Section 3) in order for useful properties to be decided.

Claim 2: CBC Casper does not consider other relevant, hard problems for achieving consensus in blockchains. Examples include reconciling chain forks, selecting which forks are valid, how reorganizations are detected and handled, recovering from accidental forks, and so on.

This would have been a nice-to-have, and indeed the paper has examples in Section 4 that sketch how to do this. However, the main result (the safety proof) doesn’t apply here – the reader can’t use it to make any conclusions about what the protocol can or cannot do, since the safety proof applies for all fault thresholds (but a liveness proof cannot do so).

Claim 3: CBC Casper deals with only one type of failure — the failure when nodes “equivocate” i.e., send self-conflicting messages. However, such failures are only a subset of faulty behavior: there are other failures that are harder to deal with that this paper does not address e.g., a malicious node that intentionally tries to prevent consensus (but does not equivocate).

The paper suggests that these are the only kind of faults considered Byzantine. However, there are other Byzantine faults that are not equivocation. For example, in a blockchain, a miner can simply mine and propagate blocks that build on old chain tips. As another example, in a voting system like a jury, a juror can simply disagree with the majority on purpose. Since the safety proof doesn’t discuss these kinds of faults, the reader learns nothing about whether or not a CBC Casper protocol is safe in their presence.


#5

For example, in a blockchain, a miner can simply mine and propagate blocks that build on old chain tips. As another example, in a voting system like a jury, a juror can simply disagree with the majority on purpose. Since the safety proof doesn’t discuss these kinds of faults, the reader learns nothing about whether or not a CBC Casper protocol is safe in their presence.

The concept of “decision” or “finality” in CBC Casper is safe under asynchrony, which means safe under all faults that are not equivocation, because such faults are indistinguishable from sufficiently high network latency.

Claim 1: CBC Casper is not Byzantine fault-tolerant because it attempts to prove correctness without considering liveness. It does not specify concrete decision-making mechanisms.

I wrote https://vitalik.ca/general/2018/12/05/cbc_casper.html yesterday; it provides more reasoning regarding liveness.

I think it should be possible to write up an academic proof for consensus under synchrony for a class of problems I call “divergence games”. Suppose you have a game where validators publish messages, and each message is either +1 or -1. If the total sum of valid messages a validator saw is positive, validators will try to publish +1, if it’s negative, validators will try to publish -1, and if it’s 0 validators will do either. If the average time between new valid messages is greatly above network latency, then I would claim that you can guarantee it will converge to + or - infinity assuming honest majority.

This would be a nice result because it’s general-purpose enough to cover (ideally) longest-chain PoW, longest-chain PoS, GHOST PoW, LMD GHOST PoS and other constructions.

Claim 2: CBC Casper does not consider other relevant, hard problems for achieving consensus in blockchains. Examples include reconciling chain forks, selecting which forks are valid, how reorganizations are detected and handled, recovering from accidental forks, and so on.

LMD GHOST does all of that! (see https://vitalik.ca/general/2018/12/05/cbc_casper.html)


#6

Hi Vitalik,

Thank you for your follow-up replies! I’ll do my best to respond (see inline).

I don’t know what you mean here. The proof in the paper shows that CBC Casper’s safety proof holds for all equivocation faults, but equivocation faults are not the same as faults where a validator intentionally casts a vote against the correct validators, and this “malicious vote” fault is definitely different from a message loss fault.

Safety under asynchrony does not come in to play here. Suppose instead that the network is synchronous and reliable. Correct validators would see the (malicious) validator vote for something other than what they voted for, but since the malicious validator votes once, no equivocation would be observed and correct validators would learn (and potentially act on) the malicious message. For example, consider the mutex lock problem in the review – even though Alice and Bob are both trying to acquire a lock, a malicious validator could claim that a different user Charlie is trying to acquire the lock (and always vote for Charlie no matter what). The safety proof is made in terms of only equivocation faults, and AFAICT does not describe how a CBC Casper protocol would tolerate malicious votes like this. But regardless, equivocation is fundamentally different from malicious voting, and malicious voting can happen undetected without being caused by network latency.

I look forward to reading a CBC Casper paper that formally describes these liveness properties and incorporates them into its safety proof :wink:

However, the point we were trying to make is that until the CBC Casper paper does this, then the safety proof is not informative – the reader can’t really conclude anything about what a protocol does when it is run, because the protocol is not guaranteed under the definitions to do anything useful.

Putting it in CBC Casper terms, there’s a non-empty subset of properties (call it the “liveness subset”) on consensus values whose truth value can only be determined by being able to correctly infer the state of other validators’ decisions (which, ostensibly, are encoded in the validators’ protocol states). The trouble is, these properties aren’t guaranteed to be consistently decided by all validators under the given safety proof – the set of properties they do decide is not guaranteed to intersect with this liveness subset.

In our review, we show that there exists a lower fault threshold than the safety proof provides whereby the detection of sufficiently many faulty validators (by weight) would prevent correct validators from consistently deciding on properties in the liveness subset – the intersection of the liveness subset and the properties they do decide would necessarily be empty for a lower fault threshold than the safety proof shows. This follows directly from known upper bounds on the number of faulty replicas a BFT protocol can tolerate while ensuring liveness.

What this means is that until CBC Casper is expanded to describe the liveness properties of the protocol family, the safety proof won’t tell us anything about how these protocols actually behave.

LMD GHOST does all of that! (see https://vitalik.ca/general/2018/12/05/cbc_casper.html)

I agree. However, LMD GHOST is only one estimator function out of an infinite number of valid estimator functions, and the CBC Casper paper is trying to make claims that hold for all of them. The existence of a CBC Casper protocol that uses a viable estimator function such as this does not prove that all CBC Casper protocols in the protocol family can address these problems. If you’re saying that all CBC Casper functions use LMD GHOST to address these problems, then this claim would be resolved (but at the expense of severely constraining the applicability of proofs of the CBC Casper family to only those protocols that use LMD GHOST).

Hope this helps clarify our reasoning! Thanks again for responding :slight_smile:


#7

One thing I think is interesting about the CBC consensus is that while there should be a global consensus of safety. There is no global liveness. In traditional protocols, the behavior of correct processes is homogeneous. Casper CBC introduces the notion of heterogeneity in to the network via the decision oracle. Correct nodes can select parameters for the decision oracle and depending on the number of faults in the network disagree with other nodes about the liveness of the network. CBC Casper demonstrates is that nodes can disagree about liveness but not about safety. This makes liveness an emergent property of the safe prototocol.

One of the pieces of complexity I think is noticeably missing in CBC Casper is guidance on how the decision oracle should paramterized and how those parameters might change over time. Should seeing censorship attack cause the correct node to decrease the number of signatures needed to progress? These are complex questions that will hopefully be analyzed in the future.


#8

This isn’t specific to CBC Casper – correct BFT processes exhibit heterogeneous behaviors. For example, consider the mutex example from our review – some validators process Alice’s request, while others process Bob’s request (heterogeneous behavior). However, all correct BFT processes must make the same decisions in order to achieve consensus (Casper or not).

What’s a decision oracle? It’s not a term in the CBC Casper paper. Is it defined elsewhere?

Consider a CBC Casper protocol that uses an estimator function that never terminates. This protocol is safe under the paper’s definition of safety, but is not live.

Consider a CBC Casper protocol that uses an estimator function that always decides every property of consensus values is False, for all consensus values. This protocol is safe under the paper’s definition, but not live.

Consider a CBC Casper protocol that uses an estimator function that decides only one property is True for all consensus values, and that property is specific to the validator (i.e. each validator has its own unique “favorite property”). This protocol is safe under the paper’s definition, but not live.

I’m not seeing how the safety proof says anything about the liveness of a CBC Casper protocol, in part because (according to Vlad) the estimator function is intentionally unspecified.

These are questions of liveness, which are not addressed in the CBC Casper paper.


#9

Agree. You can have protocols in the CBC family as defined that are not BFT under even synchrony (where BFT is the traditional definition of BFT; safe and live under some model of byzantine user behavior and some network model).

The paper does redefine BFT, which may be appropriate for a blockchain setting, but I’d like to see more rigorous arguments for why traditional definitions aren’t sufficient in the paper. Perhaps provide a straw man that is traditional BFT but clearly not good enough for a blockchain; something like what https://eprint.iacr.org/2016/454 attempts.

True, but I think this is by design. Would be nice to have some good intuition or example protocols for this eventually.

I agree BFT goes beyond equivocation. It is possible that @vbuterin’s claim is correct, and all other faults are indistinguishable from network latency of the messages received by some validator (this assumes every message sendable in the protocol could honestly be triggered by some execution where the messages seen are a subset of the global messages for any set of global messages). This would require very rigorous proof that I think is missing.

In general, byzantine behavior is assumed arbitrary because malicious incentives are extremely hard to model. I think moving away from such a model is dangerous, especially when your security guarantees are coming from economic analyses (that are thought to be more fragile in practice than simple fault counting).

In all, I agree with the review: CBC is not as-is a complete or clear defensible contribution to the BFT literature.

That being said, I think Vlad and co’s use of BFT in the paper is confusing. I’ve never seen advancements in BFT as a goal of the paper; I see this as an interesting methodology to construct existing protocols in that could reveal flaws in their design, as well as a general argument for economic analysis in the early stages of formal protocol construction. I think from these angles, the paper (though it needs refining with much more rigor and clarity) could definitely be an interesting contribution.


#10

@vbuterin thanks for this write up on casper. LMD Ghost intuitively makes a lot of sense to me. I have a follow up question in regards to your reasoning on liveness, where you say that:

Liveness in CBC Casper piggybacks off of the liveness of whatever the underlying chain algorithm is (eg. if it’s one-block-per-slot, then it depends on a synchrony assumption that all nodes will see everything produced in slot N before the start of slot N+1). It’s not possible to get “stuck” in such a way that one cannot make progress; it’s possible to get to the point of finalizing new blocks from any situation, even one where there are attackers and/or network latency is higher than that required by the underlying chain algorithm.

Can you unpack what you mean by this? Specifically, what happens if enough non-equivocating validators aren’t able to infer the state of other validators’ decisions because they aren’t consistently guaranteed to be decided, as @jude said?


#11

Claim 4: Casper CBC proves that nodes make consistent decisions even if they receive different messages, as long as there are less than t equivocation faults in their protocol states. It does so in two steps, first by guaranteeing that nodes will have common future protocol states (as long as there are less than t equivocation faults in the union of their protocol states), and then by showing that their decisions on properties of protocol states will be consistent. This result is then leveraged to guarantee the consistency of decisions on properties of consensus values.

Source: CBC Casper paper draft

Evidence: CBC Casper paper draft

Argument: (see replies to this post)

Status: Confirmed


#12

The proof is correct. However, it is not informative because it does not show that any useful properties will be consistently decided – the proof would be correct even if all the properties consistently decided are trivial (e.g. “the consensus value C is an integer”).


#13

@jude You may have already seen this video but it gives some background on the thought behind “Correct by Construction” https://slideslive.com/38911621/cbc-casper-design-philosophy

The claim is that the less defined protocol (i.e. CBC Casper only proving Safety) is okay because continuing to define the protocol in the future (i.e. proving liveness) doesn’t disrupt theorems that hold for the less defined protocol specification.

Do you think this “Correct by Construction” approach fundamentally make sense for a BFT consensus algorithm?

Based on the peer review, you say that even though validators might make consistent decisions if there are fewer than t faults, any validator behavior that provides liveness would place tighter bounds on fault threshold t than what the safety proof suggests.

So it seems that you fundamentally disagree with the “Correct by Construction” approach and are suggesting that further defining this less defined protocol WILL disrupt the theorems that held for the less defined protocol. Am I right?


#14

This is not true for Casper CBC. Casper CBC’s safety proof shows all validators (replicas) make consistent decisions on consensus value properties for any fault threshold. The reason this proof is correct right now is because the proof does not try to show that the properties have to be liveness properties. However, once Casper CBC is updated to make a liveness guarantee, the safety proof will need to be altered to show, at a minimum, that liveness properties will not be consistently decided after a certain (lower) fault threshold.

Yes.

The peer review does not make a comment on the general approach. I think the “correct by construction” approach means that they’re trying to (1) formally specify a BFT consensus protocol family, (2) show that the spec only admits protocols that exhibit certain safety and liveness properties, and (3) prove the existence of a protocol that is consistent with the specification (i.e. by constructing it and formally verifying it against the specification). If so, then I’d agree that the general approach is a valid one – this is certainly doable, and has been done before. But, I would welcome clarification from the Casper CBC team to know exactly what they mean when they say “correct by construction”.

The peer review only comments on the particular claims made in the paper. I’m sure the team could refine the proofs later once they know what liveness guarantees they want to make; the point we were trying to make is that they will need to be refined before they can say anything about liveness.


#15

very helpful. logical and makes sense.

That video I linked is the best understanding I can find on what CBC means.