LibraBFT's Safety Proof for the 21st century

This is a re-write of LibraBFT (LBFT) safety proof in the report version 2 using techniques from Lamport (or at least trying). You can also read it in english.

Definition 1: BFT assumptions are that there are at least $2f+1$ honest validators if $f$ of them are malicious.

Definition 2: LBFT is safe if $\forall\ B, \widetilde{B} \in Blocks$, such that $B$ is committed at round $k$ and $\widetilde{B}$ is committed at round $\widetilde{k} \gt k$, then $B \longleftarrow \widetilde{B}$. LBFT is safe if for every block $B$ committed, and for every block $\widetilde{B}$ committed after, $\widetilde{B}$ must extend $B$.

Theorem: LBFT is safe under BFT assumptions.

Proof:

1.

Two blocks $B_0, B_0'$ are committed if there exists two chains:
  • $B_0 \longleftarrow QC_{B_0} \longleftarrow B_1 \longleftarrow QC_{B_1} \longleftarrow B_2 \longleftarrow QC_{B_2} $
  • $\widetilde{B_0} \longleftarrow QC_{\widetilde{B_0}} \longleftarrow \widetilde{B_1} \longleftarrow QC_{\widetilde{B_1}} \longleftarrow \widetilde{B_2} \longleftarrow QC_{\widetilde{B_2}} $
With both the chains having contiguous rounds, meaning that:
  • $round(B_2) = round(B_1) + 1 = round(B_0) + 2$
  • $round(\widetilde{B_2}) = round(\widetilde{B_1}) + 1 = round(\widetilde{B_0}) + 2$
We can assume $round(\widetilde{B_0}) \geq round(B_0)$ without loss of generality.

2.

It suffices to prove that $\forall\ B_0$ and $\widetilde{B_0}$ such that $round(\widetilde{B_0}) \geq round(B_0)$ and both blocks are committed, we have $B_0 \longleftarrow \widetilde{B_0}$. It suffices to prove that for all committed blocks $B_0$ and $\widetilde{B_0}$ (in this order), $\widetilde{B_0}$ expands $B_0$.

3.

Let $B$ a certified block, then the following statements are true:
  • if $round(B) = round(B_0) \implies B = B_0$
  • if $round(B) = round(B_1) \implies B = B_1$
  • if $round(B) = round(B_2) \implies B = B_2$
  • if the round of $B$ is the same as the round of $B_0$ then $B$ is $B_0$.
  • if the round of $B$ is the same as the round of $B_1$ then $B$ is $B_1$.
  • if the round of $B$ is the same as the round of $B_2$ then $B$ is $B_2$.

Proof:

3.1

Due to the BFT assumption, there can only be one quorum certificate per round.

3.2

Let $B_1$ and $B_2$ be two certified blocks such that $round(B_1) = round(B_2)$,
by statement 3.1 $QC_{B_1} = QC_{B_2}$ which in turns implies $B_1 = B_2$. Let $B_1$ and $B_2$ be two certified blocks at the same round,
by statement 3.1 they have the same quorum certificate and thus are the same blocks.

4.

Following statement 2, either $round(\widetilde{B_0}) \leq round(B_2)$, by statement 3 $\widetilde{B_0}$ is either $B_0, B_1,$ or $B_2$ and $B_0 \longleftarrow \widetilde{B_0}$,
or $round(\widetilde{B_0}) \gt round(B_2)$. Either $\widetilde{B_0}$ is $B_0, B_1,$ or $B_2$,
or $\widetilde{B_0}$ was proposed after $B_2$.

5.

Let block $\widetilde{B_i}$ such that $round(\widetilde{B_i}) \gt round(B_2)$, then $\widetilde{B_{i-1}} = previous\_round(\widetilde{B_i})$ and: If a block $\widetilde{B_i}$ was proposed after $B_2$, then $\widetilde{B_{i-1}}$ is the parent of $\widetilde{B_i}$ and:
  • either $round(\widetilde{B_{i-1}}) \gt round(B_2)$ as well,
  • or $round(B_0) \leq round(\widetilde{B_{i-1}}) \leq round(B_2)$, and by statement 3 $\widetilde{B_{i-1}}$ is either $B_0, B_1,$ or $B_2$ and $B_0 \longleftarrow \widetilde{B_{i-1}}$.
  • either $\widetilde{B_{i-1}}$ was proposed after $B_2$ as well,
  • or $\widetilde{B_{i-1}}$ was proposed in between $B_0$ and $B_2$, and by statement 3 $\widetilde{B_{i-1}}$ is either $B_0, B_1,$ or $B_2$.

Proof:

5.1.

It suffices to prove that if $round(\widetilde{B_i}) \gt round(B_2)$, then $round(\widetilde{B_{i-1}}) \geq round(B_0)$. It suffices to prove that if $\widetilde{B_i}$ was proposed after $B_2$,
then the parent of $\widetilde{B_i}$ ($\widetilde{B_{i-1}}$) was proposed after or at the round of $B_0$.

5.2.

Due to quorum certificates having at least $2f+1$ votes, the intersection of any two quorum certificates has at least one honest validator.

5.3.

By statement 5.2, There exists an honest validator $hv$ such that $hv \in QC_{B_2}$ and $hv \in QC_{\widetilde{B_i}}$. By statement 5.2, There exists an honest validator that has voted for both $B_2$ and $\widetilde{B_i}$.

5.4.

By the preferred round rules, after $hv$ observed $B_2$, $preferred\_round(hv) \geq round(B_0)$. By the preferred round rules, after Since the validator has observed the proposal for $B_2$, it updated its preferred round to the round of $B_0$.

5.5.

Since $round(\widetilde{B_i}) \gt round(B_2)$, by the voting rules $hv$ could only vote for $\widetilde{B_i}$ if
$previous\_round(\widetilde{B_i}) \geq preferred\_round(hv)$
$\Leftrightarrow round(\widetilde{B_{i-1}}) \geq round(B_0)$. Since the validator voted for $\widetilde{B_i}$ after $B_2$, by the voting rules the validator could only have voted for $\widetilde{B_i}$ if $\widetilde{B_i}$'s previous round (the round of $\widetilde{B_{i-1}}$) was greater or equal to the round of $B_0$.

6.

By induction, using statements 4 and 5, $B_0 \longleftarrow \widetilde{B_0}$.