The Minimal Slashing Condition is a set of rules to work with many hashes and some number of nodes to finalize a block. It is carefully designed that if two incompatible blocks are finalized, then no matter how such a situation arises, there MUST exist some set of validators, with total size equal to at least 1/3 of recent active validator set, which sent messages that trigger some slashing condition.
A key goal of Casper (Proof of Stake) is that of achieving “economic finality”.
“A block B1 is economically finalized, with cryptoeconomic security margin $X, if a client has proof that either (i) B1 is going to be part of the canonical chain forever, or (ii) those actors that caused B1 to get reverted are guaranteed to be economically penalized by an amount equal to at least $X.” - Vitalik Buterin
Economic finality refers to one of two conditions:
- The condition where a sufficient number of validators have signed cryptoeconomic claims of the form "I agree to lose X in all histories where block B is not included". This gives clients assurance that either
(i) B is part of the canonical chain, or
(ii) validators lost a large amount of money in order to trick them into thinking that this is the case.
- The condition where a sufficient number of validators have signed messages expressing support for block B, and there is a proof that if some B' != B is also finalized under the same definition then validators lose a large amount of money. If clients see this, and also validate the chain, and validity plus finality is a sufficient condition for precedence in the canonical fork choice rule, then they get an assurance that either
(i) B is part of the canonical chain, or
(ii) validators lost a large amount of money in making a conflicting chain that was also finalized.
It is accomplished in Casper by introducing the concept of 'bonded validators; requiring validators to submit deposits in order to participate, and taking away their deposits if the protocol determines that they acted in some way that violates rules.
'Slashing Condition' is the set of rules which if violated by the validators in Casper, will end up slashing (deleting) the deposits. Slashing conditions are kind of law to the validators that they are not supposed to break. An honest validator follows the protocol (that defines a set of slashing conditions), that is guarenteed not to trigger any of the conditions that may end up loosing his deposit.
If a validator sends a signed message of the form
["PREPARE", epoch, HASH1, epoch_source1]
and a signed message of the form
["PREPARE", epoch, HASH2, epoch_source2]
where HASH1!= HASH2 or epoch_source1!= epoch_source2, but the epochvalue is the same in both messages, then that validator’s deposit is slashed (ie. deleted)
An honest validator is not supposed to send “PREPARE” message twice in the same epoch. “PREPARE” and “COMMIT” are terms borrowed from traditional Byzantine-fault-tolerant consensus theory. They are considered as being two different types of messages that are used in achieving consensus in Casper. Consensus will require two rounds of agreement, where PREPARE represents the first round and COMMIT represents the second round.
The intention is to make 51% attacks extremely expensive, so that even a majority of validators working together cannot roll back finalized blocks without undertaking an extremely large economic loss.
Slashing conditions need to satisfy two conditions:
- Accountable safety: It states that if two conflicting hashes get finalized, then it must be provably true that at least 1/3 of validators violated some slashing condition. This brings the idea of “economic finality”. If this happens, then we have mathematical proof that a large set of validators must have violated some slashing condition. "Evidence" of this fact can be sent into the Casper contract; expecting evidence is simultaneously easy to detect, and will effectively be submitted by a miner (because "stealable"). The validator's entire deposit will be destroyed except 4%, which is given to the evidence submitter as a "finder's fee".
Algorithm 1: every validator has exactly one opportunity to send a message of the form ["COMMIT", HASH]. If 2/3 of validators send a COMMIT for the same hash, that hash is finalized. Sending two COMMIT messages violates a slashing condition.
Now, if HASH1 and HASH2 both get finalized, then that means that each one has 2/3 commits, and so there must be 1/3 overlap, so 1/3 of validators get slashed (Diagram: Safety Proof A). It is an obvious proof that this algorithm is safe . But it is not plausibly live: if 1/2 commit A and 1/2 commit B (this could happen accidentally), then 1/6 of validators must voluntarily slash themselves in order to finalize a hash (Diagram: Safety Proof B).
Diagram*: Safety Proof A
Diagram*:Safety Proof B
Plausible liveness: It states that unless at least 1/3 of validators violated some slashing condition, there must exist a set of messages that 2/3 of validators can send which finalize some new hash without violating some slashing condition. It means, “it should not be possible for the algorithm to get ‘stuck’ and not be able to finalize anything at all”.
Algorithm 2: every validator has exactly one opportunity to send a message of the form ["COMMIT", HASH, epoch]. If 2/3 of validators send a COMMIT for the same hash with the same epoch number, that hash is finalized. Sending two COMMIT messages with different hashes with the same epoch number violates a slashing condition.
This gets around the problem in the previous algorithm, as if during one epoch we get a 50/50 situation then we can simply try again in the next epoch. But this introduces a safety flaw (no more safety): two different hashes can get finalized in different epochs (Diagram: Safety Proof C).
Diagram*: Safety Proof C
This is nontrivial, but possible to get both finalized in different epochs at the same time, it requires 4 slashing conditions, plus 1000 lines of code for Yoichi to formally prove that it actually works. These four slashing conditions are explained in Minimal Slashing Conditions by Vitalik.
If two hashes are both part of the same history then they can both get finalized, and in fact an ever-growing chain where more and more hashes at the end of the chain get finalized, then it is working as intended (Non conflicting hashes). The issue arises if hashes that are not part of the same history are conflicting. However, there is a proof that the four slashing conditions prevent two conflicting hashes from being finalized unless at least 1/3 of validators get slashed (Conflicting hashes).
Diagram*: Non conflicting hashes & Conflicting hashes
Economic rewards are added for the validators to send these PREPARE and COMMIT messages, so that enough messages get sent in time for finalization to actually happen.
Plausible liveness means that we theoretically can always finalize something, but we're repeatedly getting unlucky and never end up finalizing anything. To solve the problem of plausible liveness and ensure help achieve liveness, a mechanism is proposed called Proposal Mechanics. It proposes hashes, which the rest of the machinery (with PREPARE and COMMIT messages) then tries to finalize. But it may be faulty sometimes, so it’s the job of the slashing conditions to ensure that even if the proposal mechanism is faulty, there are no safety failures and the protocol can finalize something once the proposal mechanism stops being faulty.
Practical Byzantine Fault Tolerant (PBFT) is used to establish consensus in blockchain systems. This is one of the potential solutions to the Byzantine-fault-tolerant consensus algorithms, of which Minimal Slashing Condition is a key component.
In PBFT, every view (roughly equivalent to an epoch) is assigned a single validator, and that validator is free to propose whatever they want; they may misbehave by proposing nothing, proposing invalid hashes or proposing multiple hashes, but the other parts of the PBFT machinery ensure that such actions are not fatal, and the algorithm eventually switches over to the next epoch.
In PBFT, we can combine slashing conditions with different kinds of proposal mechanisms, if they satisfy below conditions:
the proposal mechanism must propose one hash per epoch, and it must be a valid hash.
the hashes must form a chain; that is, a hash submitted for epoch N must have a parent that was submitted for epoch N-1, a 2nd degree ancestor that was submitted for epoch N-2, etc.
the hashes must be hashes that the slashing conditions do not prevent validators from finalizing.
Fork choice rule
Rule that allows a blockchain to serve as the proposal mechanism for a consensus algorithm is called as a Fork choice rule. It is a function, evaluated by the client, that takes as input the set of blocks and other messages that have been produced, and outputs to the client what the “canonical chain” is. “Longest valid chain wins” is a simple fork choice rule and works well for PoW. GHOST is a more complicated and is there in Casper PoS.
Start off with HEAD being the genesis block.
Find the valid descendant of HEAD that has 2/3 prepares and the largest number of commits
Set HEAD to equal that descendant and go back to step 2.
When step 2 can no longer find a descendant with 2/3 prepares and any commits, use the blockchain’s underlying fork choice rule (longest-chain, GHOST, whatever) to find the tip.
A specific condition which help clients determine that a particular hash is finalized and can not be reverted back is called as 'Finality Condition'. A 'hash' is decided if 'COMMIT' message is received from two third of the active validators pool.
“A HASH is finalized if, for some particular epoch number, there exists a set of signed messages of the form
["COMMIT", epoch, HASH]
and if you add up the deposited balances of the validators that created these signed messages then you get an amount that is more than 2/3rd of the total deposited balances of the current active validator set.” - Vitalik Buterin
In other words, we can say “the hash was committed in some particular epoch by 2/3 of validators”, or “the hash has 2/3 commits in some particular epoch”. This finality condition is implemented in Casper version 1.
In full node, determining that a given hash is finalized is a two-step process of
(i) checking for the 2/3 commits, and
(ii) checking that the chain up to the hash is valid.
To make finality work for light clients, there are two approaches.
to add another kind of message that nodes can send (call it ["ATTEST", HASH, epoch] ), which has the effect that if this message is submitted into a chain where the given hash actually is the hash at that epoch, the validator gets a small reward, but if it is not then they pay a large penalty.
to give light clients access to various cryptoeconomic techniques that will allow them to verify data availability and validity very efficiently with the help of some weak honest minority assumptions; this will likely involve a combination of erasure codes and interactive verification.
Diagram* - Diagrams taken from Minimal Slashing Conditions by Vitalik.