ブロックチェーンと形式検証
～ Tezos の場合
Jun FURUSE/古瀬 淳
ブロックチェーンとは…
- 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ネットワーク:
- 中央管理者がいない
- 中立で改竄が非常に難しい
- 低コスト
オープン・ネットワークでの合意問題
シビル攻撃
閉じたネットワークでの合意形成アルゴリズムは動作しない。
オープン・ネットワークではアカウントをいくらでも作れる。 票数水増しにより合意形成の操作と妨害ができてしまう。
サトシ・ナカモトとBitcoin
シビル攻撃(票数水増し)を不可能にする難しくする:
- 投票にはDB外の有限リソースである計算能力を要求
- トークン報酬: リソースを提供し正直に行動することを奨励する
- トークンはDB上で管理
換金性のあるトークン → 暗号通貨の誕生
暗号通貨は非中央集権分散DBのシビル攻撃への解
スマートコントラクト
汎用DBだからプログラムを置くこともできる
- アカウントにコードを紐づける
- アカウントにデータを送(金す)るとコードが動き出す
- コードによるDBの変更や更なる送金
契約の自動執行が可能 (Non native tokens, 分散型交換所(DEX), etc)
ブロックチェーンでの形式検証の意義
金銭的価値の貯蔵手段となったブロックチェーン。
バグ、セキュリティーホールは価値の喪失や窃取につながる。
ハッキングによる窃取が発生した場合、被害回復は非常に難しい:
- 犯人特定が難しい (KYC/AML などはあるが)
- 非中央集権のため、窃取を取り戻すことも難しい
- Code as constitution: 「バグも仕様」という考え方
バグの無い事が非常に求められる。テストだけでは不十分
ヘッジファンド、投資銀行での形式検証
投資銀行などでもバグは大きな金銭的損失を引き起こす。
が、一回り昔、自分の周辺では形式検証が使われているという話はなかった。(個人の感想です)
- 検証の時間コストが大きすぎ、仕様変更に追いつかない。
(コストの低い静的型は大好き)
- 中央集権のため比較的対処しやすい
- 銀行内で使うクローズドソース内製品のバグを外部から突くのは難しい
ブロックチェーンは OSS でなければならない
- 最終責任者はいない: 公開コードが正義
- 誰でもノードを立ち上げ、ブロックを実行、確認できなければならない
価値を扱う OSS は攻撃者の格好の標的。
テストでは不十分で、形式検証でバグを極力なくすべき。
とはいえ、形式検証が大いに使われているわけでもなく、
毎年多額の被害が発生している†
弊社にとって別の意味で大変です😩
Tezos の特徴
- OCaml による実装。形式検証を重視
- Proof of Stake
- オンチェーン・ガバナンス
- スマートコントラクト (Michelsonスタックマシーン)
Tezos と OCaml
開発速度と安全性のバランスから OCaml を選択
- 静的型システム
- 金融システム実装での使用例
- 形式検証しやすさ (Coq, F\(*\))
Proof of Stake
分散環境での合意形成に使われる、複製できない「投票権」として 計算資源(Proof of Work)ではなく、ステーク(チェーン上に保有するトークン量)を使用。
計算資源を浪費しないのでエネルギー効率が良い:
- Tezos: 0.001 TWh (PwCしらべ)
- Ethereum: 26 TWh
- Bitcoin : 130 TWh
PoW は最近特に風当たりが強い †,†
オンチェーン・ガバナンス
プロトコルのアップグレード案をチェーン上の投票で承認する†
- ステークに比例した投票権
- 二段階投票
- 複数の案から一件を選ぶ投票
- 選ばれた案を実際に採用するか投票
ステークホルダが理解できない機能は否決される。
約3ヶ月に一度のプロトコルアップグレード。忙しい。
メリハリが大切: 形式検証するべき vs テストで済ますべき
Tezos 検証事例
- スマートコントラクト
- シェル(ネットワーク、ストレージ、暗号、etc)
- プロトコル(合意形成、経済プロトコル、スマートコントラクト)
Tezos スマートコントラクトの検証
検証活動が一番盛んだと思われる
- 参入障壁が低く、質の悪いコードがあると思われる
- ブロックチェーンの他の構成要素と比較して、プログラムは非常に短い
ハックしやすく、検証しやすい
スマートコントラクト
Michelsonスタックマシーン
- ブロックの検証時間に上限を課すため計算量を測る必要がある
言語自体を安全に、検証しやすく:
- 静的型付き純粋関数型:
param * storage -> tx list * storage
- エラーハンドリング
option, result (Either)- 例外が発生すると tx 全体が失敗
- コンテナ型:
list, set, map
- 任意精度整数
- Tail recursion (
LOOP)
Michelson プログラムの形式検証
- Mi-Cho-Coq: Michelson の Coq モデル
- Helmholtz: Michelson + 篩型
- K-Michelson: K framework による Michelson モデル化
Michelson の Coq モデル。
- Michelson opcode はそのままコンストラクタになっていて、Coq 中で Michelson プログラムを自然に書ける。
- Dependent inductive type を使って well-typed な Michelson しか書けない。
- 評価器による意味論の定義。
LOOP によって停止しない事を避けるため、評価器に 再帰呼び出し上限 fuel を設定。
例: boomerang
Michelson + 篩型
詳しくは、この後の
“Helmholtz: A Verifier for Tezos Smart Contracts Based on Refinement Types”
を。
高級言語から Michelson へのコンパイル
内部は純粋関数型
副作用バリバリの「普通の」プログラム (ex. Python) から Michelson へのコンパイルは難しい…
コントラクトの不変条件や事後条件を記述できる†
トークン実装での条件例:
# トータル発行量は変化しない:
specification {
s1: ledger.sum(tokens) = totalsupply;
}
#自分自身に送金する場合、状態は変わらない
postcondition transfer_p3 {
%from = %to -> ledger = before.ledger
}
これらの証明すべき条件を Why3を通して抽出し、 自動証明や証明支援系で証明する。
Coq でスマートコントラクトを書いて、Michelson に持っていく
- Mi-Cho-Coq と違って高級言語で書ける
- MetaCoq を使って LIGO や Rust に extraction
- Tezos の場合は LIGO に落としてそこから Michelson へコンパイル
- LIGO は単相型なので苦労があるようです
Contract interaction テストが可能
- コントラクトは一回呼び出されて終わりではなく、storage が更新され、繰り返し呼び出される
- QuickChick を使った連続呼び出し時の random property test を提供
スマートコントラクトの検証: まとめ
いろいろ道具立てはある。
- コントラクト単体の functional correctness の証明はやれば、できる
- (もちろん、やらないと、できない)
これからは contract interaction
Spec が抜けていれば…証明されない!!†,†,†
- 細かい spec を網羅することは難しい
- ざっくりとした spec からヤバそうなモノを見つけて欲しい
(そんなことできるのか)
NaCl互換の暗号ライブラリ。F\(*\)で安全性が検証されている:
- Memory safety
- Functional correctness
- Secret independence (タイミング攻撃耐性)
F\(*\) のサブセット Low\(*\) で書かれている。 KreMLin を使って C にコンパイル。
“Context” ストレージ・サブシステム
ブロックチェーン状態ためのファイルシステム
Merkle Patricia Tree を利用
- 純粋関数型データ型
- Append-only file system
- Treeの各ノードは Merkle hash H(n) を持つ
- H(File(\(v\))) = h(0 || \(v\))
- H(Internal(\(l_L\), \(n_L\), \(l_R\), \(n_R\))) =
h(1 || \(l_L\) || H(\(n_L\)) || \(l_R\) || H(\(n_R\)))
- H(Directory(\(n\))) = H(\(n\))
実装が間違っていると、ブロックチェーン状態がおかしくなる!!
Merkle Patricia Tree
このままでは各ノードのディスク上のデータ幅が違いすぎる
![]()
Plebeia Tree
最適化: Internal を Branch と Extender に分け、幅をそろえる
![]()
Plebeia Tree の不変条件
最適化のため不変条件が複雑化
- 木の形: 例: Extender の下に Extender はこない
- Hash 計算された node の子供は hash 計算されている
- ディスクに保存された node の子供はディスクに保存されている
- 木の操作に Zipper を使うため同様の不変条件が Zipper にも
OCaml で書かれた木の操作が不変条件を保存する事を F\(*\) で証明(論文)。
Plebeia: Merkle hash 衝突バグ
初期の Plebeia Merkle hash 計算:
- H(File(\(v\))) = ( h(0 || \(v\)), "" )
- H(Directory(\(n\))) = H(\(n\))
- H(Branch(\(n_l\), \(n_r\))) = ( h(1 || H(\(n_l\)) || H(\(n_r\))), "" )
- H(Extender(\(l\), \(n\)) = ( fst (H(\(n\))), \(l\) )
Hash consing のランダムテストでデータが壊れた:
H(Extender(\(l\), File(\(v\))))
= H(Extender(\(l\), Directory(Extender(\(l\), File(\(v\))))))
Plebeia: Merkle hash 衝突修正
修正版:
- H(File(\(v\))) = ( h(0 || \(v\)), "" )
- H(Directory(\(n\))) = ( h(2 || H(\(n\)) ), "" )
- H(Branch(\(n_l\), \(n_r\))) = ( h(1 || H(\(n_l\)) || H(\(n_r\))), "" )
- H(Extender(\(l\), \(n\)) = ( fst (H(\(n\))), \(l\) )
修正版の正しさを Coq で証明:
- Node の型と Merkle hash計算をモデル化
- (嘘だけれども)hash関数(文字列 → hash)の単写性を仮定
- Merkle hash計算の単写性を証明: \(n_1 \neq n_2 \Longrightarrow H(n_1) \neq H(n_2)\)
Tezos のプロトコルコードの正しさを証明していくプロジェクト
OCaml コードを Coq コードに変換する coq-of-ocaml を使用。
- Serialization の正しさ
type t = {x : int; y : int}
let t_encoding =
conv (fun {x; y} -> (x, y))
(fun (y, x) -> {x; y}) (* bug *)
(tup2 int int)
- Storage の正しさ
- ブロックチェーン状態をメモリ上で現し、その変更と、プロトコルの実際のストレージ・サブシステムへの読み書きが一致する事を証明
- Mi-Cho-Coq での Michelson モデル化の正しさ
- プロトコルコード内の Michelson 実装を coq-of-ocaml で
Coq に連れてきて比較
現在の Tezos 合意アルゴリズム Emmy*
Nakamoto consensus に基づくアルゴリズム。
確率的 finality: ブロックが作られても後で別のブランチに覆される可能性がある(確率は指数関数的に減るが)。
\(↗︎\stackrel{B_{n+1}}→ S_{n+1}\) 😢
\(.. \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}\)
次期 Tezos 合意アルゴリズム Tenderbake
BFT consensus に基づく合意アルゴリズム(3/18ころ切替)
確定的 finality: 一度ブロックがチェーンに付け加えられると覆されることはない。
Tenderbake には正しさの手証明はある。 機械証明に向けて TLA+ を使ったモデル化がされている。
TLA+ を使い、Tezos ネットワークに参加したばかりのノードが正しく現在のネットワークのブロックチェーン状態に追いつくことの検証も行っている。
結論
ブロックチェーンは非中央集権オープンネットワークDB
動作のため金銭的価値のあるトークンを扱う宿命
OSSで価値を扱うため形式検証してバグを無くしたい
Tezos では全レイヤで形式検証を頑張っている
- それでも全然証明が追いついていない…
- 実装、テスト、静的型、形式検証、うまくバランスを取っていきたい
