ブロックチェーンと形式検証
~ Tezos の場合
~ Tezos の場合
Jun FURUSE/古瀬 淳
PPL 2022, Japan, 2022-03-06
ブロックチェーンとは…
- Bitcoin
- 暗号通貨
- 投機、相場
- アナーキー、詐欺
- 反環境、制裁逃れ…
もうすこし CS 的に
ブロックチェーンとは:
汎用分散データベース
- 台帳方式
- 分散環境
- オープン・ネットワーク、非中央集権制
- スマートコントラクト
台帳方式
変更履歴集積としてのデータベース (like 銀行通帳, Git)
- \(S_i\) : ブロックチェーン状態
- \(B_i\) : ブロック: 差分。Minerがトランザクションを集めてくる。
- \(S_i = B_i(S_{i-1})\)
ブロックチェーン:
\[\mathtt{∅} \stackrel{B_{1}}→ S_{1} \stackrel{B_{2}}→ S_{2} \stackrel{B_{3}}→ S_{3} \stackrel{B_{4}}→ S_{4} \stackrel{B_{5}}→ S_{5} \stackrel{B_{6}}→ \cdots\]
分散環境
複数のデータベースノードが状態のレプリカを持つ:
- 耐故障性
- 負荷分散
衝突をどう解消するか?
ブロックチェーンでの衝突
チェーンが分岐する。どちらを選ぶか:
\(↗︎\stackrel{B_{n+1}}→ S_{n+1} \stackrel{B_{n+2}}→ S_{n+2} \stackrel{B_{n+3}}→ S_{n+3}\)
\(.. \stackrel{B_{n-1}}→ S_{n-1} \stackrel{B_{n}}→ S_{n}\)
\(↘︎\underset{B'_{n+1}}→ S'_{n+1} \underset{B'_{n+2}}→ S'_{n+2} \underset{B'_{n+3}}→ S'_{n+3}\)
分散合意アルゴリズム
ノード間の衝突を解決するアルゴリズム。
完璧なアルゴリズムは存在しない[FLP85]が、
Paxos や Raft など実用上問題ないアルゴリズムがある。
- 衝突はノード間多数決投票で解消
- ただし、固定されたノードからなる閉じたネットワークでしか動作しない
オープン・ネットワーク
誰もがノードを立て参加できる
パーミッションレスな分散DBネットワーク:
- 中央管理者がいない
- 中立で改竄が非常に難しい
- 低コスト