Security Analysis of Crosslink

This document analyses the security of Crosslink in terms of liveness and safety. It assumes that you have read The Crosslink Construction which defines the protocol.

Liveness argument

First note that Crosslink intentionally sacrifices availability if there is a long finalization stall.

It would still be a bug if there were any situation in which ${\Pi }_{\mathrm{bc}}$ failed to be live, though, because that would allow tail‑thrashing attacks.

Crosslink involves a bidirectional dependence between ${\Pi }_{\mathsf{bft}}$ and ${\Pi }_{\mathsf{bc}}$. The Ebb‑and‑Flow paper [NTT2020] argues in Appendix E ("Bouncing Attack on Casper FFG") that it can be more difficult to reason about liveness given a bidirectional dependence between protocols:

To ensure consistency among the two tiers [of Casper FFG], the fork choice rule of the blockchain is modified to always respect ‘the justified checkpoint of the greatest height [*]’ [22]. There is thus a bidirectional interaction between the block proposal and the finalization layer: blocks proposed by the blockchain are input to finalization, while justified checkpoints constrain future block proposals. This bidirectional interaction is intricate to reason about and a gateway for liveness attacks.

The argument is correct as far as it goes. The main reason why this does not present any great difficulty to proving liveness of Crosslink, is due to a fundamental difference from Casper FFG: in Crosslink the fork‑choice rule of ${\Pi }_{\mathrm{bc}}$ is not modified.

Let $\mathcal{S}$ be the subset of bc‑blocks $\{B:\text{is-coinbase-only-block}(B)\text{ and }\text{is-safety-block}(B)\}$. Assume that $\mathcal{S}$ is such that a bc‑block‑producer can always produce a block in $\mathcal{S}$.

In that case it is straightforward to convince ourselves that the additional bc‑block‑validity rules are never an obstacle to producing a new bc‑block in $\mathcal{S}$:

• The changes to the definition of contextual validity do not interfere with liveness, since they do not affect coinbase transactions, and therefore do not affect blocks in $\mathcal{S}$. That is, the bc‑block‑producer can always just omit non‑coinbase transactions that are contextually invalid.
• The Genesis rule doesn't apply to new bc‑blocks.
• The Valid context rule and Extension rule are always satisfiable by referencing the same context bft‑block as the parent bc‑block.
• The Finality depth rule always allows the option of producing a safety block, and therefore does not affect blocks in $\mathcal{S}$.

The instructions to an honest bc‑block‑producer allow it to produce a block in $\mathcal{S}$. Therefore, ${\Pi }_{\mathrm{bc}}$ remains live under the same conditions as ${\Pi }_{\mathrm{origbc}}$.

The additional bft‑proposal‑validity, bft‑block‑validity, bft‑finality, and honest voting rules are also not an obstacle to making, voting for, or finalizing bft‑proposals:

• Because ${\Pi }_{\mathrm{bc}}$ is live, there will always be some point in time at which a fresh valid bc‑header chain that satisfies both the Increasing score rule and the Tail confirmation rule exists for use in the $P.headers\_bc$ field.
• If no fresh valid bc‑header chain is available, the Increasing score rule and Tail confirmation rule allow an honest bft‑proposer to choose $headers\_bc$ to be the same as in the previous bft‑block. So, if liveness of ${\Pi }_{\mathrm{origbft}}$ depends on an honest proposer always being able to make a proposal (as it does in adapted‑Streamlet for example), then this requirement will not be violated.
• The changes to voting are only requiring a vote to be for a proposal that could have been honestly proposed.
• The bft‑finality rules are unchanged from origbft‑finality.

Therefore, ${\Pi }_{\mathrm{bft}}$ remains live under the same conditions as in Snap‑and‑Chat applied to ${\Pi }_{\mathrm{origbft}}$.

The only other possibility for a liveness issue relative to Snap‑and‑Chat would be if the change to the construction of ${\mathsf{LOG}}_{\mathrm{fin}}$ could cause it to stall, even when ${\Pi }_{\mathrm{bft}}$ and ${\Pi }_{\mathrm{bc}}$ are both still live.

However, liveness of ${\Pi }_{\mathrm{bft}}$ and the Increasing score rule together imply that at each point in time, provided there are sufficient honest bft‑proposers/validators, eventually a new bft‑block with a higher-scoring snapshot will become final in the context of the longest bft‑valid‑chain. ==TODO make that more precise.==

Because of the Extension rule, this new bft‑block must be a descendent of the previous final bft‑block in the context visible to bc‑block‑producers. Therefore, the new finalized chain will extend the old finalized chain. It could be the case that all of the new transactions are sanitized out, but that would only happen if they double‑spend or use outputs that were nonexistent in the context computed by $\text{bda-ctx}$ at the point at which they are to be contextually checked.

Finally, we need to show that Safety Mode is only triggered when it should be; that is, when the assumptions needed for liveness of ${\Pi }_{\mathrm{bft}}$ are violated. Informally, that is the case because, as long as there are sufficient honest bc‑block‑producers and sufficient honest bft‑proposers/validators, the finalization point implied by the $context\_bft$ field at the tip of the bc‑best chain in any node's view will advance fast enough for the finalization gap bound $L$ not to be hit. This depends on the value of $L$ relative to $\sigma$, the network delay, the hash rate of honest bc‑block‑producers, the number of honest bft‑proposers and the proportion of voting units they hold, and other details of the BFT protocol. ==TODO: more detailed argument needed, especially for the dependence on $L$.==

Safety argument

Discussion

The Extension rule ensures that, informally, if a given node $i$'s view of its bc‑best‑chain at a depth of $\sigma$ blocks does not roll back, then neither does its view of the bft‑final block referenced by its bc‑best‑chain, and therefore neither does its view of ${\mathsf{LOG}}_{\mathrm{fin},i}^t$.

This does not by itself imply that all nodes are seeing the "same" confirmed bc‑best‑chain (up to propagation timing), or the same ${\mathsf{LOG}}_{\mathrm{fin},i}^t$. If the network is partitioned and ${\Pi }_{\mathrm{bft}}$ is subverted, it could be that the nodes on each side of the partition follow a different fork, and the adversary arranges for each node's view of the last final bft‑block to be consistent with the fork it is on. It can potentially do this if it has more than one third of validators, because if the validators are partitioned in the same way as other nodes, it can vote with an additional one third of them on each side of the fork.

This is, if you think about it, unavoidable. ${\Pi }_{\mathrm{bc}}$ doesn't include the mechanisms needed to maintain finality under partition; it takes a different position on the CAP trilemma. In order to maintain finality under partition, we need ${\Pi }_{\mathrm{bft}}$ not to be subverted (and to actually work!)

So what is the strongest security property we can realistically get? It is stronger than what Snap‑and‑Chat provides. Snap‑and‑Chat is unsafe even without a partition if ${\Pi }_{\mathrm{bft}}$ is subverted. Ideally we would have a protocol with safety that is only limited by attacks "like" the unavoidable attack described above --- which also applies to ${\Pi }_{\mathrm{bc}}$ used on its own.

Proof of safety for LOG_fin

In order to capture the intuition that it is hard in practice to cause a consistent partition of the kind described in the previous section, we will need to assume that the Prefix Agreement safety property holds for the relevant executions of ${\Pi }_{\mathrm{bc}}$. The structural and consensus modifications to ${\Pi }_{\mathrm{bc}}$ relative to ${\Pi }_{\mathrm{origbc}}$ seem unlikely to have any significant effect on this property, given that we proved above that they do not affect liveness. ==TODO: that is a handwave; we should be able to do better, as we do for ${\Pi }_{\mathrm{bft}}$ below.== So, to the extent that it is reasonable to assume that Prefix Agreement holds for executions of ${\Pi }_{\mathrm{origbc}}$ under some conditions, it should also be reasonable to assume it holds for executions of ${\Pi }_{\mathrm{bc}}$ under the same conditions.

Recall that $\mathsf{LF}(H):=\text{bft-last-final}(H.context\_bft)$.

Using the Prefix Lemma once for each direction, we can transfer the Prefix Agreement property to the referenced bft‑blocks:

(The notation $B⪯{⪰}_{\ast }C$ means that either $B{⪯}_{\ast }C$ or $C{⪯}_{\ast }B$. That is, "one of $B$ and $C$ is a prefix of the other".)

Recall that $$\begin{array}{rcl}\text{san-ctx}& ::& [\text{bc-chain}]\to \text{bc-context}\\ \text{san-ctx}(S)& :=& \mathsf{sanitize}(\mathsf{concat}([\text{chain-txns}(C)\text{ for }C\text{ in }S]))\\ \mathsf{LF}(H)& :=& \text{bft-last-final}(H.context\_bft)\\ \text{fin}& ::& \text{bc-block}\to [\text{bc-chain}]\\ \mathsf{fin}(H)& :=& [\mathsf{snapshot}(B)\text{ for }B{⪯}_{\mathrm{bft}}\mathsf{LF}(H{\lceil }_{\mathrm{bc}}^{\sigma })]\\ \text{fin-ctx}(H)& :=& \text{san-ctx}(\mathsf{fin}(H))\\ \text{bda-ctx}(H,\mu )& :=& \text{san-ctx}(\mathsf{fin}(H)||[H{\lceil }_{\mathrm{bc}}^{\mu }])\\ {\mathsf{LOG}}_{\mathrm{fin},i}^t& :=& \text{context-txns}(\text{fin-ctx}({\mathsf{ch}}_i^t))\\ {\mathsf{LOG}}_{\mathrm{bda},i,\mu }^t& :=& \text{context-txns}(\text{bda-ctx}({\mathsf{ch}}_i^t,\mu ))\end{array}$$

Because $\mathsf{fin}$ takes the form $\mathsf{fin}(H):=[f(X)\text{ for }X{⪯}_{\mathrm{bft}}g(H)]$, we have that $g(H){⪯}_{\mathrm{bft}}g(H^{\prime })⟹\mathsf{fin}(H)⪯\mathsf{fin}(H^{\prime })$. (This would be true for any well‑typed $f$ and $g$.)

By this observation and the Prefix Agreement Lemma, we also have that, in an execution of Crosslink where ${\Pi }_{\mathrm{bc}}$ has the Prefix Agreement safety property at confirmation depth $\sigma$, for all times $t$, $t^{\prime }$ and all nodes $i$, $j$ (potentially the same) such that $i$ is honest at time $t$ and $j$ is honest at time $t^{\prime }$, $\mathsf{fin}({\mathsf{ch}}_i^t)⪯⪰\mathsf{fin}({\mathsf{ch}}_j^{t^{\prime }})$.

Because $\mathsf{sanitize}$ only considers previous state, $\text{context-txns}$ ∘ $\text{san-ctx}$ must be a prefix-preserving map; that is, if $S_1⪯S_2$ then $\text{context-txns}(\text{san-ctx}(S_1))⪯\text{context-txns}(\text{san-ctx}(S_2))$. Therefore:

Notice that this does not depend on any safety property of ${\Pi }_{\mathrm{bft}}$, and is an elementary proof. ([NTT2020, Theorem 2] is a much more complicated proof that takes nearly 3 pages, not counting the reliance on results from [PS2017].)

In addition, just as in Snap‑and‑Chat, safety of ${\mathsf{LOG}}_{\mathrm{fin}}$ can be inferred from safety of ${\Pi }_{\mathrm{bft}}$, which follows from safety of ${\Pi }_{\mathrm{origbft}}$. We prove this based on the Final Agreement property for executions of ${\Pi }_{\mathrm{origbft}}$:

The changes in ${\Pi }_{\mathrm{bft}}$ relative to ${\Pi }_{\mathrm{origbft}}$ only add structural components and tighten bft‑block‑validity and bft‑proposal‑validity rules. So for any legal execution of ${\Pi }_{\mathrm{bft}}$ there is a corresponding legal execution of ${\Pi }_{\mathrm{origbft}}$, with the structural additions erased and with the same nodes honest at any given time. A safety property, by definition, only asserts that executions not satisfying the property do not occur. Safety properties of ${\Pi }_{\mathrm{origbft}}$ necessarily do not refer to the added structural components in ${\Pi }_{\mathrm{bft}}$. Therefore, for any safety property of ${\Pi }_{\mathrm{origbft}}$, including Final Agreement, the corresponding safety property holds for ${\Pi }_{\mathrm{bft}}$.

By the definition of $\mathsf{fin}$ as above, in an execution of Crosslink where ${\Pi }_{\mathrm{bft}}$ has Final Agreement, for all times $t$, $t^{\prime }$ and all nodes $i$, $j$ (potentially the same) such that $i$ is honest at time $t$ and $j$ is honest at time $t^{\prime }$, $\mathsf{fin}({\mathsf{ch}}_i^t)⪯⪰\mathsf{fin}({\mathsf{ch}}_j^{t^{\prime }})$. Therefore, by an argument similar to the one above using the fact that $\text{context-txns}$ ∘ $\text{san-ctx}$ is a prefix-preserving map:

Proof of safety for LOG_bda

From the two ${\mathsf{LOG}}_{\mathrm{fin}}$ Safety theorems and the Ledger prefix property, we immediately have:

The above property is not as strong as we would like for practical uses of ${\mathsf{LOG}}_{\mathrm{bda}}$, because it does not say anything about rollbacks up to the finalization point, and such rollbacks may be of unbounded length. (Loosely speaking, the number of non-Safety Mode bc‑blocks after the consensus finalization point is bounded by $L$, but we have also not proven that so far.)

As documented in the Model for BFT protocols section of The Crosslink Construction):

For each epoch, there is a fixed number of voting units distributed between the players, which they use to vote for a $\ast$bft‑proposal. We say that a voting unit has been cast for a $\ast$bft‑proposal $P$ at a given time in a $\ast$bft‑execution, if and only if $P$ is $\ast$bft‑proposal‑valid and a ballot for $P$ authenticated by the holder of the voting unit exists at that time.

Using knowledge of ballots cast for a $\ast$bft‑proposal $P$ that collectively satisfy a notarization rule at a given time in a $\ast$bft‑execution, and only with such knowledge, it is possible to obtain a valid $\ast$bft‑notarization‑proof ${\mathsf{proof}}_P$. The notarization rule must require at least a two‑thirds absolute supermajority of voting units in $P$’s epoch to have been cast for $P$. It may also require other conditions.

A voting unit is cast non‑honestly for an epoch’s proposal iff:

• it is cast other than by the holder of the unit (due to key compromise or any flaw in the voting protocol, for example); or
• it is double‑cast (i.e. there are two ballots casting it for distinct proposals); or
• the holder of the unit following the conditions for honest voting in ${\Pi }_{\ast \mathrm{bft}}$, according to its view, should not have cast that vote.

Therefore, in an execution of Crosslink for which ${\Pi }_{\mathrm{bft}}$ has the one‑third bound on non‑honest voting property, for each epoch $e$ there will be at most one bft‑proposal‑valid proposal $P_e$, and at least one third of honestly cast voting units must have been cast for it. Let ${\mathcal{I}}_e$ be the (necessarily nonempty) set of nodes that cast these honest votes; then, $\mathsf{snapshot}(P_e){⪯}_{\mathrm{bc}}{\mathsf{ch}}_i^{t_{e,i}}{\lceil }_{\mathrm{bc}}^{\sigma }$ for all $i\in {\mathcal{I}}_e$ at the times $t_{e,i}$ of their votes in epoch $e$. (For simplicity, we assume that for each honest node $i$ there is only one time $t_{e,i}$ at which it obtains a successful check for the voting condition in epoch $e$, which it uses for any votes that it casts in that epoch.)

Let $B$ be any bft‑block for epoch $e$ such that $B{⪯}_{\mathrm{bft}}\text{bft-last-final}(C)$, where $C$ is some bft‑block‑valid block. Since $B{⪯}_{\mathrm{bft}}C$, $B$ is bft‑block‑valid. So by the argument above, $B$ commits to the only bft‑proposal‑valid proposal $P_e$ for epoch $e$, and $\mathsf{snapshot}(B)=\mathsf{snapshot}(P_e)$ was voted for in that epoch by a nonempty subset of honest nodes ${\mathcal{I}}_e$.

Let $H$ be any bc‑valid block. We have by definition: $$\begin{array}{rcl}\mathsf{fin}(H)& =& [\mathsf{snapshot}(B)\text{ for }B{⪯}_{\mathrm{bft}}\mathsf{LF}(H{\lceil }_{\mathrm{bc}}^{\sigma })]\\ & =& [\mathsf{snapshot}(B)\text{ for }B{⪯}_{\mathrm{bft}}\text{bft-last-final}(H{\lceil }_{\mathrm{bc}}^{\sigma }.context\_bft)]\end{array}$$ So, taking $C=H{\lceil }_{\mathrm{bc}}^{\sigma }.context\_bft$, each $\mathsf{snapshot}(B)$ for $B$ of epoch $e$ in the result of $\mathsf{fin}(H)$ satisfies $\mathsf{snapshot}(B){⪯}_{\mathrm{bc}}{\mathsf{ch}}_i^{t_{e,i}}{\lceil }_{\mathrm{bc}}^{\sigma }$ for all $i$ in some nonempty honest set of nodes ${\mathcal{I}}_e$.

For an execution of Crosslink in which ${\Pi }_{\mathrm{bc}}$ has the Prefix Consistency property at confirmation depth $\sigma$, for every epoch $e$, for every such $(i,t_{e,i})$, for every node $j$ that is honest at any time $t^{\prime }\ge t_{e,i}$, we have ${\mathsf{ch}}_i^{t_{e,i}}{\lceil }_{\mathrm{bc}}^{\sigma }{⪯}_{\mathrm{bc}}{\mathsf{ch}}_j^{t^{\prime }}$. Let $t_e=\min \{t_{e,i}:i\in {\mathcal{I}}_e\}$. Then, by transitivity of ${⪯}_{\mathrm{bc}}$:

A similar (weaker) statement holds if we replace $t^{\prime }\ge t_e$ with $t^{\prime }\ge t$, since the time of the first honest vote for $P$ necessarily precedes the time at which the signed $(P,{\mathsf{proof}}_P)$ is submitted as a bft‑block, which necessarily precedes $t$. (Whether or not the notarization proof depends on the first honest vote for $B$'s proposal $P_e$, it must depend on some honest vote for that proposal that was not made earlier than $t_e$.)

Furthermore, we have $$\begin{array}{rcl}\text{bda-ctx}(H,\mu )& =& \text{san-ctx}(\mathsf{fin}(H)||[H{\lceil }_{\mathrm{bc}}^{\mu }])\\ {\mathsf{LOG}}_{\mathrm{bda},i,\mu }^t& =& \text{context-txns}(\text{bda-ctx}({\mathsf{ch}}_i^t,\mu ))\end{array}$$

So in an execution of Crosslink where ${\Pi }_{\mathrm{bc}}$ has the Prefix Consistency property at confirmation depth $\mu$, if node $i$ is honest at time $t$ then $H{\lceil }_{\mathrm{bc}}^{\mu }$ is also, at any time $t^{\prime }\ge t$, in the bc‑best‑chain of every node $j$ that is honest at time $t^{\prime }$.

If an execution of ${\Pi }_{\mathrm{bc}}$ has the Prefix Consistency property at confirmation depth $\mu \le \sigma$, then it necessarily also has it at confirmation depth $\sigma$. Therefore we have:

Sketch: we also need the sequence of snapshots output from fin to only be extended in the view of any node. In that case we can infer that the node does not observe a rollback in LOG_bda.

Recall that in the proof of safety for ${\mathsf{LOG}}_{\mathrm{fin}}$, we showed that in an execution of Crosslink where ${\Pi }_{\mathrm{bft}}$ (or ${\Pi }_{\mathrm{origbft}}$) has Final Agreement, for all times $t$, $t^{\prime }$ and all nodes $i$, $j$ (potentially the same) such that $i$ is honest at time $t$ and $j$ is honest at time $t^{\prime }$, $\mathsf{fin}({\mathsf{ch}}_i^t)⪯⪰\mathsf{fin}({\mathsf{ch}}_j^{t^{\prime }})$.

What we want to show is that, under some conditions on executions, ...

Disadvantages of Crosslink

More invasive changes

Unlike Snap‑and‑Chat, Crosslink requires structural and consensus rule changes to both ${\Pi }_{\mathrm{bc}}$ and ${\Pi }_{\mathrm{bft}}$. On the other hand, several of those changes are arguably necessary to fix a showstopper bug in Snap‑and‑Chat (not being able to spend some finalized outputs).

Finalization latency

For a given choice of $\sigma$, the finalization latency is higher. The snapshot of the BFT chain used to obtain ${\mathsf{LOG}}_{\mathrm{fin},i,\mu }^t$ is obtained from the block at depth $\mu$ on node $i$'s best ${\Pi }_{\mathrm{bc}}$ chain, which will on average lead to a finalized view that is about $\mu +1+\sigma$ blocks back (in ${\Pi }_{\mathrm{bc}}$), rather than ${\sigma }_{\mathrm{sac}}$ blocks in Snap‑and‑Chat. This is essentially the cost of ensuring that safety is given by the stronger of the safety of ${\Pi }_{\mathrm{bc}}$ (at $\mu$ confirmations) and the safety of ${\Pi }_{\mathrm{bft}}$.

On the other hand, the relative increase in expected finalization latency is only $\frac{\mu +1+\sigma }{{\sigma }_{\mathrm{sac}}},$ i.e. at most slightly more than a factor of 2 for the case $\mu =\sigma ={\sigma }_{\mathrm{sac}}$.

More involved liveness argument

See the Liveness section above.

Every rule in Crosslink is individually necessary

Edit: some rules, e.g. the Increasing Score rule, only contribute heuristically to security in the analysis so far.