Scaling Bitcoin 2019のスケジュールが公開されたので、予習シリーズを開始!
第一弾は「Developing secure Bitcoin contracts with BitML」のペーパーの内容↓
https://arxiv.org/pdf/1905.07639.pdf
スマートコントラクトの開発用ツールはEthereum方面は充実してるけど、Bitcoinに関してはほとんど無い。まぁ単純な決済をやマルチシグくらいであれば基本的に構成するコントラクトのスクリプトの型が決まっているため、一度スクリプトを構成してしまえば後はパラメータを変更するだけというのもあるかもしれないけど、もっと複雑な金融サービスなどを構成しようとするとコントラクトの開発環境および形式証明などを含むその検証環境は重要だ。特に、現在提案されているOP_SECURETHEBAG
などでCovenantsを実装できる=有限状態マシンを実装できるようになると、その必要性は一層増す。
BitcoinでもPieter WuilleがMiniscriptというBitcoin Scriptを対象にしたDSLを発表したが、まだ正式にBIP化および仕様化はされていない。
↑のホワイトペーパーでは、Bitcoinのスマートコントラクトを開発および検証するために作ったBitMLベースのツールチェーンが紹介されている。
BitML
BitML(Bitcoin Modeling Language)はBitcoinのスマートコントラクト用のDSLでBitcoinトランザクションにコンパイルされる(そういう意味だとMiniscriptと同じレイヤーのプロダクト)。
https://eprint.iacr.org/2018/122.pdf
このツールチェーンは以下で構成される。
- BitMLコントラクトを開発するためのIDE。
- BitMLコントラクトを標準的なBitcoinトランザクションに変換するためのコンパイラ。
- BitMLコントラクトの安全性(資金がコントラクト内で凍結されることがない流動性の担保など)を検証するためのモデルチェッカーとカスタムLTLプロパティ。モデルチェッカーはMaudeをベースにしている。
セットアップ
IDEはDrRacketというSchemeから派生したプログラミング言語Racketの開発環境を使うみたいで、以下で一緒にインストールされる。
$ git clone https://github.com/bitml-lang/bitml-compiler.git $ cd bitml-compiler $./install.sh ...
インストールが完了すると、
$ drracket
を実行するとIDEが起動する↓ので、フィアルの先頭に#lang bitml
を宣言し、BitMLを記述する。
コントラクトの記述
BitMLのシンタックスはホワイトペーパーに記載されている↓
https://eprint.iacr.org/2018/122.pdf
例えば参加者A,BがいてAがBに BTC送金するコントラクトは以下のように記述できる。
#lang bitml ; コントラクトの参加者を宣言 (participant "A" "029c5f6f5ef0095f547799cb7861488b9f4282140d59a6289fbc90c70209c1cced") (participant "B" "0316589526daa876ef27937e48176da08fc95eaef7315fa20a07114d5fb8866553") (debug-mode) ; Aが1BTCをBに送る場合、Aはまず1BTC所有するトランザクションを宣言する。 ; tx:の後がシリアライズしたトランザクションで、その後の@1がアウトプットのインデックス (define (txA) "tx:02000000000102f28b8ec15a48abd9cda80d1c770ff9770dc0c549ddb1b8013b9e50a8799614aa000000001716001412a88716720982b693ab2bd2a2fcd4d98bdd2485feffffff08d59c3aeafd6003e6e099adde64f17d6ec7950619c22b50466281afa782e9d4000000001716001433845a8590dbf145b52bdd777103d1ddfdaa9cedfeffffff022fac1f000000000017a914e9f772646a0b6174c936806dab1b882e750ac04a8740420f00000000001976a914ded135b86a7ff97aece531c8b97dc8a3cb3ddc7488ac02473044022060135384eafe9a8021e8b8c46da20e7cd5713d581c3f79b1da3d2f7860a1bfed02206ca1ac1616d7ab778bcbb235b4b24286c2181ec171b8cadeaa9ee5f4f78fd330012102d5f8f263a81427330e7f26ba5832a2cd01e960bf145be2101bc0b6bb0fde8c2d0247304402200e02da2228774b47ff03a5a7c1bf1d070d0cec6cd9a08d6862e1855ba33dfb9f0220011511f10aaefbf402b2944b6a877c1ff9890a7fc3e266bbb74318b4540c555d012103ef2a573fbd46356dcbdbedcecc9aa25dcb500512e2be394297475ed157a9cfc6bdb51600@1") ; Aが1BTC送金するコントラクト (contract (pre (deposit "A" 0.001 (ref (txA)))) (withdraw "B"))
他にも、AがBTCをデポジットし、チェーンのブロック高が500000を超えるとBが引き出せるが、510000を超えるまでにBが引き出さない場合、Aがコインを引き出すことができるというコントラクトは以下のように書ける。
... ; ブロック高の宣言 (define (t) 500000) (define (t1) 510000) (contract (pre (deposit "A" 0.001 (ref (txA)))) (choice (after (ref (t)) (withdraw "B")) (after (ref (t1)) (withdraw "A"))))
コントラクトのコンパイル
DrRacketのエディタの右上の実行ボタンを押すと、以下のようにBalzacで表現されるコントラクトのトランザクションを含むコンパイル結果が表示される。Balzacというのは、A formal model of Bitcoin transactionsの形式モデルに基いたBitcoinトランザクションの抽象化層とのこと。
さらにBalzacのコードから標準的なBitcoinトランザクションに変換する必要がある。この変換は、Balzac Webエディタを使ってできる。
試しに↑のDrRacketが吐いたコードをコピペしてEvaluateすると、Tinitの署名が提供できないのでワーニングになる。これは、
const privkeyA = key:cUnBMKCcvtpuVcfWajJBEF9uQaeNJmcRM6Vasw1vj3ZkiaoAGEuH
を宣言して、以下のように署名生成に使うようにすればいい。
tx:02000000000101adbcf28818d2556fb85ce7f6068775a6a4fd4befe650d3d7d120b609e5af1e920100000017160014a5d12120913a41cdd3be9ef88b60838b8c0db3b7feffffff028ac710000000000017a914664180e7578033f9cef5bc82b3112855f775f02587a0860100000000001976a914ded135b86a7ff97aece531c8b97dc8a3cb3ddc7488ac024730440220290f9526ed5e22d4ae72c66702f5f70dff4c5ea72445cd20112782da1986332e02201d872a0a53fa13b34a9273776dfcd0ea7385e449fec1e95263bdde96fda084e10121021215eb7fabd9bb0c1f1441bf35bade28d9e64dc798a666eb4eaf47e134a7 4b446d191700@1:sig(privkeyA)
さらに最終行に
eval Tinit
を追加してEvaluateすると、Tinitの変換結果=BitcoinトランザクションのRAWフォーマットが出力される。
Tinit Transaction{1e5dfc19ba826704611bfa844e3fb4fbdc00f5f4ef79dc87424913197e2437f9 weight: 756 wu, 189 bytes version 2 purpose: UNKNOWN in PUSHDATA(71)[3044022017446454e5719b15716028375b83e2bd5e504b32f3196e3de18c5dc652bc2c120220558dc80643ce0c8b5d6ca80fccd771c54c9b8d3352f4ceec58e27517474a495d01] PUSHDATA(33)[0339bd7fade9167e09681d68c5fc80b72166fe55bbb84211fd12bde1d57247fbe1] P2PKH addr:n1q6vo5VabL1BpqVKyHjvh4vaHrAq5NcYR outpoint:2e647d8566f00a08d276488db4f4e2d9f82dd82ef161c2078963d8deb2965e35:1 out HASH160 PUSHDATA(20)[0711461f84331f5de08e04f9d5e36307b52eb6c7] EQUAL 0.001 BTC P2SH addr:2MstbQqerozS9oHt8cpL7rZjKcnVchSxEiU } 0200000001355e96b2ded8638907c261f12ed82df8d9e2f4b48d4876d2080af066857d642e010000006a473044022017446454e5719b15716028375b83e2bd5e504b32f3196e3de18c5dc652bc2c120220558dc80643ce0c8b5d6ca80fccd771c54c9b8d3352f4ceec58e27517474a495d01210339bd7fade9167e09681d68c5fc80b72166fe55bbb84211fd12bde1d57247fbe1ffffffff01a08601000000000017a9140711461f84331f5de08e04f9d5e36307b52eb6c78700000000
コントラクトの検証
続いて、BitMLコントラクトの検証について。現在以下の検証をサポートしている。
流動性の検証
コントラクトの実行にあたって、必ず資金がいずれかの参加者に渡ることが重要で、誰も入手できない条件があると資金が永遠に凍結されてしまう。
コントラクトの条件によらず、全てのパータンを考慮した上で、資金の流動性をチェックしたい場合、コントラクトの最後に(check-liquid)
を追加する。
(contract ... (check-liquid))
もし、コインの流動性が損なわれる場合、出力ボックスにその旨表示される。
その他、以下のように参加者の戦略毎に流動性のチェックをすることもできる。
(contract ... (choice (reveal (a) (withdraw "A")) (auth "B" (after 700000 (withdraw "B")))) (check-liquid (strategy "A" (do-reveal a))) (check-liquid (strategy "B" (do-auth (auth "B" (after 700000 (withdraw "B")))))))
LTL特性の検証
BitMLでは流動性の検証以外に、(check-query "query")
を使って、コントラクトに合わせてカスタマイズされたカスタムLTLプロパティを検証できる。
例えば時間制限のついたコミットメントの場合、以下のような検証ができる。
- Aがシークレットを明らかにした場合、Aのデポジットを取り戻すというチェックは以下のように書ける。
(check-query "[]<> (a revealed => A has-deposit>= 100000000 satoshi)")
- Bがシークレットを知る or Bがデポジットの資金を得るという条件のチェックは、以下のように書ける。
(check-query "[]<> (a revealed \/ B has-deposit>= 100000000 satoshi)"))
課題
今までBitcoin Scriptで作るスマートコントラクト用の開発ツールや形式証明ツールなどはほとんどなかったので、このレベルのプロダクトが出てきてるのは素晴らしい。ただ、現在どんなコントラクトでも書けるという訳ではなく、以下のような制約があるようだ。
- BitMLは完全にBitcoinに対応しているわけではなく、Bitcoin Scriptを直に書けば書けるコントラクトがBitMLでは書けないものがある。
- サポートする署名タイプは
SIGHASH_ALL
のみで、その他の署名タイプはサポートできていない。 - オフチェーンのやりとりは、シークレットの公開と承認のみを限定的にサポート。
- 動的に定義される参加者のセット(クラウドファウンディング)や、無制限の反復(マイクロペイメントチャネル)などは現状BitMLで表現できない。
- サポートする署名タイプは
- 実際に使ってみると、Balzacの知識も必要となるので、まだお手軽開発環境という状態ではなさげ。ある程度熟知して、使いこなす必要がある。
さらに、Covenantsなどが有効になるとトランザクションを跨いだ状態マシンの管理などが求められるようになると思うので、今後の発展に期待したいところ。
BitMLについては以下のサイトが参考になる。
BitML Toolchain — BitML 2019-07-23_054007 documentation
以下、ホワイトペーパーの意訳↓
Abstract
Bitcoinで実行できるスマートコントラクトを開発および検証するためのツールチェーンを紹介する。このツールチェーンは、計算上健全なBitcoinに組み込まれたスマートコントラクト用の最近のDSLであるBitMLをベースにしている。このツールチェーンは自動的にコントラクトの関係性を検証し、資金が永久にコントラクト内で凍結されたままになるようなことがないことを保証する。BitMLコントラクトを標準のBitcoinトランザクションに変換するためのコンパイラも提供される。コントラクトの実行はこれらのトランザクションをブロックチェーンに追加することに相当する。我々は代表的なコントラクトのベンチマークを通して、このツールチェーンを評価する。
1. イントロダクション
過去5年間で、Bitcoinを悪用してスマートコントラクトを実行する方法、つまり事前に合意された複雑なルールに従って暗号通貨を交換することを可能にするコンピュータープロトコルについて多くの優れた研究が行われてきた。これらの研究によって確認された多種多様なユースケースにも関わらず、Bitcoinのコントラクトの開発を容易にするためのツールサポートはまだ提供されていない。現在、このタスクでは標準的な暗号プリミティブを使用する他に、Bitcoinのブロックチェーン上のトランザクションを読み取り、追加できる複雑なプロトコルを考案する必要がある。新しいプロトコルを作るにあたっては、その正当性と安全性を確立するためにかなりの努力を必要とする。これはエラーを起こしやすいタスクで、通常手動で実行され、一部のコーナーケースを見逃す可能性がある。これらのプロトコルで使われるトランザクションの作成も同様に面倒で、十分にドキュメント化されていないBitcoinの機能(スタックベースのスクリプト言語など)と戦う必要がある。
本稿では、Bitcoinへの計算的に健全な埋め込みおよび関連するトレース特性の健全で完全な検証技術を特徴とするスマートコントラクト用の最近の高水準言語であるBitMLについて考察する。BitMLはPrinciples of Security and TrustやFun with Bitcoin Smart Contractsに記載されているスマートコントラクトの多くを表現し、適切なトランザクションをブロックチェーンに追加することでそれらを実行する。埋め込みの計算上の健全性は、たとえ敵対者が存在したとしても、BitMLのセマンティクスのレベルでセキュリティ特性がBitcoinのトランザクションレベルで維持されることを保証する。まだコントラクトを開発しBitcoinのブロックチェーンにデプロイするためのツールは存在しないため、BitMLは理論上の限界にある。
貢献
この研究では、BitMLコントラクトを書き、検証し、それらをBitcoinデプロイするためのツールチェーンを開発する。より具体的には主な貢献は次のようになる:
- BitMLはRacketに埋め込む。Racketは、BitMLコントラクトをDrRacket IDE内でプログラミングできるようにするもの。
- BitMLコントラクトの任意のLTL特性をチェックできるセキュリティアナライザー。特に分析は流動性、つまりコントラクトないの資金が永久に凍結されたままではないことを要求するスマートコントラクトのランドマーク特性を決定することができる。
- BitMLから標準的なBitcoinトランザクションへのコンパイラ。計算上の健全性の結果は、コンパイルされたコントラクトに対する攻撃もBitMLレベルで観察可能であることを保証する。したがって、セキュリティアナライザーによって検証された特性は、コンパイルされたコントラクトにも当てはまる。
- ツールチェーンを評価するためのベンチマークとして使用するBitMLコントラクトのコレクション。コレクションには、Bitcoin用に開発された最も複雑なコントラクト、金融サービス、オークション、期限付きコミットメント、宝くじ、その他の様々なギャンブルゲームなどの一部が含まれている。ベンチマークを使用して、スマートコントラクトプラットフォームとしてのBitcoinの表現力と限界について説明する。
ツールチェーンのアーキテクチャをFigure 1に示す。開発のワークフローは以下の通り。
- BitMLコントラクトを書き、必要なプロパティを指定する。オプションで参加者の戦略にいくつかの制約をし正直な参加者の行動を部分的に定義する。
- セキュリティアナライザーを通して、コントラクトが要求された特性を満たすことを検証する。
- Bitcoinトランザクションへコンパイルする。
- 選択された戦略に従ってトランザクションをBitcoinブロックチェーンに追加することで、コントラクトを実行する。
最後のステップは、拡張やカスタマイズを必要とせずBitcoinのmainnet上で実行できることに注意すること。
ツールチェーンの全てのコンポーネントはオープンソースであり、ベンチマークのコントラクトもである。チュートリアルはオンラインで利用可能で、そこにはBitcoinのtestnet上の我々の実行への参照も含む。
2. Bitcoin Contractの設計
BitMLのコントラクトでは、2人以上の参加者が特定のロジックに従って彼らのBitcoin(B)を交換できる。コントラクトは
という2つの部分で構成される。ここではBitMLの文法やセマンティクスを提供するのではなく、単純だがパラダイム的な例である相互のタイミングコミットメントコントラクトを通してそれを説明する。このコントラクトには2人の参加者(AとB)がそれぞれ1つのシークレットを選択し、一定量の暗号通貨(1Bなど)のデポジットを含む。コントラクトの目標は、各参加者は他の参加者のシークレットを知るか、そうでなければ他の三社かのデポジットを保証として受け取ることだ。コントラクトは参加者に彼らのシークレットを明らかにするための時間を与える。参加者がそれに間に合って、そのシークレットを明らかにした場合、その参加者自分のデポジットを取り戻すことができ、そうでなければ、時間切れになった後、他の参加者はそのデポジットを引き出すことができる。
我々のツールでは、このコントラクトを以下のように指定する。
最初の2行は、参加者の公開鍵を指定して参加者名のエイリアスを作成する。コントラクトの前提条件は、前編にあり、各参加者はトランザクションアウトプットの識別子とシークレットのハッシュを指定しなければならない。トランザクションアウトプットは未使用でなければならず、必要な1Bを持ち、参加者の秘密鍵を使って償還可能でなければならない。ハッシュはコントラクトの実行中に使用される。参加者が選択したシークレットであると主張する値を提供した際、この値のハッシュは前提条件のハッシュと等しくなければならない。
コントラクトロジックは、前提条件の後に指定される。トップレベルの選択では、2つの代替ブランチを定義する。Aがシークレットを明らかにした場合のみ最初のブランチを選択することができる。これが実行される場合、コントラクトは最も内側のものが続く。2つめのブランチは、高さ100,000のブロックとして指定されたタイムアウト後のみ選択でき、その場合Bはコントラクト内の資金すべて(すなわち2B)を引き出すことができる。そのため、Aはデポジットした資金を失うのを避けるため、間に合うようにシークレットを明らかにするよう動機づけられる。同様に最も内側の選択は高さ100,050ブロックまでにBにシークレットを明らかにする動機づけをするのに使われる。Bがシークレットを明らかにした場合、分岐したサブコントラクトが実行され、これによりコントラクトの残高がそれぞれ1Bの2つに分割され、参加者は自分のデポジットを引き出すことができる。
この言語はBitML構文構造をRacketコードに書き換えるのに使用されるRacketマクロシステムを利用して定義されている。このアプローチはRacket言語のエコシステムから利益を得て、我々がDrRacket IDEでBitMLコントラクトを書けるようにする。実際我々のツールチェーンはDrRacket IDEの中に、コントラクトのエディター、セキュリティアナライザーおよびBitMLコンパイラを統合している。RacketでのBitMLの実装は言語を実際に使えるようにするため理想的なバージョンのBitMLを拡張したものだ。例えば、自動的にコンパイラによって得られた全てのトランザクションにスプレッドするタイプ手数料の特別なデポジットなどを導入している。またコントラクトの正しい執行を妨げる可能性があるいくつかのエラーに対して静的チェックも実装している。例えば、同じハッシュを持つシークレットをコミットしたり、トランザクションアウトプットの二重使用など。
BitMLコントラクトの検証
このツールは、さまざまな形態の流動性を検証し、コントラクト内で資金(もしくは一定額までの資金)が永久に凍結されることが内容にする。さらに、ツールは任意のLTL式を検証することができ、この状態述語は、例えば、参加者に寄って所有される資金、提供される認可および明らかにされたシークレットを指定することができる。デフォルトでは、ツールは書く参加者の考えられる全ての動作に対して必要なプロパティを検証する。例えば、aの公開が含まれるコントラクトの場合、検証者はシークレットが明らかになる場合と明らかにならなかった場合の両方を考慮する。どちらのケースを考慮しても、認可は同様に処理される。しかし、ほとんどの場合、参加者は参加者は自分に割り当てられた行動に関してコントラクトを検証しようとし、他の参加者の行動を仮定しない(他の参加者が信頼できるとみなされない場合、彼らにとっても行動を修正する意味がでる)。例えば、参加者Aは参加者Bがシークレットを明らかにした後でのみ与えられたブランチを実行する許可を与えたいと思う。このツールを使うと、参加者の行動を制限し、シークレットが明らかにされ承認が提供される条件を指定できる。引出しや分割のように誰もが実行できる行動を制限することはできない。
例えば、参加者が選択した戦略がどうであれ、相互時限コントラクトが流動的であることを検証できる。以下の理由からcheck-liquidクエリは正しくtrueと回答する:
- Aがシークレットを明かさなければ、(ブロック高100000以降)誰もがコントラクトの全ての残高をBに転送する引出しを実行できる。
- Aがシークレットを公開し、Bがシークレットを公開しなかった場合、(ブロック100050以降)誰もがコントラクト内の残高をAに転送する引出しを実行できる。
- AとB両者がシークレットを公開した場合、誰もがコントラクトの残高を半分ずつAとBに転送する分割を実行できる。
もし、我々が16行目のafterブランチを削除すると、コントラクトの流動性は無くなる。しかし、Aの戦略がシークレットを明らかにする場合、それは流動的になる。これをcheck-liquid (strategy "A" (do-reveal a))というクエリを介して成立することを検証できる。AがBがシークレットを明らかにした後でシークレットを明らかにすることを選択した場合、つまり、Aの戦略が "A" (do-reveal a) if ("B" (do-reveal b))の場合流動性は再び失われる。
流動性に加えて、check-query
コマンドを使ってコントラクトの特定のLTL特性を確認できる。例えば、Aがシークレットを明らかにした後、Aは少なくとも自分の1Bのデポジットを取り戻すことを検証することができる。LTLではこの特性は次の式のように定式化される。
[](a revealed => <>A has-deposit>= 100000000 satoshi)
またAがシークレットを明らかにした場合、最終的にBがシークレットを明らかにするか、AがBのデポジットを入手するかも検証する。そのLTLクエリは以下の通り。
[](a revealed => <>(b revealed \/ A has-deposit>= 200000000 satoshi))
我々の検証技術はBitMLコントラクトの状態空間をmodel-checking
することに基づいている。この状態空間は無限であるため、model-checker
を実行する前に抽象化を利用して有限状態のものに削減する。この抽象化は、BitMLの具体的なセマンティクスの無限性の3つのソース、時間の経過、コントラクトの宣伝/規定、コントラクト外のBitcoinの転送を解決する。有限状態のシステムを得るため抽象化は、
この抽象化は具体的なBitMLのセマンティクスと厳密に対応する。つまり、分析中のコントラクトの具体的な各ステップは抽象ステップによって模倣され、逆もまた同様。
我々のツールは、書き換えロジックに基づくmodel-checkingフレームワークであるMaudeの抽象BitMLセマンティクスを実装している。Maudeはこの目的にとって便利だ。BitML用語間の構造的等価性を表現するための等式論理と、BitMLの抽象セマンティクスをエンコードするための条件付き書き換えルールを使用する。このような方法で、BitMLの実行可能な抽象セマンティクスを得る。BitMLコントラクトがMaudeで翻訳されると、MaudeのLTL model-checkerでユーザーが指定したセンラ訳の元でセキュリティ特性を検証する。さまざまな形態の流動性もまた対応するLTLの計算式に変換される。BitMLコンパイラの計算上の健全性は、Bitcoinでコントラクトを実行する際にmodel checkerによって検証された特性が確実に保持されることを保証する。
4. BitMLをBitcoinにコンパイル
我々のコンパイラは2つのフェーズで動作する。最初にBitMLコントラクトをA formal model of Bitcoin transactionsの形式モデルに基づくBitcoinトランザクションの抽象化層であるBalzacに変換する。それからBalzacトランザクションを標準的なBitcoinトランザクションに変換する。
BitMLからBalzacへのコンパイラは、BitMLのアルゴリズムを実装し、それをトランザクション手数料で拡張する。特に、コンパイラは各トランザクションにブロックチェーンで公開できるだけの十分な手数料が含まれていることを保証する。
BalzacからBitcoinへのコンパイラは、標準的なBitcoinトランザクションを生成する。非標準トランザクションはBitcoinネットワークおいて破棄されるのでこれは重要だ。この目的のためBalzacはP2PKHもしくはP2SH形式のアウトプットスクリプトを生成する。P2PKHは署名検証をエンコードするのに使われ(引出しによってデポジットを償還する)、一方P2SHは複雑な引出し条件のために使われる(公開されたシークレットがコミットされたハッシュと一致するかチェックするなど)。Bitcoinは標準スクリプトでプッシュされた全ての値が520バイト以内に収まることを要求するので、コンパイラは生成されたスクリプトに対してこれを満たしているかチェックする。BalzacはシリアライズされたRAWトランザクションを出力し、これはそのままBitcoinネットワークにブロードキャストできる。
5. 評価
ツールチェーンを評価するために、金融コントラクト、オークション、宝くじ、ギャンブルゲームなど代表的なユースケースのベンチマークを使用する。ベンチマークの各コントラクトについて、関係する参加者の数N、コンパイラによって取得されるトランザクションの数Tおよび流動性をチェックするための検証時間Vを表1に示す。
参加者の戦略は、流動性を確保するのに必要な場合のみ制約される。ほとんどの場合、まったく制約を課さない。シークレットに関する述語を含むコントラクトについては、原則として、可能性のある全てのシークレットの選択に対して、流動性をチェックする必要があるだろう。検証を実行可能にするため、各コントラクトは有限の述語セットのみをチェックするため、無限のシークレットの選択をリージョンの有限セットに分割し、各リージョンから1つの選択をサンプリングする。このように、流動性のチェックは有限回実行され、検証者がコントラクトの全ての到達可能な状態を確実に調査するようにする。例えば4人用の宝くじでは、34リージョン探索し、流動性を検証するのに67時間かかる。
我々のツールの性能を比較できる唯一の研究はModeling Bitcoin Contracts by Timed Automataで、これはBitcoinのコントラクトをUppaalでモデル化し、Timed Automataに基づくモデルチェックフレームワークである。これでモデル化された最も複雑なコントラクトは、2人の参加者がいる相互時限コミットメントだ。これをUppaalで検証すると30秒要するのに対し、我々のツールは100ms未満で同じ特性を検証する。このスピードアップはより高い抽象化レベルのBitMLによるもので、より低いレベルのBitcoinトランザクションで動作する。
Bitcoinは評価スタックにプッシュされる各値のサイズに520バイトの制限があるため、コントラクトを開発する際に直面した主な困難の1つは、複雑なBitMLを仕様をBitcoinにコンパイルできないことだ。場合に寄っては、そのコンパイルが520バイト制約を遵守するようにBitMLコントラクトを縮小することができた。例えば、520バイトの制約に簡単に違反する一般的なパターンは次のようなもの:
( choice ( revealif (b ) ( pred ( p0 ) ) ( C0 ) ) ( revealif (b ) ( pred ( p1 ) ) ( C1 ) ) ( after T ( C2 )) )
choiceは、その選択肢の3つのブランチに対応する3つの論理条件の分離をredeem scriptがエンコードするトランザクションにコンパイルされる。述語p0とp1およびコントラクトの参加者数に応じて、このスクリプtおは520バイトの制約に違反する可能性がある。これを回避するには、以下のように書き換える:
( choice ( revealif (b ) ( pred ( p0 ) ) ( C0 ) ) ( after T ( tau ( choice ( revealif (b ) ( pred ( p1 ) ) ( C1 ) ) ( after T1 ( C2 ) )))) )
この場合、コンパイルには2つの選択肢に対応する2つのトランザクションが含まれる。これらのトランザクションのスクリプトは選択肢の2つのブランチに対応する2つの論理条件の分離をエンコードする。この回避策を使用してトランザクション数を増やすという代償で4人用の宝くじを標準トランザクションにまとめることができた(587標準バージョン vs 138非標準バージョン)。同様の技術で(例えば述語の単純化など)、表1の全てのコントラクトを標準のBitcoinトランザクションにまとめることができる。
一般的に、520バイトの制約はBitcionのコントラクトの表現力を制限sるう。例えば公開鍵は33バイトなので、15個の署名を同時に検証する必要があるコントラクトは標準トランザクションとして使用できない。
6. 結論
スマートコントラクトのビジネスはEthereumやCardanoようなプラットフォームではやっているが、それらがBitcoinに追いついたことはない。主な理由の1つは、他のプラットフォームとは異なり、Bitcoinには高水準のコントラクト言語も関連する開発、検証ツールも無いということだ。表現力豊かでチューリング完全な言語でプラットフォームを使用することの欠点は、それがコントラクトをより広い攻撃面にさらす可能性があることだ。実際に、一連の言語によるEhtereumコントラクトの脆弱性は何億ドルもの損失を引き起こした。Ehtereumコントラクトの分析に関する最近の研究では、これらの脆弱性を検出するためのツールが作成されているが、それらの精度は、基底となる言語のチューリング完全性によって生じる固有の制限を受ける。対照的に本稿ではBitMLによって与えられたより単純な計算モデルを使って、健全で安全な検証技術を備えたツールチェーンを紹介した。
我々のベンチマークはBitMLで表現可能な多種多様なコントラクトを目にするが、改善の余地はある。まずBitMLは完全にBitcoinに対応していない。つまりBitcoinでは実行可能であるが、BitMLでは表現できないコントラクトが存在する。この不完全性の主な原因は次の3つだ。
- 関係者全員が規定する前にコンパイラによって取得された全てのトランザクションに署名する必要がある(実行時に許可用の署名のみ提供できる)。
- トランザクションで使われる署名タイプは全ての
SIGHASH_ALL
で、SIGHASH_ANYONECANPAY
やSIGHASH_SINGLE
などは使えない。 - オフチェーンのやりとりは、秘密を明らかにすることと、承認を提供することに限定される。
最初の制約は、他の人の行動に関係なく、正直な参加者が対応するBitMLコントラクトで有効になっている移動を常にBitcoinレベルで実行できるようにするために必要だ。この点に関して、BitMLは参加者が非協力的であるという標準的な仮定に従う。つまり規定後いつでも彼らは対話をやめることができる。それにも関わらず、違法行為を罰則で罰することでコントラクト内で協調を動機づけることができる。2章の期限付きコミットメントのように。上記の設計上の選択の結果として、動的に定義された参加者のセットとの契約(クラウドファウンディングなど)や、無限数の反復(マイクロペイメントチャネルなど)はBitMLでは表現できない。
BitML(およびBitcoin)の制限はさまざまな方法で克服できる。例えば、Bitcoinをそのまま使うと、上記の3の制限を緩和することが可能で、ゼロ知識オフチェーンプロトコルなどが可能になる。これは参加者がNP問題のクラスの解決策を交換するという条件付き支払いコントラクトを表現するために、プリミティブでBitMLを拡張すること可能にするだろう。同様い制限1を緩和することで、関与するすべての参加者が実行時に自分の署名を提供することを要求するサブコントラクトの動的機能を可能にするようBitMLを拡張できる。これはBitMLにおけるマイクロペイメントチャネルのモデル化を可能にするだろう。SIGHASH_ANYONECANPAY
の使用と共に(2の緩和)、クラウドファウンディングコントラクトのモデリングも可能にする。以前と同様、この拡張はBitcoinを変更することなく実現できる。
BitMLの他の拡張は、Bitcoinの拡張を必要とするだろう。例えばCovenantsでは、任意の有限状態マシンを実装することが認められている。制御されたインプットmalleabilityは、宝くじなどのマルチプレイヤーギャンブルゲームにおいてトーナメントを効率的に実装するのを可能にするだろう。これは償還トランザクションが特定のセットに属しているかどうかをチェックする新しいopcodeによって達成できる。ゼロ知識証明を使った条件付き支払いは、キーペアの有効性をチェックする新しいopcodeを利用することで実現できるだろう。任意のメッセージに対して署名をチェックする新しいopcodeは、一般的で公平なマルチパーティ計算を表現することを可能にするだろう。さらに公平で堅牢なパルティパーティ計算はより複雑なトランザクションを使って実現できる。より根本的なアプローチはBitcoinのスクリプト言語をより表現力豊かなものに置き換えることだ。例えば、Simplicityは有限ドメイン上で任意の関数を表現することを可能にする。