この記事では、Kadenaと呼ばれるセキュアでスケーラブルなスマートコントラクト実装のためのブロックチェーンについて解説します。
Kadenaは、2016年から開発が進められているセキュアでスケーラブルなスマートコントラクトを実現するためのブロックチェーンプラットフォームです。
2018年5月には、ニューヨークで開催されたConsensus 2018のイベントに合わせて、スマートコントラクトの形式的検証システムをオープンソースとしてリリースするなど、アクティブに開発が進められています。
KadenaはもともとScalableBFTと呼ばれるコンセンサスアルゴリズムを採用したプライベートチェーンとして提供されていましたが、近年はパブリックチェーンとして公開するためのプロトコル（Chainweb）も開発が進められています。
Kadenaパブリックチェーン
Kadenaのブロックチェーンは、2016年の設立時点ではエンタープライズ向けのプライベートチェーンとして提供されていました。
プライベートチェーンのコンセンサスアルゴリズムには、BFTをベースにしたScalableBFTが採用されているため、不特定多数のノードがブロックチェーンに参加することはできません。
2018年に、不特定多数のノードを対象とするパブリックチェーンを実装するため、Chainwebと呼ばれるProof of Workベースのプロトコルを提案し、2018年のQ4にローンチを目指して開発が進められています。
Kadenaのパブリックチェーンは、図1に示すとおり、エンタープライズチェーンとはコンセンサスのメカニズムは異なるものの、スマートコントラクト実装のためのPact言語や開発ツールなどは共通しています。
Chainwebアーキテクチャ
KadenaのChainwebアーキテクチャは、数百～数千のチェーンを一つに束ねるパラレルチェーンPoWです。
ピアチェーンと呼ばれるそれぞれのチェーンではそれぞれProof of Workによるマイニングが行われますが、自分自身のピアチェーンのブロックだけでなく、隣接するチェーンのブロックのマークルルートを参照する形になっています。
図2に、10個のピアチェーンを用いる場合のChainwebのイメージを示します。
図2の左に示すグラフ構造は、それぞれのピアチェーンの隣接関係を示しており、例えば1番の頂点が示すピアチェーンは、3，4，6番のピアチェーンと接しています。
図2の右に示す図は、ブロックの参照関係を立体的に示したものです。1番のピアチェーンのあるブロックは、次のブロックでは1, 3, 4, 6番のチェーンから参照されます。さらに次のブロックでは、10個のチェーンすべてから間接的に参照関係が成立します。
あるブロックが最低何ブロック後にすべてのチェーンから間接的に参照されるかは、ピアチェーンの隣接関係を示したグラフ構造におけるグラフ理論の問題に帰結できるため、大量のピアチェーンを束ねるときの設計にグラフ理論の知見が役立ちます。
一本のチェーンではなく、大量のチェーンを束ねることで、スケーラビリティを向上させ、秒間10,000トランザクションのスループットを出すことが可能だと謳われています。
また、隣接するチェーンでお互いにブロックを参照し合うことで、同じハッシュレートの単一のチェーンでのProof of Workに比べ、少ない承認数で同程度の改ざん耐性を持たせることが可能だと言われています。
クロスチェーントランスファー
大量のピアチェーンを束ねて一つのパブリックチェーンネットワークとして扱う場合、異なるピアチェーン間でのコインの移動（クロスチェーントランスファー）が問題となります。
Chainwebでは、2段階のSimple Payment Verification(SPV)をスマートコントラクトとして実装することで、安全なクロスチェーントランスファーを実現しようとしています。
図3に、2段階SPVによるクロスチェーントランスファーの実行の様子を示します。
図3では、2つの隣接するピアチェーン、Chain 1とChain 2において、同一人物（アリス）のなかで残高を移動する様子を示しています。
まず、Chain 2にあるアリスの残高10コインをDELETEし、Chain 2のブロックにコミットします。Chain 1では、Chain 2で10コインがDELETEされたトランザクションを確認し、Chain 1で新たに10コインを作成します。
直接隣接していないピアチェーン間であっても、何段階かのブロックを経由して、いずれ任意のピアチェーン同士で間接的な参照が可能なため、結果的に任意のピアチェーン間でもクロスチェーントランスファーを実行することができます。
## マークルコーン
ビットコインなど多くのブロックチェーンでは、トランザクションのマークルツリーを構成し、そのマークルルートをブロックに組み込むことでトランザクションの存在証明をしています。
Chainwebの場合、隣接する複数のピアチェーン間での参照が存在するため、あるブロックが間接的な参照関係を持つ過去や未来のブロックを図示すると、図4に示す円錐形の参照関係になります。これを、Chainwebではマークルコーン(Merkle Cone)と呼んでいます。
過去に伸びるマークルコーンは、頂点となるブロックによって存在証明ができるブロックやトランザクションを示します。
一方、未来に伸びるマークルコーンは、頂点となるブロックの存在証明をしてくれるブロックを示します。通常の単一のブロックチェーンでは、あるブロックの後続のブロック数を承認数としてカウントしますが、Chainwebでは、未来のマークルコーンに基づき承認の度合いを測ることになります。
通常のブロックチェーンでは、1ブロック間隔ごとに線形的に承認数が増えていきますが、マークルコーンの場合はブロック間隔ごとに指数関数的に承認数が増えていきます。
したがって、同じ実時間が経過したあとに、特定のブロックの内容を改ざんしようとした場合、単一のブロックチェーンに比べて改ざんが必要なブロック数が膨大となり、同じハッシュレートであってもより強固な改ざん耐性を持つことが可能です。
Pact言語
Pact言語は、LISPライクな文法を持つKadena独自のスマートコントラクト開発言語です。
Pactでは、シンプルなモジュール機能により定数や関数の再利用性を高めています。
下記に、Pactのサンプルコードを示します。「;;」で始まる行はコメント行を表し、カッコで囲まれたコードが一つの式を表しています。
コード1. Pact言語による Hello Worldプログラム
;; Define the module.
(module helloWorld 'admin-keyset
"A smart contract to greet the world."
(defun hello (name)
"Do the hello-world dance"
(format "Hello {}!" [name]))
)
;; and say hello!
(hello "World")
Pactのアクセスコントロール機能は、ビットコインのScript言語に影響を受けた公開鍵ベースの認証を採用しています。
モジュールやデータに対するアクセス権は、keysetsと呼ばれる公開鍵のリストで管理されます。
Pactには、keysetsやその他のデータを効率的に管理するためのキーバリュー型のデータベースが内包されており、データの参照や共有が簡単にできます。
コード2. Pact言語によるkeysetの管理
;; Simulate message data specifying an administrator keyset.
;; In production use 'mockAdminKey' would be an ED25519 hex-encoded public key.
(env-data { "admin-keyset": ["mockAdminKey"] })
;; Simulate that we've signed this transaction with the keyset.
;; In pact, signatures are pre-validated and represented in the
;; environment as a list of public keys.
(env-keys ["mockAdminKey"])
;; Keysets cannot be created in code, thus we read them in
;; from the load message data.
(define-keyset 'admin-keyset (read-keyset "admin-keyset"))
Pactは、EthereumのSolidity言語とは異なり、非チューリング完全なコントラクト言語です。そのため、表現力は限定されるものの、無限ループなどの危険なコードは記述することができず、セキュリティの高いスマートコントラクトを実現することができます。
また、Pactで書かれたスマートコントラクトの脆弱性をあらかじめ検出するための形式的検証システムとして、property checking systemを備えています。
### Pactの形式的検証システム
チューリング完全でないコントラクト言語により、悪意のあるスマートコントラクトの実現性を低めることができたとしても、あらゆるプログラムにはバグが混入する可能性があります。
通常のシステム開発では、単体テストやシナリオテストを実装し、プログラムのバグを検出しようとすることが多くありますが、テストに漏れがあったり、テスト自体にバグがあったりすれば、正しくバグを検出することができません。
ソフトウェアの形式的検証の分野では、プログラムを数学的な記述に変換し、その記述に想定外の動作を起こす余地がないか数学的に検証する手法が研究されています。
Pactではこの形式的検証を用いて、一般的に行われているテストの実施ではなく、数学的な検証に基づくバグの検出をすることが可能です。
例えば、Pactのデータスキーマに普遍的な制約を持たせる場合、invariantを用いて制約を記述できます。コード3は、整数型で定義されたアカウントの残高が、必ず0以上であるという制約を記述した例です。
コード3. invariantによる制約の記述
(defschema account
("user accounts with balances"
(invariants [(>= balance 0)]))
balance:integer
ks:keyset)
(deftable 'accounts:{account})
この制約条件のもとで、コード4に示すtransfer関数の脆弱性について考えてみましょう。
コード4. 脆弱性のあるtransfer関数
(defun transfer (from:string to:string amount:integer)
("Transfer money between accounts"
(properties
[(row-enforced 'accounts 'ks from)
(conserves-mass 'accounts 'balance)])
(let ((from-bal (at 'balance (read 'accounts from)))
(from-ks (at 'ks (read 'accounts from)))
(to-bal (at 'balance (read 'accounts to))))
(enforce-keyset from-ks)
(enforce (>= from-bal amount) "Insufficient Funds")
(update 'accounts from { "balance": (- from-bal amount) })
(update 'accounts to { "balance": (+ to-bal amount) })))
一見すると動作しそうなコードですが、Pactの形式的検証を実行すると、次の2つの脆弱性が見つかります。
①まず、送金に指定するamount:integerの値が負の値も許容してしまっているので、マイナスの値を相手に「送付」することで、任意の相手から残高を奪ってしまうことが可能となっています。
②また、最後の2つのupdateで、残高を更新していますが、もしfromとtoのアドレスが同じだった場合、前者のupdateは後者のupdateで上書きされてしまいます。すなわち、自分自身に送金を行うことで、何もないところから残高を増やしてしまうことが可能となっています。
これらの脆弱性に対して、amountが正の値であることと、fromとtoのアドレスが異なっていることを制約条件に加えたものが下記のコード5になります。
コード5. 形式的検証により脆弱性を修正したtransfer関数
(defun transfer (from:string to:string amount:integer)
("Transfer money between accounts"
(properties
[(row-enforced 'accounts 'ks from)
(conserves-mass 'accounts 'balance)])
(let ((from-bal (at 'balance (read 'accounts from)))
(from-ks (at 'ks (read 'accounts from)))
(to-bal (at 'balance (read 'accounts to))))
(enforce-keyset from-ks)
(enforce (>= from-bal amount) "Insufficient Funds")
(enforce (> amount 0) "Non-positive amount")
(enforce (!= from to) "Sender is the recipient")
(update 'accounts from { "balance": (- from-bal amount) })
(update 'accounts to { "balance": (+ to-bal amount) })))
形式的検証の機能により、テストを記述することなく、スマートコントラクトの脆弱性を検出し、セキュアなコントラクトを実装することができます。
参考文献：
Kadena http://kadena.io/
kadena.io – Medium https://medium.com/kadena-io
Chainweb: A Proof-of-Work Parallel-Chain Architecture forMassive Throughput DRAFT v15 http://kadena.io/docs/chainweb-v15.pdf
Kadena Chainweb https://cyber.stanford.edu/sites/default/files/kadenachainweb-bpase18.pdf
Pact – Github https://github.com/kadena-io/pact
The Pact Smart-Contract Language Revision v1.5 http://kadena.io/docs/Kadena-PactWhitepaper.pdf
The Pact property checking system https://github.com/kadena-io/pact/blob/ac759c0882d97b60473cfbb5853b1c25259e1213/docs/pact-properties.md
