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
このツールチェーンは以下で構成される。
セットアップ
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 トランザクション の抽象化層とのこと。
BitMLのコンパイル 結果
さらに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:ツールチェーンのアーキテクチャ
ツールチェーンのアーキテクチャ を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によって検証された特性が確実に保持されることを保証する。
我々のコンパイラ は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:BitMLツールチェーンのベンチマーク
参加者の戦略は、流動性 を確保するのに必要な場合のみ制約される。ほとんどの場合、まったく制約を課さない。シークレットに関する述語を含むコントラ クトについては、原則として、可能性のある全てのシークレットの選択に対して、流動性 をチェックする必要があるだろう。検証を実行可能にするため、各コントラ クトは有限の述語セットのみをチェックするため、無限のシークレットの選択をリージョンの有限セットに分割し、各リージョンから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は有限ドメイン 上で任意の関数を表現することを可能にする。