[이더리움2.0 깊이보기 시리즈]CBC Casper Explained (2/2)[5편]

Published in

Tokamak Network

37 min readDec 24, 2019

Carl Park (4000D)

이더리움2.0 깊이보기 시리즈는 개발이 진행되고 있는 이더리움2.0에 관한 스펙과 작동원리에 대해서 이해의 저변을 넓히고자 하는 목적으로 온더에서 기획되었습니다. 연재는 다음 순서로 이어집니다.

[1편] — ETH 2.0 Explained: Phase 0
[2편] — Cross Shard Communication -1- 비동기 커뮤니케이션
[3편] — Cross Shard Communication -2- 동기 커뮤니케이션
[4편] — CBC casper explained (1/2)
[5편] — CBC casper explained (2/2)
[6편] — ETH 2.0 Explained: Phase 1
[7편] — 스태이트리스 클라이언트(Stateless Client)
[8편] — ETH 2.0 Explained: Phase 2
[9편] — Execution Environment

LaTeX가 올바르게 표기되는 이 문서를 보시기 추천드립니다.

1. Minimal CBC Casper

이전 포스트에서 proposition을 기반으로 두 검증자간의 consensus safety를 다뤘습니다. Minimal CBC Casper에서 다룰 내용은 다음과 같습니다.

이전 포스트에서 다뤘던 “일관성”의 증명과 함께 노드의 protocol state를 기반으로 consensus value에 safety를 보장받을 수 있는 방법
두 검증자간의 consensus safety를 다자간의 consensus safety로 확장
Latest Message Driven GHOST의 정의

정리의 증명들만 다루며, 보조정리의 증명은 해당 페이퍼를 참고하시기 바랍니다.

1.1 Consensus Safety

1.1.1 Common Notations

Minimal CBC Casper 페이퍼에서 사용하는 정의 / 보조정리 / 정리의 목록은 여기서 확인하실 수 있습니다. 적어도 Prerequisite Notation은 사전에 한번 읽어보는 것을 강력히 권장드립니다.

두 protocol state 𝜎1,𝜎2σ1,σ2간의 transition은 포함관계(improper subset)에 있습니다.
(𝜎1→𝜎2:⇔𝜎1⊆𝜎2σ1→σ2:⇔σ1⊆σ2)
Protocol message 𝑚m의 estimate, sender, justification을 반환하는 함수는 각각 𝐸𝑠𝑡𝑖𝑚𝑎𝑡𝑒(𝑚),𝑆𝑒𝑛𝑑𝑒𝑟(𝑚),𝐽𝑢𝑠𝑡𝑖𝑓𝑖𝑐𝑎𝑡𝑖𝑜𝑛(𝑚)Estimate(m),Sender(m),Justification(m) 입니다.
Equivocating message(𝐸𝑞(𝑚1,𝑚2)Eq(m1,m2))는 𝑚1⊥𝑚2m1⊥m2로 표기합니다.
이전 글의 Byzantine nodes(𝐵(𝑀)B(M))는 equivocating validators(𝐸(𝜎)E(σ))와 동일합니다.
(𝜎σ는 protocol messages의 집합이기 때문에 𝑀M과 동일한 의미를 가집니다.)
이전 글의 weight of byzantine faults(𝐹(𝑀)F(M))는 equivocation fault weight(𝐹(𝜎)F(σ))와 동일합니다.
𝜎1⊆𝜎2σ1⊆σ2이기 때문에 𝐹(𝜎1)≤𝐹(𝜎2)F(σ1)≤F(σ2) 입니다. (단조 함수)
𝜎∈Σ𝑡σ∈Σt의 모든 future states를 반환하는 함수는 𝐹𝑢𝑡𝑢𝑟𝑒𝑡(𝜎)Futuret(σ)입니다.
이전 글의 Propositions의 집합 (Props(LC):C→{True,False})은 Properties of consensus values(P_C={True,False}^C)와 동일합니다. p∈PC는 𝑝(0)=𝑇𝑟𝑢𝑒p(0)=True와 같이 특정 consensus value에 대하여 boolean을 반환하는 map(function)입니다.
Properties of protocol states(𝑃_Σ={𝑇𝑟𝑢𝑒,𝐹𝑎𝑙𝑠𝑒}^Σ)는 Properties of consensus values에 대응하는 다른 집합입니다.
엄밀히 말하면 검증자의 protocol message를 이용하여 의사결정하는 노드는 검증자의 protocol state와 common future state가 존재할 경우 일관성이 보장된 의사결정을 내릴 수 있습니다. Minimal CBC Casper의 주된 주제 중 하나는 Properties of protocol states에 대하여 일관성을 증명한 후 이를 Properties of consensus value에서도 동일하게 일관성이 유지됨을 보이는 것입니다.
앞서 논의한 property of consensus values와 property of protocol states는 대응관계에 있습니다. 즉, p_C∈P_C,p_Σ∈P_Σ에 대해 pΣ=H(pC)인 함수(H:P_C→P_Σ)가 존재합니다. 𝐻H를 naturally corresponding property of protocol states라고 부릅니다.
H(p):⇔λσ.∀c∈E(σ),p(c)이며 의사코드로는 다음과 같습니다.

function H(p):
    return function (𝜎): // p_Sigma
        for all c in estimator(𝜎):
            if !p(c): return false
        return true

10. binary consensus를 예로들면, property of consensus values 𝑝∈𝑃{0,1}p∈P{0,1}가 𝑝(0)=𝑇𝑟𝑢𝑒,𝑝(1)=𝐹𝑎𝑙𝑠𝑒p(0)=True,p(1)=False일 때, 𝐻(𝑝)H(p)는 임의의 𝜎σ에 대하여 아래 식을 만족하는 property of protocol state입니다.

이전 글의 Estimate safety(𝑆(𝑝,𝜎):𝑝∈𝑃𝑟𝑜𝑝𝑠(𝐿_𝐶))는 property of consensus value에 대해하여 결정된(decided) 것과 동일합니다. (DecidedC,t:P_C×Σ_t→Boolean). 마찬가지로 property of protocol state에 대하여 결정된 것은 𝐷𝑒𝑐𝑖𝑑𝑒𝑑Σ,𝑡:𝑃_Σ×Σ→𝐵𝑜𝑜𝑙𝑒𝑎𝑛 으로 표기합니다.
DecidedC,t,DecidedΣ,t은 이전 글의 estimate safety의 정의와 마찬가지로 모든 future states에 대해서도 해당 property가 𝑇𝑟𝑢𝑒True일 경우에 성립합니다. 이들은 각각 이전 글의 보조정리 1, 3에 대응하는 forward cosnistency, backward consistency(Minimal CBC Casper의 보조정리 2, 3)를 가집니다.

11. 모든 future state에게 일관성을 가지는 결정된 properties (of consensus values or of protocol states)들에 대해서 노드는 의사결정(decision) 을 할 수 있습니다. properties of protocol states에대해 가능한 모든 의사 결정(𝐷𝑒𝑐𝑖𝑠𝑖𝑜𝑛𝑠Σ,𝑡DecisionsΣ,t)과 properties of consensus values에대해 가능한 모든 의사 결정(DecisionsC,t)은 다음과 같습니다.

다자간의 Consensus safety를 가진다는 것은 “consensus values에 대한 다자간의 의사결정이 일관성을 보이는 것”과 동일합니다. 하지만 그 전에 byzantine fault 𝑡t 이하일 때 common future state를 지는 것을 증명하는 것이 먼저입니다. 그 다음에 Common future state를 기반으로 다자간의 consensus safety까지 증명하도록 하겠습니다.

1.1.2 Common Futures

σ∈Σt의 모든 future states를 반환하는 함수는 𝐹𝑢𝑡𝑢𝑟𝑒_𝑡(𝜎)입니다.

보조정리 1: Monotonic futures

이 보조정리는 future states가 존재할 수 있는 공간는 protocol execution을 거치면서 점점 줄어든다는 것(shrinking)을 의미합니다.

정리 1: 2-party common futures

38번 라인의 “두 state의 합집합이 두 state의 future에 동일하게 포함된다”가 정리1 증명의 핵심입니다. 다르게 말하면, byzantine fault 𝑡 이하일 경우 𝜎1,𝜎2는 적어도 𝜎1∪𝜎2를 future state로 가집니다.

정리 2: 𝑛-party common futures

정리2의 증명은 위와 유사하기에 생략합니다.

위 정리들을 통해 다자간의 common future states는 byzantine fault 𝑡t 이하일 경우 언제나 존재하고, 적어도 ⋃_i=1^n σ_i가 common future state 중 하나일 것입니다. 따라서 정직한 노드들은 common future state가 존재함을 가정하고 아래에서 다룰 일관성을 보장받을 수 있습니다.

1.1.3 Consistent Decisions (Consensus Safety)

Consensus Safety란 각 노드들이 내린 의사 결정이 일관성을 가진다는 것과 동일한 의미입니다.

우선 properties of protocol states의 일관성을 다룬 이후 이를 이용하여 properties of consensus values의 일관성을 논의하겠습니다.

보조정리 2: Forward consistency

보조정리 3: Backward consistency

보조정리 1, 2는 이전 글의 보조정리 1, 3과 동일합니다.

정리 3: 2-party consensus safety

정리3의 증명은 정리1의 “common future state의 존재성”으로 시작합니다. 그리고 𝐷𝑒𝑐𝑖𝑑𝑒𝑑Σ,𝑡(estimate safety)와 forward, backward consistency(보조정리 2, 3)를 이용합니다. 정리3은 이전 글의 consensus safety와 동일한 의미를 가집니다.

2-party consensus safety를 곧바로 n-party consensus safety로 확장할 수 없는 예를 생각해봅시다. 세 properties of protocol states 𝑝,𝑞,𝑟가 𝑝∧𝑞⟹¬𝑟일 때, 세 노드는 각각 𝑝,𝑞,𝑟에 대해 결정할 수 있습니다. 그리고 세 pair (𝑝,𝑞),(𝑞,𝑟),(𝑟,𝑞)(p,q),(q,r),(r,q)는 각각이 2-party consensus safety를 달성할 수 있을 것입니다. 하지만 triple (𝑝,𝑞,𝑟)은 𝑝∧𝑞⟹¬𝑟이기 때문에 consensus safety를 가질 수 없습니다.

정의 3.4: Inconsistency of properties of protocol states

정의 3.5: Consistency of properties of protocol states

위 두 정의는 properties(𝑄)를 만족하는 𝜎가 존재하면 일관성을 가지고, 그렇지 않으면 일관성을 가지지 않음을 의미합니다.

따라서 각 노드들의 상태(𝜎_𝑖)에서 가능한 모든 의사 결정(𝐷𝑒𝑐𝑖𝑠𝑖𝑜𝑛𝑠Σ,𝑡(𝜎)={𝑝∈𝑃Σ:𝐷𝑒𝑐𝑖𝑑𝑒𝑑Σ,𝑡(𝑝,𝜎)})이 일관성을 가질 때 다자간의 consensus safety가 보장됩니다.

정리 4: 𝑛n-party consensus safety for properties of protocol states

정리 4의 대우는 일관성이 없으면 byzantine fault가 𝑡이상임을 의미합니다.

지금까지 논의한 것은 properties of protocol states에 대한 safety(consistency)입니다. 이를 이용하여 properties of consensus (values) 대한 safety까지 확장합니다.

정의 3.9: Consistency of properties of the consensus

ConsistentC는 𝐶𝑜𝑛𝑠𝑖𝑠𝑡𝑒𝑛𝑡Σ와 마찬가지로 모든 properties(𝑄)를 만족시킬 수 있는 𝑐의 존재성에 따라 결정됩니다.

보조정리 4:

보조정리 4는 정리 4에서 다룬 properties of protocol states(𝑝𝑖)의 일관성을 그에 대응하는 properties of consensus values(𝐻(𝑝𝑖))으로 확장할 수 있음을 의미합니다.

정리 5: 𝑛n-party consensus safety for properties of the consensus

정리 5는 정리 4에 보조정리 4를 이용하여 Σ에 대한 𝐶𝑜𝑛𝑠𝑖𝑠𝑡𝑒𝑛𝑡, 𝐷𝑒𝑐𝑖𝑠𝑖𝑜𝑛𝑠을 C로 확장한 것입니다.

지금까지 다룬 내용을 다시한번 간략히 요약하자면, byzantine fault 𝑡 이하일 경우 common futures가 언제나 존재하고, protocol states에 기반한 의사결정은 safety를 가지며, 이는 consensus values에 기반한 의사결정 또한 마찬가지로 safety를 가진다는 것입니다. 정리 4와 정리 5는 “byzantine fault 𝑡 이하일 경우”를 전제하고 있기 때문에 이에 대한 대우를 생각해보면, “일관성이 보장되는 𝐷𝑒𝑐𝑖𝑠𝑖𝑜𝑛𝑠가 없을 경우 byzantine fault 𝑡 초과”를 의미합니다.

Consensus safety는 safety를 가지는 estimate가 존재함을 보장합니다. 하지만 개별 노드가 DecidedC,t, 𝐷𝑒𝑐𝑖𝑑𝑒𝑑Σ,𝑡DecidedΣ,t를 계산하기 위해선 safety를 판별할 수 있는 oracle이 필요합니다. 이와 관련된 내용은 여기를 참조하십시오.

1.2 Example Protocols

Consensus safety를 가질 수 있는 프로토콜을 이더리움의 fork choice rule(GHOST)에 적용해 봅시다. 그 전에 estimate와 estimator를 정의하기 위한 몇가지 용어가 필요합니다.

protocol state 𝜎에서 관찰된 검증자들(observed validartors) 는 𝑂𝑏𝑠𝑒𝑟𝑣𝑒𝑑(𝜎)={𝑆𝑒𝑛𝑑𝑒𝑟(𝑚):𝑚∈𝜎} 입니다.
protocol message 𝑚 이후에 보내진 메시지들(later messages) 는 𝐿𝑎𝑡𝑒𝑟(𝑚,𝜎)={𝑚′∈𝜎:𝑚∈𝐽𝑢𝑠𝑡𝑖𝑓𝑖𝑐𝑎𝑡𝑖𝑜𝑛(𝑚′)} 입니다.
protocol message 𝑚을 보낸 검증자(message from a sender) 는 𝐹𝑟𝑜𝑚_𝑆𝑒𝑛𝑑𝑒𝑟(𝑣,𝜎)={𝑚∈𝜎:𝑆𝑒𝑛𝑑𝑒𝑟(𝑚)=𝑣} 입니다.
protocol message 𝑚을 보낸 검증자 집단(messages from a group) 은 𝐹𝑟𝑜𝑚_𝐺𝑟𝑜𝑢𝑝(𝑉,𝜎)={𝑚∈𝜎:𝑆𝑒𝑛𝑑𝑒𝑟(𝑚)∈𝑉} 입니다.
검증자 𝑣가 𝑚이후에 보낸 메시지들 은 𝐿𝑎𝑡𝑒𝑟_𝐹𝑟𝑜𝑚(𝑚,𝑣,𝜎)=𝐿𝑎𝑡𝑒𝑟(𝑚,𝜎)∩𝐹𝑟𝑜𝑚_𝑆𝑒𝑛𝑑𝑒𝑟(𝑣,𝜎) 입니다.
검증자 𝑣가 𝜎에서 보낸 최근 메시지(latest message) 는 𝐿_𝑀(𝜎)(𝑣)={𝑚∈𝐹𝑟𝑜𝑚_𝑆𝑒𝑛𝑑𝑒𝑟(𝑣,𝜎):𝐿𝑎𝑡𝑒𝑟_𝐹𝑟𝑜𝑚(𝑚,𝑣,𝜎)=∅} 입니다. 검증자 𝑣가 보낸 최근 메시지는 𝑣가 정직하다면 오직 1개만 존재합니다. (보조정리 5)
정직한 검증자 𝑣가 𝜎에서 보낸 최근 메시지들(latest messages from non-equivocating validators)

검증자 𝑣가 𝜎에서 보낸 최근 estimate(latest estimate) 는 𝐿_𝐸(𝜎)(𝑣)={𝐸𝑠𝑡𝑖𝑚𝑎𝑡𝑒(𝑚):𝑚∈𝐿_𝑀(𝜎)(𝑣)}입니다. 즉, latest messages의 estimate입니다.
정직한 검증자 𝑣가 𝜎에서 보낸 최근 estimate(latest estimates from non-equivocating validators) 는 𝐿_𝐻^𝐸(𝜎)(𝑣)={𝐸𝑠𝑡𝑖𝑚𝑎𝑡𝑒(𝑚):𝑚∈𝐿_𝐻^𝑀(𝜎)(𝑣)} 입니다.
두 protocol messages 𝑚1,𝑚2의 justification의 사이즈를 비교한 것을 𝑚1⪯𝑚2:⇔|𝐽𝑢𝑠𝑡𝑖𝑓𝑖𝑐𝑎𝑡𝑖𝑜𝑛(𝑚1)|≥|𝐽𝑢𝑠𝑡𝑖𝑓𝑖𝑐𝑎𝑡𝑖𝑜𝑛(𝑚2)|라고 합니다. ⪯는 두 메시지를 비교하기 위한 연산으로, (𝑆,⪯) 가 total order임을 보조정리 6에서 보입니다.
집합 𝑋에 함수 𝑓f를 적용한 가장 큰 원소들을 반환하는 함수 𝐴𝑟𝑔𝑚𝑎𝑥는 𝐴𝑟𝑔𝑚𝑎𝑥(𝑋,𝑓)={𝑥∈𝑋:∄𝑥′∈𝑋,𝑓(𝑥′)>𝑓(𝑥)}입니다.
genesis 블록 𝑔와 블록 데이터 𝐷에 대하여, n 번째 블록 𝐵𝑛과 모든 블록 𝐵B 은 다음과 같습니다.

이전 블록(부모 블록)을 반환하는 함수 𝑃𝑟𝑒𝑣는 다음과 같습니다.

유사하게 블록 𝑏의 n번째 부모 블록을 반환하는 함수 𝑛-𝑐𝑒𝑠𝑡𝑜𝑟는 다음과 같습니다.

블록 𝑏2가 블록 𝑏1을 포함했을 때 𝑏1⇂𝑏2로 표기하며, 정의는 다음과 같습니다.
𝑏1⇂𝑏2:⇔∃𝑛∈ℕ,𝑏1=𝑛-𝑐𝑒𝑠𝑡𝑜𝑟(𝑏2,𝑛)b1⇂b2:⇔∃n∈N,b1=n-cestor(b2,n)

1.2.1 Casper the Friendly GHOST (Latest Message Driven)

이 예시는 CBC Casper 방식을 Greedy Heaviest Observed Sub-Tree fork choice rule(GHOST)에 latest message를 기반으로 적용한 것입니다. 이전 포스트와 마찬가지로 추상적인 CBC 방식을 적용하는 것은 결국 올바른 estimator를 정의하는 것과 다르지 않습니다.

정의 4.27: Score of a block

𝑆𝑐𝑜𝑟𝑒(𝑏,𝜎)=∑𝑣∈:∃𝑏′∈𝐿𝐻𝐸(𝜎)(𝑣),𝑏⇂𝑏′(𝑣)Score(b,σ)=∑v∈V:∃b′∈LEH(σ)(v),b⇂b′W(v)

𝜎σ에서 𝑏b의 점수는 “𝑏b를 포함하는 latest estimate(𝑏′b′)를 보낸 정직한 검증자 𝑣v의 weight의 합” 이라고 할 수 있습니다. 여기서 주목할 점은 블록의 점수를 계산하기 위해서 latest estimate(latest message)을 사용했다는 점입니다.

정의 4.28: Children of a block

𝜎σ에서 𝑏b의 자식 블록들을 반환하는 함수 𝐶ℎ𝑖𝑙𝑑𝑟𝑒𝑛Children은 다음과 같습니다.

정의 4.28: Best Children of a block

Best children은 가장 높은 점수를 가진 자식 블록들입니다.

정의 4.30: GHOST

따라서 𝜎에서 블록체인 𝑏_의 fork choice rule을 수행한 결과인 “점수가 가장 높은 head 블록들”은 다음과 같습니다. 여기서 b_는 블록체인이기 때문에 “블록들의 집합”을 의미합니다.

위 수식을 풀어 설명하면 다음과 같습니다. “블록체인 b_에 포함된 각 블록 𝑏은 1) 𝑏가 자식 블록이 있을 경우 재귀적으로 𝐵𝑒𝑠𝑡_𝐶ℎ𝑖𝑙𝑑𝑟𝑒𝑛(𝑏,𝜎)에 대하여 𝐺𝐻𝑂𝑆𝑇를 다시 적용하고, 2) 그렇지 않을 경우 𝑏 자기 자신을 반환한다.” 입니다. 따라서 𝐺𝐻𝑂𝑆𝑇(𝑏_,𝜎)는 𝑏_에서 점수가 가장 높은 head 블록들입니다.

정의 4.31: Casper the Friendly GHOST

Casper the Friendly GHOST의 estimator는 genesis block 𝑔에 대하여 𝐺𝐻𝑂𝑆𝑇를 적용한 것과 동일합니다.

1.2.2 Casper the Friendly CBC Finality Gadget

Finality gadget은 PoW와 같은 underlying blockchain 위에서 동작하는 합의 프로토콜입니다. Finality gadget을 적용함으로써 genesis block이 아니라 finality gadget이 제공하는 finalized block에서 underlying blockchain의 fork choice rule을 적용하게 됩니다. 이번 예시에서는 CBC Casper 방식을 통해 finality gadget을 구성하겠습니다.

Underlying blockchain의 블록 𝐵, 이전 블록 𝑃𝑟𝑒𝑣, n 번째 조상 𝑛-𝑐𝑒𝑠𝑡𝑜𝑟, 블록체인 포함관계 𝑏1↓𝑏2는 이전 정의와 동일합니다.

𝐻𝑒𝑖𝑔ℎ𝑡은 블록 𝑏b의 높이를 반환하는 함수입니다.

Fork choice rule F는 “시작 블록”과 “블록체인(블록들)”을 인자로 받고 “head 블록”을 반환하는 함수입니다. (F:B×P(B)→B).

정의 4.38: Consensus values in the CBC Finality Gadget

CBC Finality Gadget에서는 Casper FFG와 마찬가지로 epoch의 checkpoint 블록을 기준으로 의사결정을 내립니다. 따라서 자연수 𝐸𝑝𝑜𝑐ℎ_𝐿𝑒𝑛𝑔𝑡ℎ∈ℕ+에 대하여, consensus values C는 다음과 같습니다.

1.2.1 Casper the Friendly GHOST에서 사용한 Score, Children, Best_Children, GHOST들을 블록이 아닌 에퍽에 대하여 재정의 해야 합니다. 𝑆𝑐𝑜𝑟𝑒_𝐸𝑝𝑜𝑐ℎ, 𝐶ℎ𝑖𝑙𝑑𝑟𝑒𝑛_𝐸𝑝𝑜𝑐ℎ𝑠, 𝐵𝑒𝑠𝑡_𝐶ℎ𝑖𝑙𝑑𝑟𝑒𝑛_𝐸𝑝𝑜𝑐ℎ𝑠은 단순히 consensus values만 모든 블록 𝐵에서 checkpoint 블록으로 달라진 것이므로 자세한 설명은 생략합니다.

정의 4.42: GHOST on epochs

정의 4.43: Estimator for the CBC Finality gadget

GHOST 또한 모든 블록 𝐵가 아닌 checkpoint 블록을 대상으로 수행하기에 동일한 로직을 가집니다.

정의 4.43: Fork Choice Rule for the CBC Finality gadget

기존의 fork choice rule은 F({g},b_) 이었습니다. Fork choice를 시작하는 블록을 CBC Casper의 estimator를 적용한 것으로, CBC 검증자들이 합의한 블록은 finalized된 것을 의미합니다.

2. Refinement and Verification of CBC Casper

Refinement and Verification of CBC Casper는 Minimal CBC Casper를 개선하고 Safety와 Liveness를 보다 엄밀히 증명하였습니다. 특히 Isabelle/HOL을 이용하여 formal verification을 구현한 결과를 LayerXcom/cbc-casper-proof에서 확인할 수 있습니다.

2.1 Safety Oracle

이전 포스트에서 언급했던 simple clique oracle의 정의 및 clique 내부의 검증자들이 정말 safety를 올바르게 판별할 수 있는지는 엄밀히 증명하지 않았습니다. Minimal CBC Casper 또한 증명을 생략한 상태이고 얻을 수 있는 자료는 오랜기간 병합되지 않은 cbc-casper/cbc-casper-paper#13뿐입니다. 논리상 문제가 있는 부분은 아직 발견되지 않았으며 사소한 오탈자와 용어정리 측면에서는 변경의 여지가 있음을 감안하고 살펴보도록 하겠습니다.
(보조정리가 많이 사용되는 관계로 결론을 내기위해 필요한 보조정리를 위주로 살펴봅니다. 모든 정의 및 보조정리 목록은 여기서 확인할 수 있습니다.)

2.1.1 Definitions

Latest justifications from non-Equivocating validators:

정직한 검증자 𝑣의 𝜎에서의 최신 메시지 𝑚의 justification입니다.

Validators agreeing with p in σ:

이전 포스트에서 논의했던 “𝑝에 동의하는 검증자”들의 집합입니다. 검증자 𝑣는 𝜎에서의 모든 latest estimates가 𝑝에 대해 참일 경우 “𝑝에 동의”합니다.

Validators disagreeing with p in σ:

이전 포스트에서 논의했던 “𝑝에 반대하는 검증자”들의 집합입니다. 동의하는 검증자들(𝐴𝑔𝑟𝑒𝑒𝑖𝑛𝑔(𝑝,𝜎)), 반대하는 검증자들(𝐷𝑖𝑠𝑎𝑔𝑟𝑒𝑒𝑖𝑛𝑔(𝑝,𝜎)), equivocating하는 검증자들(𝐸(𝜎))는 서로 겹치지 않습니다. (mutually disjoint)

Weight measure:

검증자 집단의 총 weight의 합을 반환하는 함수입니다.

Non-equivocating majority:

이전 포스트에서 “clique에 속한 검증자들의 총 weight이 모든 검증자의 weight의 1/2보다 클 때 clique 내부 혹은 외부의 새로운 메시지가 estiamte의 score를 변경시키지 않는다”고 했습니다. 위 문장의 선행 조건을 𝑀𝑎𝑗𝑜𝑟𝑖𝑡𝑦^𝐻(𝑉,𝜎)로 표기합니다.

Non-equivocating majority driven property:

𝑀𝑎𝑗𝑜𝑟𝑖𝑡𝑦_𝐷𝑟𝑖𝑣𝑒𝑛𝐻(𝑝)는 모든 𝜎∈Σσ∈Σ에 대하여 ㅔ[¬MajorityH(Agreeing(p,σ))]∨[MajorityH(Agreeing(p,σ))∧∀c∈E(σ),p(c)]일 것입니다. 따라서 𝑀𝑎𝑗𝑜𝑟𝑖𝑡𝑦_𝐷𝑟𝑖𝑣𝑒𝑛𝐻는 𝑀𝑎𝑗𝑜𝑟𝑖𝑡𝑦𝐻가 참이라면 “다수가 동의하는 𝐷𝑒𝑐𝑖𝑑𝑒𝑑𝐶,𝑡 될 수 있는 𝑝의 집합”는 의미로 해석할 수 있습니다.

Max weight driven property:

𝑀𝑎𝑗𝑜𝑟𝑖𝑡𝑦_𝐷𝑟𝑖𝑣𝑒𝑛𝐻과 유사합니다. 특히 V∖Agreeing(p,σ)∖Disagreeing(p,σ)∖E(σ)=∅ 인 𝜎 (메시지를 보내지 않은 검증자가 없을 경우) 에서는 𝑀𝑎𝑗𝑜𝑟𝑖𝑡𝑦_𝐷𝑟𝑖𝑣𝑒𝑛𝐻와 동일한 의미를 가집니다.

Later disagreeing messages:

𝜎에서 메시지 𝑚이후로 검증자 𝑣가 보낸 𝑝에 반대하는 메시지들의 집합입니다.

helper function(!) := “!({a}) = a”:

! 함수는 크기가 1인 집합에서 유일하게 존재하는 해당 원소를 반환하는 함수입니다. 크기가 1보다 크거나 0일때는 정의되지 않습니다. !는 𝐿_𝐻^𝑀,𝐿_𝐻^𝐸와 같은 정직한 노드의 최신 메시지(혹은 estimate)는 1개만 있기 때문에 해당 메시지(혹은 estimate)를 선택하기 위해 사용됩니다.
Clique with n layers:

𝑛=1일 때를 1-layer clique라고 합니다. 1-layer clique의 정의는 이전 포스트와 동일하게 “상호 동의” 하였고, 이후에 “반대하지 않는” 검증자들 입니다.
𝑛>1일 경우 재귀적으로 𝜎에서 𝐿_𝐻^𝐽(𝜎)(𝑣)로 protocol state를 대상으로 clique를 확인하며, 𝑛-layer clique라고 합니다.

위 그림에서 실선은 부모 블록 참조를, 점선은 메시지 justification을 의미합니다. 이 때, 검증자 A, C, D가 2번째로 보낸 파란색 블록들의 justification은 빨간 블록들을 포함하고 있다는 사실에 주목하십시오. 그리고 빨간 블록들은 (암시적으로) 검증자 A가 처음으로 보낸, 가장 왼쪽의 빨간 블록을 justification으로 포함하고 있습니다. 1-layer clique는 가장 왼쪽 블록에 대한 clique를 형성하기 위하여 파란 블록들(latest estimates)과 그의 justificatoin (latest justification)에 대한 “𝐴𝑔𝑟𝑒𝑒𝑖𝑛𝑔과 𝐿𝑎𝑡𝑒𝑟_𝐷𝑖𝑠𝑎𝑔𝑟𝑒𝑒𝑖𝑛𝑔”.을 이용하고 있습니다.

Minimal transitions:

One layer clique oracle threshold size:

이전 포스트에서 다뤘던 “𝑒-clique in 𝑀이 안전하기 위한 검증자들의 weight의 합의 최소값”입니다. 이는 byzantine fault 𝑡와 다른 값입니다. 𝑇ℎ𝑟𝑒𝑠ℎ𝑜𝑙𝑑𝑡(𝑉,𝜎)는 𝑀𝑎𝑗𝑜𝑟𝑖𝑡𝑦𝐻(𝑉,𝜎) 보다 더 큰 값에 대하여 비교하고 있습니다. (Weight(V)/2+t−Weight(E(σ))>Weight(V∖E(σ))/2) 따라서 𝑇ℎ𝑟𝑒𝑠ℎ𝑜𝑙𝑑𝑡(𝑉,𝜎) 이면 𝑀𝑎𝑗𝑜𝑟𝑖𝑡𝑦𝐻(𝑉,𝜎) 입니다. (보조정리 32)

Clique oracle with n layers:

이제 clique의 내부 혹은 외부 검증자가 보낸 새로운 메시지 m¯가 clique를 새로운 𝜎′와 기존 검증자 집단 𝑉에 대하여 그대로 유지할 수 있음을 살펴봅시다.

2.1.2 Cliques Survive Messages from Validators Outside Clique

보조정리 16: Minimal transition from outside clique maintains clique

보조정리 11부터 보조정리 15는 minimal transition을 일으킨 검증자를 제외한 다른 검증자들의 다양한 특성들(later, equivocation status, latest message, latest justification, later disagreeing)을 변경시키지 않음을 보입니다. 이를 이용하여 보조정리 16을 증명할 수 있습니다.

이 보조정리는 clique 외부의 검증자들이 보낸 새로운 매시지들은 clique를 바꾸지 못한다는 의미입니다. 따라서 외부 검증자들의 equivocating 여부와 관계 없이 clique는 항상 유효할 것입니다.

다음으로는 clique 내부의 검증자들이 보낸 새로운 메시지들에 대하여 clique가 보존될 수 있는지 살펴봅시다. 경우를 나누자면 서로가 동의함을 확인한 clique 내부 검증자들은 새로운 메시지를 보낸 검증자가 1) non-equivocating 하거나 2) equivocating 하거나 둘 중 하나일 것입니다.

2.1.3 Cliques Survice Messages from Validators Inside Clique

이 항목에서 논의할 내용은 다음 순서로 구성됩니다.

(보조정리 17): 우선 새로운 메시지와 clique에 속한 검증자 집합간의 관계에 대해서 다룹니다.
(보조정리 18 ~ 보조정리 23): clique 내부의 정직한(non-equivocating) 검증자 𝑣⎯가 보낸 새로운 메시지 𝑚⎯는 검증자 집단 𝑉이 𝐽𝑢𝑠𝑡𝑖𝑓𝑖𝑐𝑎𝑡𝑖𝑜𝑛(𝑚⎯)에 대한 동의를 암시합니다.
(𝑉⊆𝐴𝑔𝑟𝑒𝑒𝑖𝑛𝑔(𝑝,𝐽𝑢𝑠𝑡𝑖𝑓𝑖𝑐𝑎𝑡𝑖𝑜𝑛(𝑚⎯)))
(보조정리 24): Majority clique 내부의 정직한(non-equivocating) 검증자 𝑣⎯⎯⎯v¯가 보낸 새로운 메시지 𝑚⎯는 𝑣⎯가 𝜎′에서 𝑝에 대해 동의합니다.
(𝑣⎯⎯⎯∈𝐴𝑔𝑟𝑒𝑒𝑖𝑛𝑔(𝑝,𝜎′))
(보조정리 25 ~ 보조정리 31): 2, 3번을 확장하여 Majority clique 내부의 정직한(non-equivocating) 검증자 𝑣⎯가 보낸 새로운 메시지 𝑚⎯는 clique를 𝜎′에서 여전히 유효합니다.
(보조정리 32 ~ 보조정리 36): clique 에 속한 검증자가 보낸 새로운 메시지 𝑚⎯이 equivocating 하더라도 clique는 보존됩니다.

2.1.3.1 보조정리 17

보조정리 17: Free sub-clique

이 보조정리는 𝑣⎯의 새로운 메시지 𝑚⎯는 적어도 𝑉∖{𝑣⎯}로 이루어진 새로운 clique를 생성한다는 의미입니다. 물론 𝑚⎯가 𝐴𝑔𝑟𝑒𝑒𝑖𝑛𝑔(𝑝,𝐿_𝐻^𝐽(𝜎′)(𝑣⎯)))를 동일하게 유지한다면, 검증자 집합은 새로운 clique에서도 동일합니다.

2.1.3.2 보조정리 18 ~ 보조정리 23

보조정리 20: Latest honest messages from non-equivocating messages are either the same as in their previous latest message, or later

보조정리 20은 크게 두가지 경우로 나누어져 있습니다. 𝑣⎯가 𝑣의 새로운 메시지를 발견했을 때, 이를 𝑁𝑒𝑤 라고 한다면, 𝑁𝑒𝑤=∅ 혹은 𝑁𝑒𝑤≠∅ 인 두 가지 경우로 나뉩니다. 이 두 경우들이 ∨로 해당 보조정리에서 연결되어 있습니다.

보조정리 23: Non-equivocating messages from clique members see clique agree

보조정리 20에 따르면, 𝐽𝑢𝑠𝑡𝑖𝑓𝑖𝑐𝑎𝑡𝑖𝑜𝑛(𝑚⎯)을 통해 𝑣⎯가 𝑣의 새로운 메시지를 확인했는지 아닌지에 따라 경우가 나뉘었습니다. 이 두 경우를 clique의 정의 각각과 연결지어 증명합니다. 첫 번째 경우(𝑁𝑒𝑤=∅)엔 clique의 정의 “clique에 속한 검증자들은 서로가 동의함을 확인함”를 이용합니다. 두 번째 경우(𝑁𝑒𝑤≠∅)엔 clique의 정의 “이후에 disagreeing 하지 않음”을 이용합니다.

보조정리 23은 𝐽𝑢𝑠𝑡𝑖𝑓𝑖𝑐𝑎𝑡𝑖𝑜𝑛(𝑚⎯)에 대해서 clique가 동의함을 보이고 있습니다. 그러나 𝐽𝑢𝑠𝑡𝑖𝑓𝑖𝑐𝑎𝑡𝑖𝑜𝑛(𝑚⎯)은 어디까지나 과거 메시지입니다. 새로운 프로토콜 상태인 𝜎′로 확장하는 것은 보조정리 24에서 다룹니다.

2.1.3.3 보조정리 24

보조정리 24: New messages from majority clique members agree

2.1.3.4 보조정리 25 ~ 보조정리 31

보조정리 31: New non-equivocating latest messages from members of majority clique don’t break the clique

2.1.3.5 보조정리 32 ~ 보조정리 36

Equovication 한 검증자는 clique의 정의(상호 동의)에 따라 clique에 속할 수 없습니다. 따라서 clique의 검증자 집단은 해당 minimal transition으로 인해 𝑉∖{𝑣⎯}으로 변경될 수 밖에 없습니다. 따라서 우리는 clique 검증자 집단의 weight의 총 합은 𝑊𝑒𝑖𝑔ℎ𝑡({𝑣⎯})만큼 줄어듬에도 불구하고, clique oracle이 유효할 수 있는지를 주목해야 합니다.

보조정리 33부터 35는 clique oracle이 minimal transition에 대하여 33) 검증자가 clique 외부에 있을 때 34) 검증자가 내부에서 non-equivocating 할 때 35) 검증자가 내부에서 equivocating 할 때로 나누어 증명 합니다. 그리고 이 세개의 보조정리를 취합하여 보조정리 36을 증명합니다. 보조정리 33, 34는 기존의 보조정리 16, 31에 대응합니다. 따라서 이번엔 equivocation을 다루는 보조정리 35에 집중합니다.

보조정리 35: Clique oracles preserved over minimal transitions from equivocating validators

보조정리 36: Clique oracles preserved over minimal transitions

보조정리 33, 34, 35을 이용하여 증명합니다.

2.2 Clique Oracle Is A Safety Oracle

지금까지 clique oracle의 검증자 집단 내부 혹은 외부에서의 새로운 메시지의 equivocation 여부와 관계 없이 항상 clique oracle이 보존된다는 것을 살펴봤습니다. 이렇게 항상 유지되는 clique oracle을 이용하여 consensus safety를 적용할 수 있는 𝐷𝑒𝑐𝑖𝑑𝑒𝑑𝑡를 판별할 수 있는지, 다르게 표현하면, clique oracle이 safe oracle인지 살펴보겠습니다.

보조정리 37: if there is a clique, then everyone in the clique is agreeing in the current protocol state.

보조정리 38: if there is a threshold sized clique where no validators are equivocating, then the estimator will agree.

보조정리 39: Cliques exist in all futures

보조정리 40: Clique oracle is a safety oracle

Conclusion

이번 포스트에서는 n-party consensus safety 정리와 이를 적용한 Casper the Friendly GHOST (Latest Message Driven GHOST)와 Casper the Friendly CBC Finality Gadget를 살펴봤습니다. 또한 이전 포스트에서 미흡했던 safety에 대한 내용을 clique oracle이 safety oracle인지 살펴보았습니다.