owned this note
owned this note
Published
Linked with GitHub
# CBC Casper Explained (1/2)
> [CBC Casper Explained (2/2)](https://hackmd.io/y2PLjPwSQ3-RY1_Y9np4ow?view)
CBC(correct-by-construction) Capser는 consensus safety를 달성할 수 있는 프로토콜의 추상적인 구조입니다. 본 포스트에서는 [AbstractCBC](https://github.com/ethereum/research/blob/master/papers/cbc-consensus/AbstractCBC.pdf), [CasperTFG](https://github.com/ethereum/research/blob/master/papers/CasperTFG/CasperTFG.pdf) 두 페이퍼의 내용을 다룰 것입니다.
AbstractCBC는 "프로토콜 상태"와 "프로토콜 상태 전이"(protocol execution, morphism), "estimator"를 정의한 이후 estimate safety와 conosensus safety를 만족할 수 있는 프로토콜을 **수학적으로 증명**합니다. 추상적인 Casper CBC 구조를 상속하여 합의가 필요한 대상에 적용하기 때문에 CBC Casper family of protocol이라고 부릅니다.
CasperTFG(Casper the Friendly Ghost)는 binary consensus와 blockchain consensus(fork choice)를 consensus safe하도록 **스펙을 정의**하고 estimate safety를 만족할 수 있음을 보입니다. 또한 estimate safety를 올바르게 판별할 수 있는 **clique oracle**을 간략하게 소개합니다.
<!-- TODO: In a non-trivial consensus protocol, protocol-following nodes following completely independent executions of the protocol can decide on inconsistent values. Equivocating nodes can (by definition) exclusively show different nodes messages from independent protocol executions, and as a result, a large enough number of equivocation faults is fundamentally enough to cause consensus failure in any consensus protocol. -->
## Symbols & Terminology
- "consensus (value), ${C}$"
- binary consensus: {0, 1}
- blockchain consensus: fork choice
- "estimate (or proposition), $p$": "guesses" about the value of the consensus
- "logic of consensus with proposition, ${L_C}$":
- "set of propositions, $Props(L_C)$": map all possible consensus values to “True” or “False”
- $p \in Props(L_C), p: C \to \{True, False\}$
- "protocol state, $\sigma$"
- $\sigma \in \Sigma$
- "protocol execution (or morphism), $mo(\Sigma)$": transition from $\sigma_1$ to $\sigma_2$
- $\tau \in mo(\Sigma), \tau: \Sigma \to \Sigma$
- $\exists \tau \in mo(\Sigma), \sigma \xrightarrow[]{\tau} \sigma' \Leftrightarrow \sigma \to \sigma'$
- closed under composition: $\tau_1, \tau_2 \in mo({\Sigma}) \implies \tau_1 \circ \tau_2 \in mo({\Sigma})$
- "estimator, $\mathcal{E}$": maps protocol states to propositions
- $\mathcal{E}: \Sigma \to Props(L_C)$
- consistency: $\forall p \in Props(L_C) ,\forall \sigma \in \Sigma,$ if $\mathcal{E}(\sigma) \Rightarrow p$ then $\neg(\mathcal{E}(\sigma) \Rightarrow \neg p)$
- "estimate safety, $S(p, \sigma)$"
- $S(p, \sigma) \Leftrightarrow \forall \sigma': \sigma \to \sigma_1, \mathcal{E}(\sigma') \Rightarrow p$
- "common future state, $\sigma_1 \sim \sigma_2$"
- $\exists \sigma_3: \sigma_1 \to \sigma_3 \land \sigma_2 \to \sigma_3$
- "consensus safety, $\sigma_1 \sim \sigma_2 \implies \neg(S(p,\sigma_1) \land S(\neg{p},\sigma_2))$"
- "non-triviality": the protocol is able to choose between mutually exclusive values.
- $\exists p \in Props(L_C), \exists \sigma_0, \sigma_1, \sigma_2 \in \Sigma: (\sigma_0 \to \sigma_1 \land \sigma_0 \to \sigma_2) \land (S(p, \sigma_1) \land S(\neg p, \sigma_2))$
- "validator, $v$"
- $v \in V$
- "protocol message, $M$"
- $M = Props(L_C) \times V \times \mathcal{P}(\Sigma)$
- "justification of a message, $J(m)$": 메시지의 유효성을 확인하기 위한 프로토콜 상태
- "dependency of two messages, $m_1 \prec m_2$":
- 동치: $m_2$가 $m_1$이후에 생성되었다.
- "latest message from a validator: $L(v, M)$": 검증자가 가장 마지막에 보낸 메시지
- "weight": 검증자가 예치한 토큰의 수량
- "score": 블록의 점수
- "equivocation": 의존성을 가지지 않는 두 메시지 쌍의 관계. 정직한 노드는 equivocation하지 않는다.
- "weight of byzantine faults, faulty weight": byzantine 노드의 weight의 합
## 1. Estimate Safety Consensus Protocols
Estimate Safety Consensus Protocols는 $(C, L_C, \Sigma, \mathcal{E})$ 로 이루어져있습니다.
Binary consensus는 {0, 1}에 대한 합의를, blockchain consensus는 올바른 블록체인에 대한 합의를 결정합니다. 합의의 대상이 되는 것들을 **consensus value**($C$)라고 표현합니다.
**estimate**(혹은 proposition, $p$)은 consensus value가 올바른지 아닌지에 대한 명제입니다. 따라서 estimate는 $C$ 에서 {True, False}로 가는 map이라고 표현할 수 있습니다.
합의에 사용된 **logic**($L_C$)은 다르게 표현하자면 estimate의 집합($props(L_C)$)입니다. 어느 estimates를 이용하여 합의를 이루어 냈는가를 의미합니다.
**protocol states**($\Sigma$)는 합의를 이루는 노드들의 상태입니다. 노드가 합의를 결정하는 기준은 검증자들이 보낸 protocol message에 따라 결정됩니다. 따라서 a protocol state($\sigma, \sigma \in \Sigma$)은 protocol messages의 집합과 동일합니다.
마지막으로 **estimator**($\mathcal{E}$)는 protocol states에서 estimate로 가는 map입니다. 즉, $\sigma_1$에 있는 노드가 estimator를 이용하여 자신의 True인 proposition를 식별할 수 있으며 또한 $\sigma_2$에 있는 다른 노드의 estimate를 식별할 수 있습니다. 이러한 정보를 바탕으로 각 노드는 개별적으로 consensus safe가 보장되는 estimates를 추측할 수 있습니다.
estimator는 어느 $\sigma$에서 $p$가 True라면 $\neg p$에 대해서는 False라는 점에서 일관성을 가집니다. (if $\mathcal{E}(\sigma) \Rightarrow p$ then $\neg(\mathcal{E}(\sigma) \Rightarrow \neg p)$)
consensus value $C$는 특징되지 않았으며, estimator 또한 단순한 a map from state to proposition 이기 때문에 추상적으로 정의됩니다. 해당 페이퍼 제목에 abstract가 들어가는 이유 또한 그 때문입니다. binary consensus, blockchain consensus는 그에 맞는 estimator를 정의하고 있습니다.
반면 protocol state는 검증자들의 protocol message의 집합으로 정의됩니다. protocol message는 consensus values, 검증자, 그리고 protocol states의 tuple입니다. ($M := C \times V \times \Sigma$) 이에 대한 자세한 설명은 [2. Casper the Friendly Binary Consensus](#2-Casper-the-Friendly-Binary-Consensus)에서 다루겠습니다.
### 1.1 Estimate Safety ($S(p, \sigma)$)
**Estimate safety**는 "proposition $p$가 protocol state $\sigma$에서 safe하다는 의미"이며, $S(p, \sigma)$로 나타냅니다. $\sigma$의 모든 future state $\sigma'$에 대해 estimator는 동일한 $p$를 반환해야 합니다.
$$
S(p, \sigma) \Leftrightarrow \forall \sigma': \sigma \to \sigma_1, \mathcal{E}(\sigma') \Rightarrow p
$$
모든 $\tau \in mo(\Sigma), \sigma \xrightarrow[]{\tau} \sigma'$ 에 대하여 위 조건을 만족해야 하는데, 이는 $\sigma \xrightarrow[]{\tau_1} \sigma$ 인 $\tau_1$(identity-transition)에 대해서도 성립해야 합니다.
또한 $\sigma_1 \xrightarrow[]{\tau_{12}} \sigma_2 \xrightarrow[]{\tau_{23}} \sigma_3$일 때, $\tau_{13} \in mo(\Sigma): \tau_{13} = \tau_{12} \circ \tau_{23}$인 $\tau_{13}$도 존재하기 때문에, $\sigma_1$의 future state는 $\{\sigma_2,
\sigma_3\}$ 가 됩니다. ($\because \sigma_1 \xrightarrow[]{\tau_{13}} \sigma_3$).
노드들은 오직 proposition p가 estimate safety할 경우에만 의사결정을 합니다.
---
### 1.2 Consensus Safety ($\sigma_1 \sim \sigma_2 \implies \neg(S(p,\sigma_1) \land S(\neg{p},\sigma_2))$)
**Consensus safety**는 각 노드들이 estimate safety를 가지는 common future protocol state를 개별적으로 판단할 수 있음을 의미합니다. 즉, 두 노드가 각각 $\sigma_1, \sigma_2$에 있을 때 "각 노드가 개별적으로 내린 결정들은 서로 일관성이 존재"하기 때문에 safety가 보장됩니다.
**common future protocol state**는 다음과 같이 정의됩니다.
![](https://i.imgur.com/dQc0I2z.png)
Consensus safety를 증명하기 위한 3개의 보조정리를 먼저 살펴봅시다.
- Lemma 1: Forwards Safety
$$
\forall \sigma':\sigma \to \sigma',\hspace{1.5mm} S(p,\sigma) \implies S(p,\sigma')
$$
![](https://i.imgur.com/vs7GtQF.png)
이 보조정리는 estimate safety가 모든 future state를 포함한다는 사실로부터 증명할 수 있습니다. "$\sigma$의 모든 future state $\sigma'$"에 대해 $\mathcal{E}(\sigma') = p$ 이기 때문에, $\sigma'$의 future state($\sigma''$) 또한 $\mathcal{E}(\sigma'') = p$라는 사실이 "estimate safety at $\sigma$"에 내포되어 있습니다.
- Lemma 2: Current Consistency
$$
S(p,\sigma) \implies \neg{S(\neg{p},\sigma)}.
$$
![](https://i.imgur.com/KZ6MtTb.png)
이 보조정리는 상반되는 두 propositions ($p, \neg p$)가 동시에 safe할 수 없다는 의미를 가집니다. estimator의 일관성 (if $\mathcal{E}(\sigma) \Rightarrow p$ then $\neg(\mathcal{E}(\sigma) \Rightarrow \neg p)$)을 이용하여 증명할 수 있습니다.
- Lemma 3: Backwards Consistency
$$
\forall \sigma:\sigma \to \sigma',\hspace{1.5mm} S(p,\sigma') \implies \neg{S(\neg{p},\sigma)}
$$
![](https://i.imgur.com/vhyW7IM.png)
이 보조정리는 protocol state $\sigma'$에서 safe한 estimate $p$의 반대($\neg p$)가 previous state $\sigma$에서 safe하지 않음을 의미합니다.
3개의 보조정리는 아래의 다이어그램으로 표현될 수 있습니다. 한가지 흥미로운 사실은, Lemma 2에 의해 $\neg S(\neg p, \sigma_2) \implies S(p, \sigma_2)$ 라는 점 입니다. 즉, 두 노드가 각각 $\sigma_1, \sigma_2$에 있고, common future state를 가지고, 1번 노드가 $S(p, \sigma)$을 확인한다면, 1번 노드는 2번 노드 또한 $S(p, \sigma_2)$ 라는걸 확인할 수 있습니다. ($\because S(p, \sigma_1) \xrightarrow[]{\text{Lemma 1} \circ\text{Lemma 3} \circ\text{Lemma 2}} S(p, \sigma_2)$)
![](https://i.imgur.com/M5CknrP.png)
- Theoreom 1: Consensus Safety
$$
\sigma_1 \sim \sigma_2 \implies \neg(S(p,\sigma_1) \land S(\neg{p},\sigma_2))
$$
![](https://i.imgur.com/7tsHYEP.png)
Consensus safety 정리는 common future state를 가지는 두 protocol states($\sigma_1, \sigma_2$)는 1) $\neg S(p, \sigma_1)$ 혹은 2) $\neg S(\neg p, \sigma_2)$ 임을 보장합니다.
- 1번 경우에는 estimate safety가 없기 때문에 $p$에 대해 의사결정을 하지 않을 것입니다.
- 2번 경우에는 Lemma 2에 의해 $\neg S(\neg p, \sigma_2) \Leftrightarrow S(p, \sigma_2)$ 와 동일한 의미를 가집니다.
위 증명의 (4)번 주장이 지금까지 논의한 "합의의 일관성"을 가장 명확히 보여줍니다. 이는 별도의 Lemma 4로 따로 정의합니다.
- Lemma 4: Distributed Consistency
$$
\sigma_1 \sim \sigma_2 \implies \hspace{2mm} (S(p,\sigma_1) \implies \neg{S(\neg{p},\sigma_2)})
$$
이 보조정리는 Lemma 1, Lemma 3로 부터 유도되었으며, "노드가 safe estimate를 기반으로 내린 개별적인 결정(decision)는 다른 노드가 내린 결정와 일관성을 가지는 것"을 의미합니다. 즉, 다른 protocol state에 있는 다른 노드와 common future state $\sigma_3$를 가지기만 하면, 다른 노드 또한 $\sigma_3$에 대해 estimate safety를 가질 것이고, 이는 해당 노드가 consensys safety가 보장된 의사결정을 할 수 있음을 보장합니다.
지금까지는 common future state를 기반으로 내린 결정의 safety를 논의했습니다. 하지만 실제 상황에선 common future state가 존재하지 않는 경우가 더 많을 것입니다. 가령 blockchain fork가 발생하거나 byzantin 노드가 내린 결정에 따르지 않는 상황들일 것입니다. 이런 특성을 **non-triviality**라 부르며, 상호 배재하는 두 protocol states에 대해서도 safety를 보장할 수 있어야 합니다.
non-triviality는 다음과 같이 정의됩니다.
![](https://i.imgur.com/OFfJGIw.png)
$$
\exists p \in Props(L_C), \exists \sigma_0, \sigma_1, \sigma_2 \in \Sigma: (\sigma_0 \to \sigma_1 \land \sigma_0 \to \sigma_2) \land (S(p, \sigma_1) \land S(\neg p, \sigma_2))
$$
- Lemma 5: Maintaining a shared future is non-trivial
$$
\exists \sigma_1, \sigma_2 \hspace{1mm}.\hspace{1mm} \sigma_1 \nsim \sigma_2 \\
\text{Where } \sigma_1 \nsim \sigma_2 \text{ denotes } \neg{(\sigma_1 \sim \sigma_2)}
$$
![](https://i.imgur.com/1cmuZof.png)
이 보조정리는 non-triviality 때문에 common future state가 항상 존재하는것은 아님($\exists \sigma_1, \sigma_2 \in \Sigma: \sigma_1 \nsim \sigma_2$)을 의미합니다.
위 증명의 3번이 consensus safety theorem의 대우입니다. 이는 consensus failure를 의미하며, non-triviality가 발생할 수 있는 조건을 보여줍니다.
- Lemma 6: Consensus Failure
$$
S(p,\sigma_1) \land S(\neg{p},\sigma_2) \implies \sigma_1 \nsim \sigma_2
$$
![](https://i.imgur.com/fINWoK9.png)
아래 그림은 non-triviality로 인해 common futre state를 가지지 않는 상황을 보여줍니다. 두 개의 분기가 존재하며, 각 분기별로 두 개의 future states로 나눠지는 모습입니다.
<!-- ![](https://i.imgur.com/mzAWyj7.png) -->
![](https://i.imgur.com/EOkuOCN.png)
<!-- TODO: σ1 and σ2 have common a future only as long as there are less than t Byzantine faults in σ1 ∪ σ2. This allows for states without shared protocol futures (allowing non-triviality) but still allows for consensus safety from our previous result (although now only as long as there are less than t Byzantine faults). -->
지금까지 Estimate safe consensus protocol을 살펴보았습니다. 위 내용을 다시한번 정리하면,
1. $\sigma_1$에 있는 노드 A는 $p$에 대해 $S(p, \sigma_1)$인지 알 수 있습니다. 또한 $\sigma_2$에 있는 다른 노드 B와 common future state($\sigma_3$)를 가진다는 것을 확인한다면, A는 개별적으로 $\sigma_3$에 대해 합의를 결정할 수 있습니다. 이는 B또한 마찬가지로 $S(p, \sigma_1)$을 확인한다면 개별적으로 $\sigma_3$에 대해 합의를 결정할 수 있습니다. A와 B의 개별적인 의사결정은 (byzantine fault하지 않다는 가정하에) consensus safety theorem에 의해 일관성이 보장됩니다.
2. 또한 common future state가 존재하지 않는 non-trivial한 상황도 발생할 수 있으며 (Lemma 6), 이 경우 합의는 진행될 수 없을 것입니다.
프로토콜이 "어떻게 byzantine fault tolerant할 수 있는지"는 binary consensus와 blockchain consensus 예시들을 살펴보며 논하겠습니다.
## 2. Casper the Friendly Binary Consensus
이제 consensus safety proof를 위한 protocol state, estimator 및 기타 개념들을 Binary Consensus를 예제로 순차적으로 살펴봅시다.
- **protocol states**는 `t`이하의 byzantine fault를 보이는 protocol message의 집합입니다. -- as sets of messages that exhibit up to t Byzantine faults --
- **protocol messages**($\mathcal{M}$)는 (estimate, sender, justification)으로 이루어집니다. **estimate**($p$)는 $\{0, 1\}$ 중 하나이고, **sender**는 validator($v \in V$) 입니다. 그리고 **justification**($J(\mathcal{M})$)은 protocol messages입니다. protocol message의 'estimator를 justification에 적용한 결과가 estimate와 동일' 할 때 유효합니다. 즉 메시지 $m \in \mathcal{M}: m = (p, v, j)$ 은 $\mathcal{E}(j) = p$ 일 때 유효합니다.
- protocol message의 justification은 특정 검증자의 protocol state를 확인하는 용도로 사용됩니다. 따라서 protocol message를 받은 노드는 해당 검증자의 protocol state를 justification으로 파악한 이후 common future state를 찾을 수 있습니다. 이는 곧 consensus safety 정리를 적용할 수 있는지 각 노드가 개별적으로 파악 가능하다는 의미이기도 합니다.
- protocol message의 정확한 정의는 다음과 같습니다.
![](https://i.imgur.com/PYho6KN.png)
$\mathcal{P}$는 [멱급수(powerset)](https://en.wikipedia.org/wiki/Power_set)를 의미하며, 모든 부분집합들의 집합입니다. 위 정의를 통해 protocol message는 $Props(L_C) \times V \times \mathcal{P}(\Sigma)$ 공간에 있음을 확인할 수 있습니다.
- estimator($\mathcal{E}$)는 protocol messages를 0, 1, 혹은 $\emptyset$ 중 하나의 값으로 보내는 map입니다.
$$
\mathcal{E}:\mathcal{P}(\mathcal{M}) \to \{0, 1\} \cup \{\emptyset\}
$$
protocol message $\mathcal{M}$의 estimate, validator, justification를 반환하는 helper function $E, V, J$을 다음과 같이 정의합니다.
$$
\exists m \in \mathcal{M}, m = (e, v, j): \\
E(m) = e \\
V(m) = v \\
J(m) = j
$$
따라서 protocol message은 $\mathcal{E}(J(m)) = \emptyset$ 이거나 $\mathcal{E}(J(m)) = E(m)$ 일 때 유효합니다.
- 이제 메시지 $m_2$가 $m_1$에 **dependency**를 가지는 것을 $m_1 \prec m_2$로 표기합니다.
$$
m_1 \prec m_2 \iff m_1 = m_2 \text{ or } \exists m' \in J(m_2) \hspace{1mm} . \hspace{1mm} m_1 \prec m'
$$
(𝑚1≺𝑚2⟺𝑚1=𝑚2 or ∃𝑚′∈𝐽(𝑚2). 𝑚1≺𝑚′)
Justification이 protocol message의 protocol state를 의미하기 때문에, dependency를 통해 $\exists \tau \in mo(\Sigma): J(m_1) \xrightarrow[]{\tau} J(m_2)$를 확인할 수 있습니다.
마찬가지로 validator $v$가 보낸 메시지 $m$에서 dependency를 반환하는 helper function D은 다음과같이 정의될 수 있습니다.
$$
D(m) = \{m\}\cup \bigcup_{m' \in J(m)} D(m')
$$
두 메시지의 선후관계를 dependency를 통해 파악할 수 있습니다. 따라서 이제 검증자의 **latest message**를 다음과같이 정의할 수 있습니다.
$$
m \in L(v, M) \iff \nexists m' \in D(M) : V(m') = v \text{ and } m' \succ m
$$
즉 latest message $m$ from validator $v$는 "$v$가 $m$에 의존하는 다른 메시지를 보내지 않음", 혹은 "$m$ 이후에 다른 메시지를 보내지 않음"으로 말할 수 있습니다.
- estimator를 정의하기 앞서 우선 validator의 **weight** $W$과 메시지의 집합 $M$에서 estimate의 **score를** 다음과 같이 정의합니다.
$$
W:\mathcal{V} \to \mathbb{R}_+ \\
\text{Score}(e, M) = \sum_{\substack{v \in \mathcal{V} \\ : m \in L(v,M) \\ \text{with } E(m) = e}} W(v)
$$
- 드디어 메시지 집합 $M$에 대하여 binary consensus estimator를 highest score를 가진 estimate를 반환하도록 다음과같이 정의할 수 있습니다. 만일 highest score가 유일하지 않다면, $\emptyset$을 반환합니다.
\begin{align}
\mathcal{E}(M) &= 0 &\text{ if } \text{Score}(0, M) > \text{Score}(1, M), \\
\mathcal{E}(M) &= 1 &\text{ if } \text{Score}(1, M) > \text{Score}(0, M), \\
\mathcal{E}(M) &= \emptyset &\text{ if } \text{Score}(1, M) = \text{Score}(0, M)
\end{align}
지금까지 protocol state, protocol message, estimator를 정의했습니다. 이제 byzantine fault `t`를 계산하는 방법을 정의하고, `t` 이하의 protocol message에 대해서 binary consensus가 estimate safety를 가지는지, consensus safety 정리를 만족 하는지 살펴봅시다.
- 한 검증자가 생성한 두 메시지가 dependency를 가지지 않을 때, 해당 메시지 쌍을 **equivocation**하다고 정의합니다. equivocation인지 아닌지 판별하는 함수 $Eq$는 다음과 같습니다.
$$
Eq(m_1, m_2) \iff V(m_1) = V(m_2) \text{ and } m_1 \nsucc m_2 \text{ and } m_1 \nprec m_2
$$
(𝐸𝑞(𝑚1,𝑚2)⟺𝑉(𝑚1)=𝑉(𝑚2) and 𝑚1⊁𝑚2 and 𝑚1⊀𝑚2)
non-triviality 관점에서 생각해보면, common future state를 가지지 않는 $\sigma_1, \sigma_2$를 justification으로 사용하는 protocol message $m_1, m_2$는 항상 equivocation일 수 밖에 없습니다. equivocation은 합의할 수 없는 두 protocol states를 판별하고 최종적으로 byzantine validator의 메시지를 검열하는데 사용할 수 있습니다.
- equivocate한 검증자 $v$를 byzantine하다고 부르거나 집합 $M$에서 byantine fault를 보였다고 합니다. 따라서 메시지 집합 $M$에서 검증자 $v$가 byzantine faulty한지 반환하는 함수$B(v, M)$를 다음과같이 정의합니다.
$$
B(v,M) \iff \exists m_1, m_2 \in D(M) : v = V(m_1) \land Eq(m_1, m_2)
$$
또한 메시지 집합 $M$에서 byzantine nodes를 반환하는$B(M)$은 다음과 같습니다.
$$
B(M) = \{v \in \mathcal{V}: B(v,M)\}
$$
마지막으로 메시지 집합 $M$에서 weight of byzantine faults를 계산하는 함수 faulty weights $F(M)$를 다음과 같이 정의할 수 있습니다.
$$
F(M) = \sum_{v \in B(M)} W(v)
$$
- 이제 **protocol state**를 `t` 이하의 byzantine faults를 포함하도록 재정의합니다. $\Sigma_t$로 표기하며, 메시지의 집합들이기 때문에 $\Sigma_t \subset \mathcal{P}(\mathcal{M})$입니다. subset관계인 이유는 $\sigma$는 protocol message의 집합이고, $\Sigma$는 $\sigma$의 집합이기 때문입니다.
$$
\Sigma_t = \left\{\sigma \subseteq \mathcal{M}: F(\sigma) \leq t \right\}
$$
- **protocol executions**은 $\sigma, \sigma' \in \Sigma_t$ 간의 transition입니다. $\sigma, \sigma'$는 각각 protocol message의 집합이기 때문에, protocol execution은 $\sigma, \sigma'$가 improper subset 관계를 가진다와 동치입니다.
$$
\forall \sigma, \sigma' \in \Sigma_t \hspace{3mm} : \sigma \to \sigma' \iff \sigma \subseteq \sigma'
$$
앞서 논의했던 "protocol execution은 composition에 대해 닫혀있다"는 주장도 improper subset 관게 또한 composition에 대해 닫혀있기 때문에 동일하게 성립합니다.
- 온전히 정의된 protocol state, protocol execution, estimator를 이용하면 abstract 하게 정의했던 estimate safety가 binary consensus에도 동일하게 적용될 수 있습니다. 따라서 **binary estimate safety**를 다음과 같이 정의합니다.
$$
S_t(e, \sigma) \iff \forall \sigma' \in \Sigma_t: \sigma \to \sigma',\hspace{1.5mm} e = \mathcal{E}(\sigma')
$$
Binary estimate safety는 앞서 논의한 consensus safety proof를 만족하기 때문에, byzantine fault가 `t` 이하의 safe estimate에 대해 내린 노드의 개별적인 결정들은 consensus safe합니다.
## 3. Casper the Friendly GHOST
Casper the Friendly GHOST는 fork choice에 consensus safety를 부여하는 프로토콜입니다.
이제 binary consensus에서 사용한 개념들을 이용해 blockchain consensus를 정의해봅시다. protocol state, execution, estimate를 제외한 나머지 개념들은 binary consensus와 동일하게 사용합니다.
- 프로토콜 메시지는 새로운 블록을 제안하는 것입니다. 마찬가지로 3개의 요소(estimate, sender, justificatoin)를 가지는데, estimate는 **부모 블록**이고 justification은 해당 메시지의 유효성을 검증하는데 등 사용되는 **protocol state** 입니다. 메시지(새로운 블록)는 부모 블록(estimate)이 블록체인(justification)의 head일 때 유효합니다.
protocol messages $\mathcal{M}$은 다음과같이 정의됩니다.
$$
\begin{equation*}
\begin{split}
&\text{Genesis Block} = \{\emptyset\}\\
&\mathcal{M}_0 = \{\text{Genesis Block}\} \times \mathcal{V} \times \{\text{Genesis Block}\}\\
&\mathcal{M}_n = \bigcup_{i=0}^{n-1} \mathcal{M}_i \times \mathcal{V} \times \mathcal{P}(\bigcup_{i=0}^{n-1} \mathcal{M}_i)\\
&\mathcal{M} = \{\text{Genesis Block}\} \cup \lim_{n \to \infty} \bigcup_{i=0}^{n} \mathcal{M}_i
\end{split}
\end{equation*}
$$
- fork choice rule을 정의하기 앞서 두 블록의 포함관계를 먼저 정의해야 합니다. 블록 $b_1$이 블록 $b_2$의 블록체인에 포함되었을 때 $b_1 \downarrow b_2$라고 표기합니다. 이는 앞서 봤던 $\sigma' \subseteq \sigma'$의 improper subset 관계와 동일한 정의입니다.
$$
b_1 \downarrow b_2 \iff b_1 = b_2 \text{ or } b_1 \downarrow E(b_2)
$$
따라서 블록 $b$의 score 정의또한 변경된 포함관계를 이용하여 약간 달라지게 됩니다.
$$
\text{Score}(b, M) = \sum_{\substack{v \in \mathcal{V} : \\ m \in L(v,M) \\ b \downarrow E(m)}} W(v)
$$
그리고 마지막으로 메시지 집합 $M$에 대하여 블록 $b$의 "자식 블록"들을 반환하는 helper function $C(b, M)$을 다음과같이 정의합니다.
$$
C(b,M) = \{b' \in M : E(b') = b\}
$$
드디어 blockchain consensus의 estimator를 정의할 수 있는 모든 개념들이 정리되었습니다. 다시한번 말하자면, 해당 estimator는 fork choice rule을 구현합니다.
![](https://i.imgur.com/Qo6IOwX.png)
이제 Consensus safety 정리를 적용하기 위하여 **blockchain estimate safety**를 다음과같이 정의합니다.
$$
S_t(b, \sigma) \iff \forall \sigma' \in \Sigma_t: \sigma \to \sigma',\hspace{1.5mm} b \downarrow \mathcal{E}(\sigma')
$$
Blockchain estimate safety는 앞서 논의한 consensus safety proof를 만족하기 때문에, byzantine fault가 `t` 이하의 safe estimate에 대해 내린 노드의 개별적인 결정들은 consensus safe합니다.
## 4. Simple Safe Oracle
estimate safety는 모든 future state에 대한 논의였습니다. 하지만 노드가 내리는 결정은 유한한 시간 안에서 내려져야 합니다. Estimate safety를 판별하는 candidate estimate에 대한 safety가 올바른지 모델링하기 위하여 "ideal [adversary](https://en.wikipedia.org/wiki/Adversary_model)"를 생각해봅시다. ideal adversary는 $\sigma, \sigma' \in \Sigma_t: \sigma \to \sigma', \mathcal{E}(\sigma') \neq \mathcal{E}(\sigma)$인 $\sigma'$을 검색하여 공격합니다. 즉, adversary는 estimate safety가 존재하지 않는 future state를 발견할 수 있습니다. 그리고 "ideal safety [oracle](https://en.wikipedia.org/wiki/Oracle_machine)"은 ideal adversary가 공격에 실패할 경우 True를 반환합니다.
만약 ideal oracle이 공격에 실패하는 "특정 상황"을 발견할 수 있다면, safety oracle을 구성하여 estimate safety가 보장되는 estimates를 선별할 수 있습니다. (물론 실제 구현으로 들어가면 완전히 ideal하기는 힘듭니다.)
앞서 말한 "특정 상황"을 일반화 해 봅시다. 먼저 두 estimate $e, e'$간의 **agreement**를 $e \equiv e'$로 표기합니다. 이는 binary consensus의 $e = e'$, blockchain consensus의 $e \downarrow e'$에 대응합니다. **disagreement**는 $e \not\equiv e'$로 표기합니다.
- "protocol message의 집합 $M$에서 validator $v_i$는 validator $v_j$가 estimate $e$에 대해 동의(agreeing)함을 확인함"을 다음으로 정의합니다.
- $v_i$ has exactly one latest message in $M$ (we are denoting this message as $L(v_i, M)$)
- $v_j$ has exactly one latest message in the justification of $v_i$'s latest message, $J(L(v_i, M))$ (which we denote as $L(v_j, J(L(v_i, M)))$
- This message's estimate agrees with $e$, i.e. $E(L(v_j, J(L(v_i, M)))) \equiv e$
이는 다음과 동일한 의미를 가집니다.
$$
v_i \xrightarrow[\text{$M$}]{\text{$\equiv, e$}} v_j \iff E(L(v_j, J(L(v_i, M)))) \equiv e
$$
agreement에 대한 정의는 명확합니다. 두 검증자 모두 유일한 latest message $m_i = L(v_i, M), m_j = L(v_j, J(m_i))$를 보낸 것으로, 두 메시지 $m_i, m_j$의 justification은 포함관계에 있습니다. $v_i$가 알고 있는 protocol state에 대한 protocol message이기 때문에 "$v_i$는 $v_j$가 estimate $e$에 동의하는 것을 확인할 수 있다"고 말할 수 있습니다.
- 반대로 "protocol message의 집합 $M$에서 validator $v_j$는 validator $v_j$가 estimate $e$에 대해 반대(disagreeing)함을 확인함"을 다음으로 정의합니다.
- $v_i$ has exactly one latest message in $M$, $L(v_i, M)$
- $v_j$ has exactly one latest message in the justification of $v_i$'s latest message, $J(L(v_i, M))$ (which we denote as $L(v_j, J(L(v_i, M))))$
- $v_j$ has a message $m \in M$ that is undelivered to $v_i$ : $m \succ L(v_j, J(L(v_i, M))))$
- And this $m$ disagrees with $e$, $E(m) \not\equiv e$
이는 다음과 동일한 의미를 가집니다.
$$
v_i \xrightarrow[\text{$M$}]{\text{$\not\equiv, e$}} v_j \iff \exists m \in M : V(m) = v_j \land m \succ L(v_j, J(L(v_i, M))) \land E(m) \not\equiv e
$$
disagreement의 경우엔 $v_j$가 $v_i$에게 전달한 latest message $m_j$이외에 전달하지 않은 메시지 $m$이 하나 더 존재합니다. $m$은 $m_j$에 의존($m_j \prec m$)하며 $E(m) \not\equiv e$입니다.
두 검증자 $v_i, v_j$가 서로 estiamte $e$에 대해 동의함을 확인했다는 것은, 두 검증자가 보낸 latest message $m_i, m_j$는 $E(m_i) = E(m_j) = e, J(m_i) = J(m_j)$일 것입니다. 하지만 한가지 주목할 점은 정직한 노드들(non-equivocating nodes)은 특정 프로토콜 상태($M$)에서 서로 estimate e에 대해 동의하는지, 반대하는지 확인할 수 있습니다. 이러한 노드의 집합을 $e$-clique in $M$ 이라고 부릅니다.
### 4.1 Clique Oracle
$e$-clique를 이용하여 estimate safety를 판별하는 oracle을 clique oracle이라 부릅니다. Clique oracle이 항상 올바른 판단을 내릴 수 있는지 간략히 검증하기 위하여 $t=0$일 때의 protocol state $\Sigma_t$를 생각해봅시다. $t=0$ 이기 때문에 equivocating node가 없는 상황입니다. 이 때 $e$-clique에 속한 노드들의 총 weight을 $W_{clique} = \sum_{v \in Clique(e, M)} W(v)$에 대하여, 검증자들이 각자 계산한 $Score(e, M) = W_{clique}$가 있을 것이고, 새로운 메시지가 $e$-clique 내부 혹은 외부에서 생성될 수 있습니다.
이 때 1) $e$-clique 내부의 메시지들은 score를 감소시킬 수 없습니다. 그러한 메시지는 equivocating 하기 때문에 $t=0$ 이라는 가정에서 존재하지 않을 것입니다. $t > 0$일 경우에도 동일합니다. 또한 2) $e$-clique에 속한 노드의 weigts의 합($W_{clique}$)이 모든 검증자의 weights의 합($W_{total}$)의 1/2보다 클 때, $e$-clique 외부의 메시지들은 $e$와 대립하는 $e'$가 $W_{clique}$보다 높은 score를 가지게 할 수 없습니다.
$Score(e', M)$은 최대 $W_{total} - W_{clique}$일 것입니다. 따라서 $W_{clique} \gt W_{total} / 2$인 한, $Score(e', M) < Score(e, M)$ 입니다. $t > 0$일 때는, $W_{clique} - W_{total}/2 > t - F(M)$ 인 한, $e$-clique im $M$는 언제나 $e$에 대해 estimate safety를 판별할 수 있습니다.
(위에서 대룬 내용들은 다음 포스트에서 보다 자세하게 증명합니다.)
Clique oracle은 아래 알고리즘을 이용해 구현할 수 있습니다.
<!-- ![](https://i.imgur.com/GeZC0KZ.png) -->
![](https://i.imgur.com/0DX38Or.png)
### 4.2 Subjective Fault Tolerance Thresholds
Clique oracle이 지정한 fault tolerance $t$는 각 노드별로 다르게 지정할 수 있습니다. 두 노드의 fault tolerances $t_1 < t_2$에 대해 각 노드는 $\Sigma_{t1}, \Sigma_{t2}$의 상태를 관리합니다. $t_1 < t_2$이기 때문에 $\Sigma_{t1} \subset \Sigma_{t2}$입니다. 모든 $\sigma_1 \in \Sigma_{t1}, \sigma_2 \in \Sigma_{t2}$의 common future state $\sigma_3$은 $\sigma_3 \in \Sigma_{t1} \cup \Sigma_{t2}$에 있지만, $\sigma_1 \to \sigma_3$이기 위해선 $\sigma_3 \in \Sigma_{t1}$ 이어야 합니다. 하지만 오직 $F(\sigma_1 \cup \sigma_2) \leq t_1$일 때, $\sigma_2 \in \Sigma_{t1}$이고 $\sigma_3 \in \Sigma_{t1}$으로 두 protocol state $\sigma_1, \sigma_2$가 common future state를 공유하게 됩니다.
![](https://i.imgur.com/tOXm2gT.png)
Tolerance threshold $t$를 프로토콜이 아닌 개별 노드들이 관리한다는 점에서 공격자가 target threshold를 정확히 알 수 없는 장점이 있습니다. clique에 속한 노드가 전체 노드의 1/2 이상일 때 clique oracle에 의해 보장되는 estiamte safety는 각 정직한 노드들이 설정한 tolerance thresold $t$의 최소값에 의존합니다. 따라서 정직한 노드 대부분이 $t$를 낮게 설정할 경우 clique oracle의 safety는 더욱 높아질 수 있습니다. 정직한 노드들이 $t$를 0에 가깝게 설정하면, 전체 프로토콜의 성능을 희생하고 safety를 높일 수 있습니다.
## 5. 결론
AbstractCBC와 CasperTFG를 통해 estimate safety protocol을 수학적으로 정의하고, 이를 binary consensus와 blockchain consensus에 적용하는 방법을 살펴보았습니다. CBC Casper는 두 노드가 common future state를 가지는 한, 한 노드가 내린 의사결정은 다른 노드 또한 동일하게 내릴 수 있음을 consensus safety 정리를 통해 증명하였습니다. 이를 두고 Vlad Zamfir는 **전통적인 PBFT와 같은 합의 알고리즘과 질적으로 다르다**는 평가를 했습니다.
두 페이퍼에서 생략한 safety oracle, liveness, synchrony assumption, 다자간의 consensus safety를 다음 포스트에서 다루도록 하겠습니다.
---
## References
- https://github.com/ethereum/research/blob/master/papers/cbc-consensus/AbstractCBC.pdf
- https://github.com/ethereum/research/blob/master/papers/CasperTFG/CasperTFG.pdf
###### tags: `cbc` `casper` `cbc capser` `explained`