チュートリアル: ブロックチェーンの計算モデル

Transcription

1 PPL 2018 [C4] チュートリアル : ブロックチェーンの計算モデル Shin Saito, Sachiko Yoshihama IBM Research - Tokyo

2 背景 近年ブロックチェーン技術に代表される分散技術が注目を浴びている 仮想通貨のインフラとして 業務アプリケーションのプラットフォームとして 金融 保険 貿易 健康管理 トレーサビリティ 食の安全 法整備も進んでいる 改正資金決済法 (2016): 仮想通貨 仮想通貨交換業者 の定義 改正犯罪収益移転防止法 (2017): 特定事業者 として 仮想通貨交換業者 を追加

3 参考 : 仮想通貨の定義 資金決済に関する法律 ( 平成二十八年六月三日公布 ) 改正 第二条第 5 項この法律において 仮想通貨 とは 次に掲げるものをいう 一物品を購入し 若しくは借り受け 又は役務の提供を受ける場合に これらの代価の弁済のために不特定の者に対して使用することができ かつ 不特定の者を相手方として購入及び 売却を行うことができる財産的価値 ( 電子機器その他の物に電子的方法により記録されている ものに限り 本邦通貨及び外国通貨並びに通貨建資産を除く 次号において同じ ) であって 電子情報処理組織を用いて移転することができるもの 二不特定の者を相手方として前号に掲げるものと相互に交換を行うことができる財産的価値であって 電子情報処理組織を用いて移転することができるもの 通貨建資産 : 電子マネーなどを指すとみられる

4 分散技術 (Distributed Ledger Technology) 複数の対等なノードがそれぞれを保持 同期 ノード A ノード A ノード A スマートコントラクト TX を accept するか否か TX に伴うビジネスロジックを実行 ノード A DLT の特徴 = トランザクション (TX) 列 TXs Alice Bob: 10BTC Bob Charlie: 5BTC 得意非集中性耐障害性耐監査性インテグリティ否認防止 不得意 秘匿性 スケーラビリティ

5 ブロックチェーン ( 以下 チェーン ) のデータ構造の 1 つ をブロックのチェーンとして構成 追記のみ可能 改竄不可能 (or 改竄検出可能 ) 否認不可能なデータ構造 分散合意 ( 非集中型コンセンサス ) ノードが対等に同期を取る ブロック N を改竄してもバレないためにはブロック N+1 すべての改竄が必要 ブロック N-2 のハッシュ値 ブロック N-1 のハッシュ値 ブロック N のハッシュ値 TX 1 TX 2 TX N

6 スマートコントラクト スマートコントラクト [Szabo '94] TXをacceptするか否か Aliceの残高は10BTC 以上? TXに伴うビジネスロジックを実行 Aliceの残高 -= 10BTC BoBの残高 += 10BTC チューリング完全 / 不完全 法律の契約 (legal contract) とは直接の関係はない User Alice Bob User Alice Bob Balance 100 BTC 10 BTC Alice Bob: 10BTC Balance 90 BTC 20 BTC

7 DLT のバグを突いた攻撃または不具合例 Bitcoin: Script malleability による DoS 攻撃とウォレットクライアントへの攻撃 Ethereum: The DAO 事件 (2016) スマートコントラクトの不具合を突いた 65 億円仮想通貨流出事件 ( 後述 ) Ethereum: コンセンサスバグ (2016) Parity (Ethereum クライアント ) のマルチシグウォッレットバグ (2017) マルチシグ = 複数人の署名がないと通貨を使用できない仕組み 34 億円の被害 ETH が凍結されてしまう Parity のバグによりコントラクトを破壊 (2017) 316 億円分の ETH がロックされる Ethereum に多いのはチューリング完全なスマートコントラクトであったりと 表現力が強いためか 分散計算モデルとしての検証が不十分では?

8 参考 : 仮想通貨流出事件の例 Mt. Gox (2011): 2609BTC 秘密鍵のないアドレスに誤送信 BitFloor (2012): 24K BTC (155 億円 ) セキュリティ対策の不備 Mt. Gox (2014): +750K BTC (470 億円 ) +28 億円 Coincheck (2018): 500M XEM (580 億円 ) New! セキュリティ対策の不備 Reference: Poloniex (2014): 97BTC (6000 万円 ) 出金コードの脆弱性 Bitstamp (2015): 19K BTC (12 億円 ) Bitfinex (2016): 120K BTC (777 億円 ) マルチシグアーキテクチャの脆弱性? NiceHash (2017): 4.7K BTC (60 億円 )

9 なぜ検証が不十分か 分散システムゆえの複雑さ スマートコントラクトの表現力ゆえの複雑さ どんどん新しい実装が出る 本発表の目的 DLT 実装およびその上のスマートコントラクトの解析の参考となる 主要なDLT 実装の紹介 モデル化ならびに解析手法の例を紹介

10 主要な DLT 実装

11 システムの前提 悪意のあるノードの存在 ( ビザンチン障害 ) を仮定する 一部の Permissioned 型システムはクラッシュ障害のみを仮定する ノードはネットワーク上に分散している 同期には時間がかかる ノード間通信は非同期的である ネットワークは信頼できない 送信したメッセージは重複したり 変形したり 順序が変わったり 消えたりする ネットワークが分断することもあり得る

12 DLT アーキテクチャの大分類 Public 型 参加ノード ユーザ誰でも許可制 Permissioned (Consortium) 型 合意に参加するノード数不定たいてい固定 合意アルゴリズム インセンティブ設計系 (Proof of Work など ) ファイナリティなしあり ビザンチン合意系 アプリケーション仮想通貨など業務アプリケーション 重視される性質非集中性 障害耐性速度 プライバシー

13 DLT の実装タイプ 各カテゴリから主要なものを紹介 スマートコントラクトの表現力 の共有範囲 Public 型 Permissioned 型 非チューリング完全全共有 Bitcoin - チューリング完全 全共有 Ethereum Hyperledger Fabric v1 一部共有 - Corda

14 DLT の実装例 (1): Bitcoin [Nakamoto 09] をベースにしたブロックチェーン実装 各種の Public 型 DLT 実装のもとになっている DLTタイプチェーン構造資産 TX 検証タイプ共有コンセンサスファイナリティスマートコントラクト Public 型 線形 コイン (BTC/XBT) UTXO + Script UTXO ベース 全共有 Proof of Work なし Script 非チューリング完全

15 登場人物 マイナー (Miner) 報酬を目当てにマイニングを行い ブロックを作成するノード マイナー フルノード (Full node) チェーンの正当性検証のみを行う良いノード メリットがないので減少傾向にあるとか フルノード クライアント (Client) 手数料を支払い TX を送信してそれがチェーンに加えられるのを待つ クライアント

16 プロトコル (1): TX の送信 クライアントが TX を送信 TX 内容はコインの移転のみ マイナー A マイナー B TX は P2P ネットワークにより各マイナーの mempool (memory pool) に入る TX98 TX100 TX100 TX99 TX100: Alice -> Bob: 10 BTC クライアント 現在の mempool サイズは約 27M TXs:

17 プロトコル (2): マイニング競争 各マイナーは mempool にある TXs からブロックを作るべくマイニング競争を行う マイナー A マイナー B なぜか? マイニングに成功してチェーンにつなげられると 報酬が (BTC で ) 入るから ( 後述 ) ブロックを捏造して広げるより真面目にマイニングしたほうが割にあう ( と考えられる ) から TX98 TX100 TX100: Alice -> Bob: 10 BTC TX100 TX99 クライアント Images from いらすとや

18 マイニングとは (Proof of Work) ブロックヘッダの dhash 値が ターゲット 値以下になるような nonce を見つける作業 double hash: dhash x := sha256 (sha256 x) ブロックを作成できたということが 作業の証拠 = Proof of Work になる Hashcash として電子メール送信などでも提案されていた ブロックヘッダ [80] ブロックバージョン [4] 直前ブロックハッシュ [32] TXsのMerkle rootハッシュ [32] 現在時刻 [4] 現ターゲット値 (Bits) [4] 見つけたnonce [4] such that dhash( ブロックヘッダ ) <= ターゲット値

19 マイニングとは (Proof of Work) 最近のブロックの例 (#511924) 7e35b090f5fc858f a62376fe3cc01916ee9 Bits (hex) 困難度 (difficulty) ターゲット (hex) ブロックヘッダハッシュ (hex) Nonce (hex) 175d97dc 3,007,383,866, ( 約 3.0T) dc975d f7e7e35b090f5fc858f a62376fe3cc01916ee9 8dfc9f01 Bits 値をデコードしたのがターゲット ターゲットから計算 たしかにハッシュ値 < ターゲット値 困難度 : 条件を満たす nonce を見つけるために必要なハッシュ計算回数の目安

20 参考 : 難易度調整 困難度は 2016 ブロック生成される毎に調整される 約 10 分でブロックが生成されるように調整される つまり約 2 週間毎に難易度調整が発生 2016 x 10min = 20160min = 336hrs = 14days

21 参考 : 通貨単位 ISO 4217: 3 文字の通貨コードを規定 始めの 2 文字 : ISO に規定の国名コード 3 文字目 : イニシャル 例外 : 特定の国に関連付けられていない場合 1 文字目 : X 2-3 文字目 : 短縮名 法定通貨の例 日本円 : JPY 米ドル : USD ISO4217 準拠の例 リップル : XRP ネム : XEM 非準拠の例 ビットコイン : BTC (XBT の呼称もある )

22 プロトコル (3): ブロック追加 Nonce が見つかったらマイナーはそのブロックをチェーンに追加 ブロードキャストする マイナー A マイナー B Block 1002 Coinbas e TX98 TX100 TX100 TX99 TX98 TX100 TX100: Alice -> Bob: 10 BTC Block 1001 クライアント Block 1000 Images from いらすとや

23 プロトコル (4): ブロック検証 ブロックを受け取ったマイナーまたはフルノードはブロックならびに含まれる TXs を検証する フォーマット 署名 (Script による 後述 ) 金額の整合性 (UTXO) 検証が済んだら自身のチェーンにブロックを追加する マイナー A TX100: Alice -> Bob: 10 BTC マイナー B TX100 TX99 クライアント Images from いらすとや

24 TX の検証 : UTXO (Unspent TX Output) TX は input (TXs) と output からなる Input = 誰からもらったコインを使うか Output = 誰にコインをあげるか TX output は spent か unspent である ある TX の input で指定されている TX output は spent であるとよぶ 制約 Input には unspent な TX output (UTXO) しか使えない Output の金額の合計は Input の金額の合計に等しい TX #98: Charlie -> Alice 100BTC Input 1: Output 1: To Alice: 100 BTC おつりは自分に戻す TX #100: Alice -> Bob: 10 BTC Input 1: TX #98-1 Output 1: To Bob: 10 BTC Output 2: To Alice: 90 BTC Input = 100 Output =

25 TX の検証 : UTXO (Unspent TX Output) 正当な TX はコインの所有先を変えるだけ ではコインはどこから生まれるのか? 正しくはこうなっている TX #100: Alice -> Bob: 10 BTC Input 1: TX #98-1 答 : 新規ブロックが生成されるとき そのブロックに採掘報酬 (coinbase) が含まれている そのコインはブロックを生成したマイナーに帰属する これにより系全体のコインが増加 Output 0: To Miner: 12.5 BTC Output 1: To Bob: 10 BTC Output 2: To Alice: 90 BTC Input = 100 Output = Coinbase は 100 ブロック以後に使える

26 参考 : 採掘報酬 (Coinbase) ブロックを作成したマイナーには報酬が支払われる このトランザクションを coinbase とよぶ 1 ブロック 50 BTC から開始 210,000 ブロックごとに半減 ( 現在 12.5 BTC) 0 になったあとはクライアントの払う手数料 (TX fee) のみがマイニングの動機になる BTC の発行総額 6,929,999 番目のブロックが最後 約 2100 万 BTC が発行される 約 132 年かかる見込み

27 UTXO ベースとアカウントベース Bitcoin では 現在の残高 を保持していない この方式を UTXO ベースとよぶ UTXO からわかるから ブロックを作成する際に 最新の状態 を計算する必要はない 一方 一部の Public 型や多くの Permissioned 型の実装では 系の最新の状態 (= world state) をデータベースに保存している これをアカウントベースとよぶ ブロックを作成する際に 最新の状態 を計算する必要がある

28 TX の検証 : Script TX output を費消 (spend) するには 秘密鍵による署名が必要である 必要な署名がそろっていることを Script の実行で検証する Script は TX output および対応する TX input に格納されている これらを連結して実行した結果が true になる場合のみ TX は正当であるとされる Script Forth 言語に似たスタックベース言語 非チューリング完全 これにより単一の署名もしくは複数の署名 ( マルチシグ ) を要求できる

29 チェーンのフォークとコンセンサス (PoW) マイニングとブロックの生成は各マイナーが独立に行うため チェーンが分岐することがある これをフォーク (fork) とよぶ Fork の解消を Bitcoin ではコンセンサスとよぶことが多い コンセンサスには Proof of Work が用いられる マイナー A Block 1002 Block 1001 Block 1003 マイナー B Block 1003 Block 1001 Block 1000 Block と 1003 のどちらが正当?

30 チェーンのフォークとコンセンサス (PoW) Proof of Work での正しい振る舞い : 困難度の和が最大の branch を main とみなし その branch にブロックをつなげていく Main branch からはずれたブロック ( と TXs) は 無かったことになる 要は長い方 マイナー A Block 1002 Block 1004 Block 1003 Block 1002 マイナー A Block 1004 Block 1003 マイニング競争とは main branch を取る競争 ファイナリティがないコンセンサス いま main branch にいるブロックでも いつか main から外れる可能性 51% 問題 : 51% のハッシュパワーで乗っ取り可能 Block 1001 Block 1000 Block 1003, 1004 が届いたとする Block 1001 Block 1000

31 参考 : プロトコル変更に伴うフォーク ソフトフォーク : 後方互換性のあるプロトコル変更 収束 P2SH (Pay to Script Hash) スクリプトの導入 Segwit (Segregated Witness) ハードフォーク : 互換性のないプロトコル変更 分裂 The DAO 事件 ( 後述 ) の結果 : Ethereum v.s. Ethereum Classic ブロックサイズ拡大 : Bitcoin Core v.s. Bitcoin Unlimited

32 Bitcoin まとめ 利点 巧みなインセンティブ設計により Bitcoin に価値があると思うマイナーはまじめに動作するほうが合理的 単に系を破壊したい場合を除く 欠点 電気代の無駄 低速 結託により 51% より小さいハッシュパワーでも乗っ取りできる可能性 (Selfish mining)

33 DLT の実装例 (2): Ethereum Bitcoin をもとにチューリング完全なスマートコントラクトの実行系を組み込ん だ スマートコントラクトの実行に仮想通貨を使う という建付け The DAO 事件を引き起こした 任意の資産を扱える DLTタイプチェーン構造資産 TX 検証タイプ共有コンセンサスファイナリティスマートコントラクト Public 型 線形 コイン (ETH) + 任意 スマートコントラクト アカウントベース 全共有 Proof of Work なし EVM チューリング完全

34 Bitcoin からの変更点 アカウント ( アドレス ) に 2 種類ある EOA (Externally Owned Account): いわゆるユーザアカウント 通貨 Ether (ETH) を保持する Contract: Ether を送信することによってスマートコントラクトを実行できる アカウントベース 現在の各アカウントが所持する ETH および各 contract の内部状態がブロックに格納されている PoW の変種 (Ethash) を採用 ASIC 耐性 : 専用ハードで高速にハッシュ計算することを防止 Proof of Stake (PoS) への移行が計画されている が依然としてすすまない

35 スマートコントラクト Contract EVM で動作 : スタックベースのバイトコード言語 Solidity などの高級言語からコンパイルして実行 実行には gas が必要 ステップごとに減っていく 0 になると実行失敗 Storage とよぶ内部状態 (KVS) を持つ 他アカウントへの ETH 送信ができる 他コントラクトの呼び出しができる デプロイ : コントラクトの送信も TX 実行 コントラクトへ Ether ( と引数 ) を送信 ユーザの指定したレートで Ether が gas に変換される Gas を消費しながら実行 Gas が 0 になったら失敗 実行が終了したら残った gas は Ether に変換され送信者に戻される 消費された gas はマイナーへの報酬になる

36 ブロックの追加 検証 アカウントベースなので マイナーのブロック追加時には 最新の状態 の計算が必要 TX がコントラクトの呼び出しの場合 その計算時に EVM 上のバイトコード実行が行われる その結果に基づきコントラクトの内部状態および各カウントの保持する ETH の更新が行われ 最新ブロックの内容となる

37 Ethereum まとめ 利点 Bitcoin にチューリング完全なスマートコントラクトの処理系を組み込み 多彩な処理が可能になった 欠点 スマートコントラクトの表現力 それらの間の呼び出しが可能であること が相まって操作的意味論が複雑になり 致命的なバグを含みかねない ( 実際に含んだ )

38 The DAO 事件 (The DAO Attack) (2016) Ethereum 上で出資者が非集中的な意思決定を行う DAO の 1 つ 例えば資金の投資先を出資率で多数決して決める DAO: Decentralized Autonomous Organization 1 万人以上から 7M ETH ($150M) 以上を集める 攻撃 2016/6/17 Recursive Call Bug を悪用して DAO Split をループ 6.5M ETH が流出 ハードフォークにより解決 要はなかったことにした Ethereum (ETH) と Ethereum Classic (ETC) への分裂を招いた

39 参考 : The DAO の仕組み スマートロックのベンチャー Slok.it が開発 入金 出資者は The DAO に ETH を出資 The DAO が出資者に DAO トークンを配布 投資 投資先の決定は DAO トークンによる多数決 出金 DAO トークンの引き上げ (Split): 子 DAO に資金 (ETH) を移す という提案を submit 子 DAO からは 28 日後から資金を 引き上げられる Reference: =72171

40 Recursive Call Bug: Parent DAO Object DAO { Map<Object, int> credit int balance Invariant (sum o: credit[o]) = balance Method withdrawall(object o) { 2: if (credit[o] > 0) { // 2.5: credit[o] = 0 3: this.balance -= credit[o] 4: o.pay(credit[o]) 5: credit[o] = 0 } } } 親 DAO this から子 DAO o へ資金を移す移す際に子 DAO の処理が走る 親 DAO:DAO credit[o] o.pay(credit[o]) o: 子 DAO credit[o] From [Grossman+, POPL 18]

41 Recursive Call Bug: Good Child DAO Object DAO { Map<Object, int> credit int balance Invariant (sum o: credit[o]) = balance Method withdrawall(object o) { 2: if (credit[o] > 0) { // 2.5: credit[o] = 0 3: this.balance -= credit[o] 4: o.pay(credit[o]) 5: credit[o] = 0 } } } Object GoodClient { Object Dao int balance Method init(object dao) { 1: this.dao = dao } Method pay(int profit) { 2: this.balance += profit } } お金を受け取ったので内部変数 balance を更新

42 Recursive Call Bug: Bad Child DAO Object DAO { Map<Object, int> credit int balance Invariant (sum o: credit[o]) = balance Method withdrawall(object o) { 2: if (credit[o] > 0) { // 2.5: credit[o] = 0 3: this.balance -= credit[o] 4: o.pay(credit[o]) 5: credit[o] = 0 } } } (2) 呼び返された場合 credit[o] の値はまだ変わっていない! o.pay() をまた呼べる Object Attacker { Object Dao, bool stop, int balance Method init(object dao) { 1: Dao = dao 2: stop = false } Method pay(int profit) { 3: this.balance += profit 4: if (!stop) { 5: stop = true 6: Dao.withdrawAll(this) 7: Dao.withdrawAll(this) 8: } 9: stop = false } } (1) 呼び返す!

43 Recursive Call Bug ここまで大規模な被害になった原因 Recursive call bug の利用 ソース中で transfer() を呼ぶべきところを Transfer() を呼んでいるという typo

44 DLT の実装例 : Hyperledger Fabric v1 ファイナリティを持つ PBFT ベースのコンセンサスを採用 処理並列化のため各機能コンポーネントを分解 MVCC (Multi-version Concurrency Control) による楽観的実行と検証 系の最新の状態 (KVS) を保存している DLTタイプチェーン構造資産 TX 検証タイプ共有コンセンサスファイナリティスマートコントラクト Permissioned 型 線形 任意 スマートコントラクト MVCC アカウントベース 全共有 PBFT 変種 あり Go 言語チューリング完全

45 参考 : Hyperledger Fabric v0.x Hyperledger プロジェクトの Permissioned 型実装の 1 つ ほぼ PBFT [Castro and Liskov 99] に基づいた実装 スケーラビリティ的には不利であった 全ノード間で bloadcast を繰り返すための通信オーバーヘッド TX の実行が linear に行われることによる非並列化オーバーヘッド

46 登場人物 ( いずれも Docker コンテナ ) Endorser TX の simulation を行うノード Committer も兼ねている Commiter Orderer からブロックを受け取って ( それを検証し ) チェーンに追加するノード Orderer TX の順序付けを行い Committer にブロックを配布するノード Client TX の simulation を endorser に依頼して結果を取りまとめ orderer に送るプログラム Endorser Committer Orderer クライアント

47 プロトコル (1) TX の送信と simulation Client は必要な Endorsers に TX proposal を送信し simulation を依頼する Endorser は現在のの状態をもとにスマートコントラクトの実行 (simulation) を行う スマートコントラクト ( チェーンコードとよぶ ) もコンテナ上で動作 実行後 KVS の Read/Write set (RWSet) などを計算し client に返す この時点では KVS の更新は行わない 結果を endorsement とよぶ TX prop 100: transfer(alice, Bob, 10) クライアント Endorser A Endorser B Endorser C Endorsement 100 from A Endorsement 100 from B Endorsement 100 from C Committer Orderer Committer

48 RWSet の計算 KVS の各エントリは (key, value, version) 自然数とみなせる Read set の各エントリは (key, version) Write set の各エントリは (key, new_value) Key Value Version Alice Bob 10 3 Simulates transfer(alice, Bob, 10) Read set: [ (Alice, 5), (Bob, 3) ] Write set: [ (Alice, 90), (Bob, 20) ]

49 プロトコル (2) Orderer での順序付け Endorser A Client は必要なだけの (endorsement policy を満たせるだけの ) endorsement が 集まったら TX にまとめ Orderer に 送信する Orderer は届いた TX を一列に順序付けし いくつかまとめてブロックにする Orderer はブロック (TX) の内容の検証を行わない クライアント Endorser B Endorser C TX 100: transfer(alice, Bob, 10) End. 100 from A End. 100 from B Orderer Block 1000 TX98 TX100 End. 100 from C Committer Committer

50 プロトコル (3) Block の配布とチェーンへの追加 Orderer はブロックを Committer (Endorser 含む ) に配布する Committer は届いたブロック ( と TXs) の検証を行い 検証結果と共にチェーンに追加する TX に含まれる Endorsement が互いに一致しないなら reject フラグを立てる Endorsement が policy を満たさないなら reject フラグを立てる MVCC: Endorsement に含まれる read set のバージョンが現在の KVS のバージョンと一致するなら accept フラグ そうでないなら reject フラグ クライアント Endorse A Endorser B Endorser C Committer D Block 1000 TX98 TX100 Orderer Committer E

51 Endorsement Policy TX が正当であると規定するための endorsement に関する制約を endorsement policy とよぶ Policy はスマートコントラクトの deploy 時に指定する Policy 例 3 個以上の endorsement が必要でそのうち 2 個以上が一致する必要がある 基本的には m-of-n をネストしたもの Policy の設定はビザンチン耐性と密接な関連があるので慎重な設定が必要 ノードが全 4 台 policy を 2-of-3 とすると最大 1 台までの障害ノードを許容するビザンチン耐性を実現できるようにクライアントを設計できる

52 参考 : MSP (Membership Service Provider) Hyperledger Fabric は複数の利害関係者による業務使用を想定している ノードやユーザがある Fabric ネットワークに属しているかどうかを MSP 単位で判定する 例 MSP IBM はノード A, B, C およびユーザ M をメンバとする MSP BOJ はノード D, E およびユーザ N, O をメンバとする Endorsement policy も正しくは MSP を意識した形で書く 例 : 3-of-3(IBM, BOJ, JPX): それぞれの Org からの endorsement が必要で かつ それらがすべて一致する必要がある

53 Hyperledger Fabric v1 まとめ 利点 Permissioned 型ならではの ファイナリティのあるコンセンサス TX simulation の並列化による高パフォーマンス Docker 採用による環境非依存性 欠点 設定の複雑化 High frequency な環境では TX の reject が多発する 匿名性の欠如 (v1.1 で対応予定 ) クライアントのやるべきことが多い

54 DLT の実装例 : R3 Corda 業務アプリケーションで必要なプライバシーの保護に特化 金融アプリを想定 関係者にしか TX を送らない Notary が UTXO 検証 DLT タイプ チェーン構造 資産 Permissioned 型 資産インスタンスごと線形 任意 TX 検証 Notary + スマートコントラクト タイプ 共有 コンセンサス ファイナリティ スマートコントラクト UTXO ベース 一部共有 Notary あり コントラクトコード (on JVM) チューリング完全

55 登場人物 ノード ネットワークを構成するマシン ユーザとほぼ 1:1 ノード Notary ( 公証人 ) TX の二重使用を検証するためのサービス ノード上で動作 Notary KVS

56 参考 : 他の DLT との相違点 (Bitcoin と同じ ) UTXO をもとにした TX 構成 そもそも UTXO とは何であるか? コインの所有先を表す (Bitcoin と異なる ) ただしコイン以外の任意のデータ型を構成できる Corda では state とよぶ (Corda は金融アプリを想定しているので ) なんらかの債権を表すことが多い IOU = I Owe You (Bitcoin と異なる ) TX は関係者としか共有しない (Hyperledger と同じ ) スマートコントラクトの実行結果が決定的でないといけない

57 Corda のデータ構造 State インスタンスに相当対応付けられたコントラクト C State 100 IOU { Lender: Alice Borrower: Bob Amount $100 } Contract: C TX 古い states を input にし 新しい states を output に指定したもの 古い state は unspent でないといけない State 100 IOU { Amount $100 } TX 1000: C.pay($50) State 100 IOU { Amount $50 } Vault いわゆる Spent unspent ふくめ全ての state を保持 State 100 State 100 State 100 あるノードの Vault State 100 State 101 State の最新状態

58 TX 1000: C.pay($50) プロトコル (1): TX の提案 Alice が現状の state を input 更新後の state を output に含む TX を作成する この state は Alice と Bob の間で共有 この state にはコントラクト C が関連付けられているとする TX の Participants を Alice, Bob とする State 100:v3 IOU { From: Alice To: Bob Amount $100 } Contract: C State 101:v2 Cash { Owner: Alice Amount $50 } Contract: C State 100:v4 IOU { From: Alice To: Bob Amount $50 } Contract: C State 101:v3 Cash { Owner: Bob Amount $50 } Contract: C Alice は TX に署名して Bob のみに送信 Alice SigA Bob Vault State 100 v1 State 100 v2 State 100 v3 State 101 v1 State 101 v2

59 TX 1000: C.pay($50) プロトコル (2): TX の検証 Bob は関連付けられた Contract を使って 提案された更新後 state が正しいことを検 証する UTXO 制約も確認する 検証を通ったら Bob は TX に署名をして Alice に送り返す State 100:v3 IOU { From: Alice To: Bob Amount $100 } Contract: C State 101:v2 Cash { Owner: Alice Amount $50 } Contract: C State 100:v4 IOU { From: Alice To: Bob Amount $50 } Contract: C State 101:v3 Cash { Owner: Bob Amount $50 } Contract: C Alice SigA SigB Bob Vault State 100 v1 State 100 v2 State 100 v3 State 101 v1 State 101 v2

60 プロトコル (3): Vault 更新 両者の署名が得られたら TX が確定する Alice と Bob は Vault を更新する State 100:v3 IOU { From: Alice To: Bob Amount $100 } Contract: C State 101:v2 TX 1000: C.pay($50) State 100:v4 IOU { From: Alice To: Bob Amount $50 } Contract: C State 101:v3 Cash { Owner: Alice Amount $50 } Contract: C Cash { Owner: Bob Amount $50 } Contract: C Alice SigA SigB Bob Vault State 100 v1 State 100 v2 State 100 v3 State 100 v4 State 101 v1 State 101 v2 State 101 v3

61 Corda まとめ 利点 業務アプリケーションに特化したプライバシーの実現 他にも ( 省略したが ) オラクルサービスなど 通信量削減とプライバシー保護のための P2P プロトコル ( ブロードキャストしない ) 欠点 資産が多人数の間を渡るにしたがい プライバシーがなくなっていく State の遷移タイミングの厳密な順序関係はわからない P2P プロトコルの欠点をカバーする特権ノードが必要

62 DLT 実装の検証

63 DLT に求められる性質 [Yoshihama and Saito 17] Safety/Consistency 確定したブロックや TX が求められる制約を満たす ( 例 : 二重使用が起こらない ) Authenticity/Non-repudiation ( スマートコントラクト ) 意図しない実行パスを辿らない Liveness ( ファイナリティ ): コンセンサス手続きが完了する Public 型の場合は漸近的ファイナリティ 決定性が重要になることが多い Tamper Resistance: チェーンの改竄耐性 Privacy/Anonymity: 主体者の秘匿 TX 内容の秘匿 TX の存在の秘匿 Resiliency 障害からの復旧がいかになされるかは実運用で非常に重要

64 ( 古典的な ) 否定的結果 FLP 定理 [Fischer, Lynch and Paterson, JACM 85] 各ノードが決定的に動作し 通信が asynchronous ならば 1 台でも faulty なノードがいると合意は実現できない タイムアウトや確率的アルゴリズムで回避 (Brewer の ) CAP 定理 [Gilbert and Lynch, SIGACT News 02] データ複製において Consistency Availability Partition-tolerance の全てを保証することは不可能である DLT 実装では上記条件のいずれかを妥協して実現

65 検証例 : 確率的解析 Selfish mining の解析 [Eyal and Sirer, FC 14] Selfish mining: マイナーが結託し マイニングしたブロックを公開しないまま次のマイニングを続ける 結託側 / その他のハッシュパワー比を α:1-α としてマルコフ過程を構築 条件によっては 1/3 のハッシュパワーで乗っ取れる ほかには [Garay and Kiayias, Eurocrypt 15] など 参考 : 松尾ほか ブロックチェーンの未解決問題

66 検証例 : プログラム / システム検証 I/O オートマトン PBFT (Practical Byzantine Fault Torelance) の定理証明 [Castro+, OSDI 99] 実装を I/O オートマトンで記述 仕様 ( 単一ノードからなるステートマシン ) を I/O オートマトンで書いて simulation を証明 もちろん CSP [Hoare 78] でも CCS [Milner 80] でも π 計算 [Milner 92] でもよい Process キューが v::q なら send(v) 遷移できてキューは q になる キューを q とするといつでも recv(v) 遷移できてキューは q ++ [v] になる send(v) recv(v) 同時に状態遷移 Network Buffer ( 略 )

67 検証例 : プログラム / システム検証 Callback を判定するようなプログラム解析 [Grossman+, POPL 18] コントラクトは 任意の trace から callback を含まない等価な (= 状態を保存する ) trace が構成できるとき Effectively Callback Free (ECF) であるという定義を与えた つまり callback で呼ばれたときの状態がきれいなら callback ありでも ECF といえる コントラクトが ECF であるか否かの決定手続を与えた 1 行目の trace と等価な callback free trace の例 スマートコントラクトの決定性解析 [Iwama+, PPL 18] ( このあとすぐ )

68 検証のためのツール モデル検査 SPIN NuSMV FDR4 Prism UPPAAL 自動だが複雑なモデルを表現しにくい 証明ベース Event-B 仕様記述言語 Coq Agda Isabelle/HOL Lean その他 現状では人手の介入が必要だが複雑なモデル ( 例 : 無限集合など ) が表現可能

69 まとめ ブロックチェーンに代表される分散技術において 実装の形式的な検証は非常に有効である一方 複雑な分散システムを 記述 検証できるための高度な手法やフレームワークが要求される 本会議参加者のみなさまの知見により この分野の研究がさらに進むことを願います

70 参考文献 ( 技術資料 ) Bitcoin Bitcoin Wiki. Bitcoin Project. Bitcoin 日本語情報サイト (2017). ビットコイン解説 > ビットコインとは何か?: 1 漆嶌賢二 (2014). Bitcoin を技術的に理解する : a/ bitcoin Ethereum Ethereum Project. Hyperledger Fabric v1 R3 Corda Corda で認識相違のない取引を.

71 参考文献 ( 論文 ) S. Grossman et al. (2017). Online detection of effectively callback free objects with applications to smart contracts. POPL 2018, Article 48. DOI: 岩間, 立石, 齋藤, 天野, 吉濱 (2018). ブロックチェーンにおけるチェーンコードの決定性の解析. PPL 18. 吉濱佐知子, 齋藤新 (2017). 分散技術におけるインテグリティとプライバシー保護. CSS 17. Wild. J. Garay, A. Kiayias, N. Leonardos (2015). The Bitcoin Backbone Protocol: Analysis and Applications. EUROCRYPT 15. DOI: 6_10. Latest version (2017) appears at I. Eyal, E. Sirer (2014). Majority is Not Enough: Bitcoin Mining is Vulnerable. FC 14. DOI: C. Cachin and M. Vukolić (2017). Blockchain Consensus Protocols in the

72 参考文献 ( 論文 ) (2) S. Nakamoto (2008). Bitcoin: A Peer-to- Peer Electronic Cash System. S. Gilbert and N. Lynch (2002). Brewer's conjecture and the feasibility of consistent, available, partition-tolerant web services. ACM SIGACT News 33 (2). DOI: Practical Byzantine fault tolerance. OSDI 99. M. Fischer, N. Lynch and M. Paterson (1985). Impossibility of distributed consensus with one faulty process. J. ACM 32 (2). DOI: M. Castro and B. Liskov (1999).