DaiLambda, Inc.

slides5

ブロックチェーンの数理と実装

最終回/全5回

DaiLambda, Inc.

Jun FURUSE/古瀨淳

応用数理I,社会数理概論I, Nagoya university, 2023-05-12

Eratta #1

SmartPy はつい最近更新があり、文法が少し変わりました。
授業でやった例や演習をそのまま解くには:

https://legacy.smartpy.io/ide

を使ってください。

スライド中コード例へのリンクURLも修正する必要があります:

https://smartpy.dev/ide?code=...
→ https://legacy.smartpy.io/ide?code=...

スライドの方も書き換えます。

Eratta #2

演習で作ったアカウントはシードフレーズのみから秘密鍵が導出されます。パスワードは秘密鍵を暗号化するものです:

シードフレーズ(=乱数) → 秘密鍵 ⇄ 暗号化されたパスワード

Tezos の別の秘密鍵情報保存方式と混乱していました🙇:

シードフレーズ(=乱数) + パスワード → 秘密鍵

それぞれ、緑色の情報がブラウザに保存されます。
どちらも、秘密鍵そのものをブラウザに保存しないためです。

Eratta #2.5

Trust wallet の脆弱性について

この秘密鍵もシードフレーズのみから導出されます。パスワードは関係ありませんでした:

シードフレーズ(=乱数) → 秘密鍵 ⇄ 暗号化されたパスワード

シードフレーズが \(2^{32}\) 種しかなかったので、秘密鍵を全列挙できるというメチャやばい脆弱性でした。

トピック

ブロックチェーンシステムの安全性

ブロックチェーンの安全性

金銭的価値の貯蔵手段となったブロックチェーン。
バグ、セキュリティーホールは価値の喪失や窃取につながる。

ハッキングによる窃取の被害回復は非常に難しい:

犯人特定が難しい (カストディでの KYC/AML などはあるが)
非中央集権のため、窃取を取り戻すことも難しい
警察もあまり動いてくれない
Code as constitution: 「バグも仕様」という考え方

バグの無い事が非常に求められる。

オープンソースとなる宿命

誰も瑕疵責任を取らない金銭システムを動かしてもらうには、
システム設計図であるソースコードを公開するしかない:

ソースコードを見れば挙動を理解できる
実行プログラムへのコンパイルを各人が行える

実際ほぼ全てのブロックチェーンプロジェクトがノードや
スマートコントラクトの実装コードを公開している。

(実際にコードを読む人はほとんどいないが、読もうと思えば読める、のが大事)

オープンソースの危険性

悪意のある者もソースコードを読める。

金銭的価値を扱うオープンソースコードは攻撃者の格好の標的:

脆弱性を発見し、そこからトークンを盗む
マネーロンダリングなど行えば犯人特定は難しくなる

(ソースコードがなくても脆弱性は探せるが、手間はかかる)

余談: 秘密鍵を盗む方が技術的には簡単…

なんとかして偽ウォレットに誘導し、そこで秘密鍵を入力させる
- 😈「ウォレットに脆弱性がみつかったので、ここで更新して
- 😈「ウォレットの使い方がわからない？教えてあげます
監禁して秘密鍵を強要する。 (別の「技術」が必要)

プログラミングはさほどいらないが、
盗んだ秘密鍵の残高にしかアクセスできない

余談: 基本プロトコルの限界を狙った攻撃

例: 51%攻撃などのプロトコル自体の弱点を突いた攻撃

ブロックチェーンの合意アルゴリズムなどの限界はもとより知られており、「ソースコードの脆弱性」ではない。

ただし、このような攻撃に必要なリソースは非常に高い。

実際にコードの脆弱性をついた窃盗事件例

ほんの一部…

ノード実装の脆弱性: Bitcoin 184B BTC bug
スマートコントラクトの脆弱性: The DAO, Parity, etc.
ウォレットの脆弱性: Trust wallet using MT19937

Bitcoin 184B BTC bug (2010-08)

何者かが Bitcoin の整数オーバーフローの脆弱性を突いて
184B BTC のビットコインを生成。

Bitcoin の設計流通上限は 21M BTC。

対処

ノード実装のバグを直し、この生成命令を取り除く fix を
プロトコルに追加

オーバーフローは怖い…

The DAO (2016-06)

DAO と呼ばれる Ethereum 上の投資プラットフォームが使うスマートコントラクトの Reentrancy 脆弱性が突かれ、コントラクトに預けられていたトークンが盗まれる。

被害額: 3.6M ETH = 当時のETH流通量の 15%、 50M USD。

対処

過去のブロックを改変し、窃盗に関する送金命令を全て取り除く

改竄不可能性を謳っていたブロックチェーンにおける「改竄」に反発したグループが窃盗履歴を保持した Ethereum Classic を作成、分裂(=ハードフォーク)が起こる。

Parity vulnerability #1 (2017-07)

Ethereum で使われている Parity multi-sig ウォレットが使うスマートコントラクトの脆弱性が突かれ、資金が流出する。

被害額: 150K ETH、 32M USD 相当

Parity vulnerability #2 (2017-11)

同じく Parity multi-sig ウォレットのスマートコントラクトが使用するライブラリの所有権が何者かに奪われる。

所有権を握った者がライブラリをブロックチェーンから削除。
スマートコントラクトが動作しなくなり、そこに蓄えられていたトークンを引き出す方法がなくなる。

被害額: 513K ETH, 160M USD 相当

The DAO 事件を上回る被害額だったが、過去の改竄は行われなかった。

なぜライブラリを消せる設計にしたのか…

Trust wallet using MT19937 (2022-11)

シード生成に暗号学的に安全ではない乱数発生アルゴリズム MT19937 を使用。

シードフレーズも \(2^{32}\) 種しかなかった。128GB のメモリがあれば全列挙できてしまう。(本来なら \(2^{256}\) 種)

被害額: 170K USD

対処

ウォレット作成会社が被害額を補填。危険な秘密鍵を有するアカウントから資金を移動するよう広報。

どうやってブロックチェーンを安全にするか

バグ、脆弱性のないシステムを作りたい

正しい道具を使う
安全なデザインを行う
ソフトウェアテスト
バクのないことを検証する

どうやってブロックチェーンを安全にするか

正しい道具を使う

安全なデザインを行う

ソフトウェアテスト

形式検証

正しい道具を使う

Tezos はノード実装に関数型言語OCaml を採用。

プログラミングの中心構成要素から副作用を排除
静的型システムによる型安全性、型推論
異常系を飛ばして書けない
上の良い性質を破る素人は触らない
関数型言語、特に OCaml は形式検証研究の土台としてすぐれており、研究成果にも一日の長がある

副作用の排除(関数型プログラミングスタイル)

純粋関数

数学的な関数と同じく、同じ入力値に対して常に同じ値を返す:

f(v) = v1,　 f(v) = v2 ならば常に v1 = v2

純粋性があると

人間+機械による、プログラムの理解、解析、変換が容易
→ バグが少なくなる

変数への代入や入出力などの副作用があると、
純粋性が破れ、バグが混入しやすくなる。

できるだけ副作用を使わない、使う際にはできるだけ分離するスタイルで書く。 OCaml はこのスタイルがわりと得意。

静的型システム

プログラムやその式を型(int, bool, 関数)で分類する。
辻褄の合ったコードの組み合わせしかできない:
　例: 3 + true はおかしい

型安全性

型のついたプログラムは実行時型エラーを起こさない

型推論

型が書いていないプログラムの型を自動的に推論。

型推論アルゴリズムの完全性: 何かしらの型がつくコードは必ず型推論できる

OCaml には完全に近い型推論があるので、関数定義中ではほとんど型を書かなくてよい。

異常系を飛ばして書けない

Antony Hoare:
「NULL参照は10億ドルにも相当する私の誤りだ。」

正常値と異常値(例: null, undefined, -1)の区別が曖昧なプログラミング言語では、異常系を手当を忘れるバグが多い。

静的型システムのある言語では、しっかり区別をするので異常系を無視することができない:

type ('a, 'err) result =
  | Ok 'a
  | Error 'err (* エラーケースを無視して書けない *)

形式検証

プログラムの挙動が仕様に沿っていることを数理的に証明。

Coq や Isabelle など関数型言語を基礎にした形式検証システムが多く、 OCaml は非常に親和性が良い。 (Coq は OCaml で書かれている)

どうやってブロックチェーンを安全にするか

正しい道具を使う

安全なデザインを行う

ソフトウェアテスト

形式検証

安全なデザインを行う

危険性のあるデザインを排除する

主にスマートコントラクトVMのデザインに関して

スマートコントラクト VM

ブロックチェーンでは、

実行可能な命令セットを安全なものに制限し、
プログラム実行コストに比例したガス課金を行うため

実際のCPUに似せた仮想機械をつかう:

固定長整数 (16, 32, 64bit 整数、 etc)
→ オーバーフローの可能性 (ex. 184B BTC bug, BEC contract bug)
単純なデータ構造しかない (整数、バイト列くらい)
→ 複雑なデータ構造(list や map など)のライブラリを構築する必要
→ バグ (ex. Parity 脆弱性)
副作用ありあり
異常系対処が強制されない (null と整数を混ぜて使うなど)

ꜩ Michelson VM

仮想機械だが、高級言語的な安全性機能を搭載:

可変長整数: 固定長整数は存在しないので、オーバーフローがない。
タプル、リスト, map などのコンテナ型を VM レベルで用意
純粋関数型。副作用はない
静的型システム
Option型 (Some x or None) や result型 (Ok x or Error e) があり、異常系の処理を忘れることができない

最終的な実行プログラムの安全性を検証しやすい。

ꜩ Michelson VM

Michelson は種々の安全性機構が入っているので、
人の手でも書けない、ことはない。

多くのバグが書けない & 型検査により事前に検出できる。

高級言語から Michelson へのコンパイラ作成も容易:

コンパイラに問題があれば、まず生成 Michelson コードの型検査が通らない

他のブロックチェーンでは…

Ethereum で使われている EVM は Michelson に比べれば CPU にかなり近い。

高級言語と、そのコンパイラの方で安全性を担保。

ただし、最終的な実行対象である EVM は副作用をたくさん使うため、検証が難しい。

The DAO 事件の Reentrancy バグ

スマートコントラクト特有の脆弱性なので紹介する

The DAO 事件の Reentrancy バグ

The DAO は銀行のような Ethereum コントラクト

// SENDER: 送金者  AMOUNT: 送金額
contract bank {
  deposit() // 振込
  {
    map[SENDER] += AMOUNT; // 振込額を残高に足す
  }

  withdraw() // 引出
  {
    send(SENDER%default, map[SENDER]); // 全残高を返金
    map[SENDER] = 0; // 残高を0に
  }
}

ここに脆弱性が…

Reentrancy バグを突く

withdraw() からの返金を受けたら呼び戻すコントラクト

contract bank { // 銀行コントラクト
  deposit()
  {
    map[SENDER] += AMOUNT;
  }

  withdraw()
  {
    send(SENDER%default, map[SENDER]);
    map[SENDER] = 0;
  }
}

contract attacker { // 攻撃コントラクト
  do_deposit() // 振込
  {
    send(bank%deposit, 10);
  }

  default() // 攻撃
  {
    // 呼び戻す
    send(bank%withdraw, 0);
  }
}

attacker.do_deposit() で bank.map[SENDER] を 10 に
attacker.default() を使うと bank.withdraw() が 10 送金
残高情報 bank.map[SENDER] は 10 のまま!
1. に戻る。bank からどんどん資金を吸い取れる。

ちゃんと Reentrancy バグを突く

実際には、無限ループになると bank の残金が 0 になったり、
ガス欠になり、攻撃は失敗する。ループ回数を有限にする必要:

contract bank { // 銀行コントラクト
  deposit()
  {
    map[SENDER] += AMOUNT;
  }

  withdraw()
  {
    send(SENDER%default, map[SENDER]);
    map[SENDER] = 0;
  }
}

contract attacker { // 攻撃コントラクト
  do_deposit() // 振込
  {
    send(bank%deposit, 10);
  }

  default() // 攻撃
  {
    // 自分の残高が大きくなったらやめる
    if (BALANCE < 100) {
      send(bank%withdraw, 0);
    }      
  }
}

相変わらず bank.map[SENDER] は 10のまま。

攻撃対象コントラクトに実行を戻すので “Reentrancy bug”。

Reentrancy 脆弱性の本質

なぜ脆弱になったか?

プログラムが満たすべき不変条件:

map[SENDER] + SENDERへの送金額が一定

が壊れた状態で悪意あるプログラムに実行を移してしまった:

withdraw()
{
  send(SENDER%default, map[SENDER]); // 不変条件が壊れたまま実行が移る
  map[SENDER] = 0;
}

Reentrancy バグの修正

プログラムが満たすべき不変条件:

map[SENDER] + SENDERへの送金額が一定

が成り立っている時にのみ外部プログラムに実行を移す:

// 修正バージョン。 map[SENDER] の更新を送金の前に行う
withdraw()
{
  amount = map[SENDER];
  map[SENDER] = 0; // ここでいったん不変条件は壊れる
  send(SENDER%default, amount); // 不変条件が回復してから実行が移る
}

不変条件の抽出と検証

プログラム実行が外部コントラクトに移る時に不変条件が成り立っていることは、プログラム検証を行うことで確認できる。

ただし、プログラムの仕様 = 満たすべき不変条件を不足なく発見するのは難しい…

先ほどの:

map[SENDER] + SENDERへの送金額が一定

も銀行だから成り立つ条件。機械が自動的に探してくれるものではない。 → 形式検証の難しさ。

Reentrancy bug をなくすのは難しい

Reentrancy 問題は広く知られている…
にもかかわらず、今でも発生する。

2022-11: Uniswap reentrancy vulnerability: Ethereum 上の分散取引所 Uniswap が使っているコードに reentrancy 脆弱性が発見される。
バグ報奨金制度を通した報告のため、被害はなし。

そもそも Reentrancy が起きないようにする #1

返金先をスマートコントラクトを持たないアカウントに限定すれば reentrancy は起こらない。

ꜩ Tezos の場合、

スマートコントラクトのないアカウント tz[123]* と
スマートコントラクト KT1*

は簡単に判別できる。特に KT1* は SENDER になれない。

ただし、入金元がスマートコントラクトである場合、預け入れられた資金は返金できなくなるので、入金も同様に制限する必要がある。 → 制限としてはキツすぎる場合がある。

そもそも Reentrancy が起きないようにする #2

コントラクト実行の最中に、他コントラクトコードを実行しなければ、「一時的な不変条件の壊れ」による問題を回避できる。

ꜩ Tezos では、send() による送金先コードの実行はその場ではなく、現コードの実行終了後:

  withdraw()
  {
    op = send(SENDER%default, map[SENDER]); // ここでは送金命令を作るだけ
    map[SENDER] = 0;
    return op; // エントリポイント実行終了後、送金命令を実行する
  }

他コントラクトの関数的な呼び出し方ができなくなるので、
スマートコントラクトの書き方が難しくはなる。

どうやってブロックチェーンを安全にするか

正しい道具を使う

安全なデザインを行う

ソフトウェアテスト

形式検証

ソフトウェアテスト

ソフトウェアの全部一部を動かして期待した動作を行うか確かめる。

ユニットテスト: 関数単位などの小さいコンポネントのテスト
結合テスト: ユニットを組み合わせたテスト
システムテスト: ソフトウェアシステム全体のテスト

テストは技術的には難しくない。地道にやっていく。

Fuzzing

ランダムに生成した入力データや、既存の入力データを改変したものをプログラムに与え、誤動作やクラッシュしないかをテストする

Tezos での例: ノンネイティブトークンを実装するスマートコントラクトが規格に合致しているかをテスト

QuickCheck

関数型言語 Haskell で発達してきたプロパティテスト手法

プロパティテスト:プログラムが指定した性質(プロパティ)を満たすかどうかを調べるテスト。

Generator: 関数への入力値を型定義情報から自動生成してくれる
Shrink: プロパティを満たさない反例となる入力例を見つけた場合、その反例からさらに小さい反例を探す。
　例: [3; 5; 7; 11] というリストが反例となる場合、その部分リスト　　　である [3] や [5; 7]も判例になっていないか試す
小さい反例だと原因を探しやすい
Tezos での例: ノード実装の至る所で使われている

Mutation テスト

プログラムの一部を意図的に改変し、意図的にバグが埋め込まれた状態を作る。

この「バグ」が現在のテストケースによって発見されるかを
チェックする。

どのテストケースも「バグ」で失敗しなかった場合、改変場所に対するテストが甘いことがわかる。

Tezos での例: スマートコントラクト実装のテストケースの評価

ソフトウェアテストの限界

色々とテクニックはあるが、テストはプログラムを与えられた条件下で動かしてうまくいくかを見る。

やるべき

難しくはないのでどんどんやるべき。

完璧ではない

有限のケースでしか試せない。
テストされていないケースは無保証

どうやってブロックチェーンを安全にするか

正しい道具を使う

安全なデザインを行う

ソフトウェアテスト

形式検証

形式検証

数理的にプログラムが好ましい性質を持っている(or いない)ことを証明する。

テストとは違い、証明できれば絶対の安全を保証できる。
証明は一般的に難しい。

形式検証をブロックチェーンへ

産業的には、形式検証はクリティカルシステムに使われてきた:

航空宇宙産業
原子力発電

ブロックチェーンもクリティカルシステム。形式検証して安全性を保証していきたい。

形式検証のいろいろ

モデル検査
静的型システムを使った検証
定理証明支援系

モデル検査

プログラムを有限状態遷移系としてモデル化し、モデルが検証したい性質を満たすかを自動的に検証する。

利点: 自動
欠点: 効率の良いモデル化が難しい

Tezos とモデル検査

Tenderbake: 現在の Tezos 合意アルゴリズム

BFT 合意に基づく確定的 finality を持つアルゴリズム
(Nakamoto アルゴリズムは確率的 finality)

Tenderbake には正しさの手証明はある。

モデル検査による Tenderbake の正しさの検証

形式使用言語 TLA+ を使った Tenderbake のモデル化

Tezos ネットワークに参加したばかりのノードが正しく現在のネットワークのブロックチェーン状態に追いつくことが検証されている。

静的型システムを使った検証

プログラム中の値が持つ性質を型で表し、値の組み合わせを適合する型の間のみに強制、プログラム全体の性質を保証する。

OCaml のようなレベルの型システムは:

大したことは検証できない
ただ、強力な型推論があるので非常に便利

より複雑な型システムを使い、プログラムの安全性検証を行う

依存型(dependent type)

依存型では型情報に値を導入し、複雑な性質を表現、保証
(Coq, F*, Agda など)

(* 通常の ML *)
(* リストの先頭要素を返す。空リストでは失敗する *)
hd : 'a list -> 'a

(* リストの結合 *)
append : 'a list -> 'a list -> 'a list

型の中に値を書ける ('a, n) list : 長さ \(n\) のリスト

(* 非空リストしか受け取らない *)
hd : ('a, succ n) list -> 'a

(* リストの結合。結果の長さは引数の長さの和 *)
append : ('a, n) list -> ('a, m) list -> ('a, n+m) list

篩型(refinement type)

篩型システムでは型に条件式を書くことができる。 (LiquidHaskell など)

(* 通常の ML *)
(* リストの先頭要素を返す。空リストでは失敗する *)
hd : 'a list -> 'a

(* リストの結合 *)
append : 'a list -> 'a list -> 'a list

篩型では集合の内包表記 { 変数 : MLの型 | 条件式 }
で型の条件を書ける:

(* 非空リストしか受け取らない *)
hd : {x: 'a list | length x > 0} -> 'a

(* リストの結合。結果の長さは引数の長さの和 *)
append :
  {x : 'a list} -> {y : 'a list} -> 
  {z : 'a list | length z = length x + length y }

複雑な型の検査

依存型や篩型を使えば、プログラムが与えられた仕様を満たすことを検証できる。

ただし、型推論、型検査は難しい。

定理証明系

依存型を使った数学の証明システム。例: Coq

証明を人間が書くための言語を提供

SMTソルバを使った検査

解くべき問題を一階述語論理式の充足可能性問題に変え、 SMTソルバを使って解く。例: F*, LiquidHaskell

Tezos スマートコントラクトの検証

検証活動が一番盛ん

参入障壁が低く、質の悪いコードがあると思われる
ブロックチェーンの他の構成要素と比較して、プログラムは非常に短い

ハックしやすく、検証しやすい

Mi-Cho-Coq

Michelson の Coq モデル。

Michelson のプログラムを Coq 中で自然に書ける。
評価器による Michelson の動作(=意味論)の定義。

これらを使って Michelson プログラムの性質を証明できる

例: boomerang

Boomerang コントラクト (Michelson)

parameter unit;
storage unit;
code
  {
    CDR;
    NIL operation;
    AMOUNT;
    PUSH mutez 0;
    IFCMPEQ
      {
      }
      {
        SOURCE;
        CONTRACT unit;
        ASSERT_SOME;
        AMOUNT;
        UNIT;
        TRANSFER_TOKENS;
        CONS;
      };
    PAIR;
  }

Boomerang コントラクト (SmartPy)

# https://legacy.smartpy.io/ide を使ってください
import smartpy as sp

class MyContract(sp.Contract):
  def __init__(self):
    self.init()

  @sp.entry_point
  def default(self):
    sp.if (sp.amount == sp.tez(0)):
      pass
    sp.else:
      sp.send(sp.source, sp.amount)
    
@sp.add_test(name = "MyTest")
def test():
  alice = sp.test_account("Alice")
  scenario = sp.test_scenario()
  contract = MyContract()
  scenario += contract
  scenario += contract.default().run(source = alice.address, amount = sp.tez(100))

ConCert

Coq でスマートコントラクトを書き、Michelson にコンパイル

Mi-Cho-Coq と違って高級言語で書ける
Coq のレベルでプログラムの証明が書ける

コントラクト相互作用テストが可能

スマートコントラクトは一回呼び出されて終わり、ではなく、storage が更新され、繰り返し呼び出される
QuickChick を使ったプロパティテストを提供

Helmholtz

Michelson + 篩型。

Michelson コードに篩型を書くことができる。
SMT ソルバ Z3 による自動検証

これらを使って Michelson プログラムの性質を証明できる

例: booemrang

Archetype

コントラクトの不変条件や事後条件を記述できるコード例

トークン実装での条件例:

# トータル発行量は変化しない:
specification {
  s1: ledger.sum(tokens) = totalsupply;
}

#自分自身に送金する場合、状態は変わらない
postcondition transfer_p3 {
    %from = %to -> ledger = before.ledger
  }

これらの証明すべき条件を証明支援系 Why3を通して抽出し、自動証明や定理証明系で証明する。

コンパイラの正しさの証明(をしたい)

高級言語で書かれたコントラクトを高級言語上で検証しても、
コンパイラが腐っていては意味がない

高級言語から Michelson へのコンパイラ LIGO の正しさの研究

さすがに時間がかかりそう…

(形式検証による正しさ証明とは比べるべくもないが、
コンパイラ実装が間違っていると出力 Michelson の型エラーとして現れることが多い。その点は楽。)

スマートコントラクトの検証: まとめ

いろいろ道具立てがある。

コントラクト単体の機能の正しさの証明はやればできる
(ただし技能が必要…)
これからは複数のコントラクト間のやりとりでの安全性証明 (ex. Reentrancy 問題)

形式検証の課題

証明する仕様が抜けていれば…証明されない!!†,†,†

細かい仕様を網羅することは難しい
ざっくりとした仕様からヤバそうなモノを見つけて欲しい
(そんなことできるのか)

Tezos ノード実装の検証

暗号ライブラリ HACL\(*\)

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 に分け、幅をそろえる