Marloweセキュリティの総合ガイド：監査結果、組み込まれた機能制限、台帳のセキュリティ機能

免責事項：Marloweセキュリティに関する本稿の内容は、いかなる種類の保証もなく「現状のまま」提供されています。本稿の内容は、財政、投資、法律、税金に関するアドバイスを含むがこれに限定されない専門的なアドバイスを目的としたものではありません。Input Output Globalは、読者が本稿から得られる情報の使用またはこれへの依存に一切の責任を負いません。

はじめに

ほとんどのブロックチェーンにおいて、スマートコントラクトとは、事前に定義された特定の条件が満たされると自動で実行されるコンピュータープログラムです。Cardanoではこれがやや異なります。スマートコントラクトの実行は、Cardanoノードに外部から送信されたトランザクションで発生します。しかし、内部の仕組みに関係なく、スマートコントラクトは金融、不動産、商業、その他多くの業界で役立ちます。

スマートコントラクトを使用したトランザクションは相当な価値の移動や移転を伴う場合があり、悪人の格好のターゲットになる可能性があります。同様に、コーディングの欠陥や脆弱性のために、この価値がロックされたり丸ごと失われたりするケースも考えられます。

望ましくない結果を避けるためには、堅牢なセキュリティフレームワークを実装する必要があります。これには、設計原則、監査、そして、開発者や取引所、その他スマートコントラクトを扱う人々によるベストプラクティスが含まれます。

Marloweは、あちこちのCardano技術コミュニティから次々と寄せられる幅広いリソースに追加されたツールと言語のエコシステムであり、Cardanoブロックチェーンで金融スマートコントラクトやトランザクション用スマートコントラクトの開発を可能にするためにInput Output Global（IOG）によって開発されました。

Marloweスイートは、セキュリティ重視で設計、開発されています。Marloweには、コントラクトが有限で、必ず終了するようになど、機能上の制限が組み込まれています。また、再帰やループなど望ましくない結果を防ぐために、特定のプログラミングが構築できないようになっています。Marloweをメインネットにデプロイする前に、サードパーティのTweagが静的動的監査を実行しています。こうしたセキュリティ対策やその他の機能によって、スマートコントラクトを安全に作成、開発するプラットフォームが実現しています。

本稿ではMarloweのセキュリティに焦点を当て、セキュリティ監査の結果、それに対するチームの対応、組み込みまれた機能制限、デプロイに含まれるセキュリティ分析ツール、そして、Marlowe使用時に必要な予防策と考慮すべき事柄について説明します。

本稿の構成

本稿は、6つの明確に定義されたセクションから構成されています。

1. スマートコントラクトの監査
2. スマートコントラクトに対する攻撃
3. Tweagによる監査
4. セキュリティ強化のために組み込まれたMarloweの機能制限
5. トランザクションの検証
6. 通貨ポリシー

本稿では、まずスマートコントラクトにおける監査の重要性と、現在存在するスマートコントラクトに対するさまざまな攻撃のタイプを総合的に理解したうえで、Marloweツールスイートが、安全なスマートコントラクトの開発環境を維持するために、監査と強力なセキュリティ原則をいかに活用しているかを説明します。

スマートコントラクトの監査

概要

スマートコントラクトに固有の自律性と、特定のトランザクションにおける比較的高いリスクは、一貫性とセキュリティの確保が非常に重要であることを意味しています。スマートコントラクトを実行したときにどのように動作するかを正確に知り、あらゆる欠陥の可能性や害意のあるコードを検知して対処できるようにすることが求められます。セキュリティの観点からスマートコントラクトの監査を行うことは、その後の失敗や損害を防ぐための最良の方法です。監査では、スマートコントラクトのコードと条件をデプロイ前に徹底的に検査し、コントラクトが期待通りに動作することを確認します。

監査メソッド

スマートコントラクトの監査のアプローチはプロジェクトごとに多岐に渡りますが、スマートコントラクトは手動または自動のメソッドを使って分析することができます。通常、ほとんどのプロジェクトでは両方を組み合わせています。

ドキュメントの収集

監査プロセスを開始する前に、監査担当者はプロジェクト関連文書を収集する時間を取ります。関連文書には、技術文書、白書、コードベース、その他監査プロセスに関連し、役立つと思われる資料が含まれます。

手動監査

このスマートコントラクト監査形式では、複数の人々が、コードを行ごとに、また、コントラクトロジック、コントラクトアーキテクチャー、および組み込まれたセキュリティ対策を分析して、正確であること、設計が効率的であることを確認します。手動監査では、コーディングエラーを明らかにするだけでなく、設計上の欠陥を見つける場合もあります。手動監査は、非常に徹底的で正確なメソッドとみなされる傾向があります。

自動監査

手動監査と異なり、自動監査では通常ソフトウェアを中心としたアプローチでテストを実行します。独自のソフトウェア監査ツールや既成のツールはバグの検出に役立ちますが、特定の脆弱性が明らかにならない場合があります。

こうしたメソッドは補完的であるため、監査のベストプラクティスとは、手動監査と自動監査を組み合わせてあらゆる潜在的欠陥、バグ、脆弱性を検知し修正することです。

監査後のアクション

監査プロセスが完了したら、監査担当者は調査結果の詳細を記載したレポートを作成します。これには、程度別のエラー分類および一連の推奨事項が含まれます。

コントラクトのエラーは次のように分類できます。

• クリティカル：コントラクトやプロトコルの安全機能を妨げる可能性のある欠陥
• メジャー：資金の損失やプロトコルの制御不能に陥る可能性があるコーディングやロジックにおける特定のエラー
• ミディアム：資金へのリスクはないが、コントラクトのパフォーマンスや信頼性に影響を及ぼす可能性のあるエラー
• マイナー：通常セキュリティにほとんどもしくはまったく影響のない、非効率なコード
• 参考：通常コーディングスタイルやベストプラクティスに関する問題を指摘するもの

スマートコントラクトの監査の利点

監査はどのようなアプリケーションにも重要ですが、ブロックチェーンで実行されるスマートコントラクトや分散型アプリケーション（DApp）にとっては、こうした分散型台帳の持つ不変という性質のために特に重要となります。

スマートコントラクトを監査する利点としては、リスクを先回りして特定する、高くつきかねないエラーを回避する、全体的な開発環境を改善する、脆弱性についての洞察、そしてそれをいかに排除するかについての洞察を得られる、などが挙げられます。

リスクを先回りして特定する

監査されていないスマートコントラクトをデプロイすることは賭けであり、開発者や企業が行うべきことではありません。スマートコントラクトの中には多額の資金が絡むものもあり、紛失したり侵害された場合、さらに大きな負債につながる可能性があります。こうしたリスクの是正に積極的に取り組むことで、何らかの悪い結果につながる可能性が大幅に緩和されます。

高くつきかねないエラーを回避する

コーディングエラーやロジックエラーによって、または、コントラクトへの悪質な干渉の結果資金が永久にロックされてしまうという事態を経験したいと思う顧客や開発者はいません。また、経済的損失はその一面に過ぎず、法的に重大な影響が生じる場合もあります。

全体的な開発環境を改善する

ソフトウェアの監査は、単なる推奨ではなく要件です。アプリケーション、またはアプリケーションスイートのセキュリティを保証し、ベストプラクティスに従うことで、提供するものが強化され、より健全な開発環境が生まれます。

脆弱性についての洞察、そしてそれをいかに排除するかについての洞察を得られる

ソフトウェアの開発において、予防はパッチよりも優れています。スマートコントラクトの場合、ブロックチェーンが不変であるためにパッチのチャンスはありません。徹底的な監査によって、コード、コントラクトロジック、アーキテクチャー、その他多くのパラメーターに関する多くの情報が得られ、開発者は可能な限り最良のコントラクトを作成することが可能になります。

スマートコントラクトに対する攻撃

リエントラシー攻撃

この攻撃では、二番目のコントラクトを呼び出すことによってスマートコントラクト機能にトランザクションの制御を一時的に放棄させ、二番目のコントラクトで最初のコントラクトに再帰的な引き出し呼び出しをかけ始め、最初のコントラクトがステータスを更新する前に資金を排出させます。この種の攻撃はスマートコントラクトのコーディングのバグによって可能になります。2016年のDAOの事件には、このリエントラシー攻撃が絡んでいます。

Cardanoブロックチェーンでは、設計によってリエントラシー攻撃が不可能になっています。CardanoはEUTXOモデルを使用しているため、スマートコントラクトはアトミックであり互いに呼び出すことはないことから、リエントラシーが不可能になります。

フロントランニング

ブロックチェーンの設計によっては、オンチェーンで確認される前にスマートコントラクトやトランザクションが一時公開できるようになっているものもあります。これらの保留中のトランザクションはメモリープールを通じてネットワーク全体で共有されており、攻撃者はコントラクトが意図する結果を見ることができます。このような保留中のトランザクションを見ることができる攻撃者は、他のユーザーの利益を犠牲にして、保留中の取引に基づいて利益を得ることができるような、新しい取引やトランザクションを導入することができます。つまり、攻撃者は自分の利益のためにトランザクションの実行順序を操作するのです。

この種の事件は他のブロックチェーンでは大問題ですが、Cardano（およびMarlowe）がフロントランニングに対して脆弱であるという証拠はありません。

Oracle操作

Oracleはブロックチェーンを外部システムに接続し、スマートコントラクトはOracleから受け取ったデータに基づいて実行される場合があります。この外部システムへの依存性は、Oracleが受信したインプットがOracleにフィードされる前に操作された場合、スマートコントラクトの実行におけるセキュリティと整合性が損なわれる可能性があることを意味しています。

この他にも、スマートコントラクトのセキュリティの脆弱性には、算術エラー、整数のオーバーフローとアンダーフロー、スマートコントラクトの可視性設定、タイムスタンプ操作などがあります。

Tweagによる監査

このセクションでは、Tweagによるセキュリティ監査の結果、Marloweチームの対応、Marloweの設計に組み込まれたセキュリティ原則に焦点を当てます。

Tweagによるセキュリティ監査と社内の対応の要点

TweagがMarlowe言語の手動監査と自動監査を行った結果、いくつかの問題が明らかになりました。

重大度の高いものには、負のデポジットの処理、「二重満足」の防止、ステータス不変条件の適用、形式仕様とPlutus実装間の差異、資金保存定理の証明などが含まれます。

負のデポジットの処理

デポジットからの収入は、マイナスの場合でも構わずデポジットのインプットを合計することによって計算されますが、セマンティクスはこれをゼロデポジットとみなします。Marlowe終了ステータスにおけるバランスチェックがないことと併せて、終了残高がMarloweバリデーターに支払われた値と異なってもよくなります。これは、マイナスデポジットを可能にするMarloweコントラクトによって悪用される可能性があります。

社内の対応

この問題は、Marloweセマンティクスバリデーターに負のデポジットに対するガードを追加することによって解消されました。ガードによって、バリデーターの負のデポジットのセマンティクスがMarloweのIsabelleセマンティクスと一致することが保証されます。具体的には、負のデポジット分はゼロデポジットとして扱われます。したがって、負のデポジットでPlutusデータのアカウント残高は減少せず、内部残高の合計は、MarloweセマンティクススクリプトアドレスへのUTXOに入っている値と一致します。

二重満足の防止

Marloweバリデーターは、同じトランザクションで実行されているMarloweバリデータースクリプトの複数のコピー間で二重満足を防止しましたが、Marloweバリデーターが同じトランザクションで別のPlutusバリデーターと一緒に実行している場合は防止できませんでした。

社内の対応

二重満足は、Marloweバリデーターが当事者へ支払いを行うトランザクション中に実行される唯一のPlutusスクリプトとなることを強制することによって防止できるようになりました。これにより、Marloweコントラクトは、二重満足が不可能な状況下でのみ、別のPlutusスクリプトとの調整が可能になりました。この緩和策の正確性を確認するために、いくつかのプロパティベースのテストが追加されました。

ステータス不変条件の適用

元々、Marloweバリデーターは自身の正しい操作について楽観的な仮定をしており、Plutusの実行コストを削減するために特定のステータス不変条件についてチェックしていませんでした。

社内の対応

Marloweセマンティクスバリデーターは初期ステータスと最終ステータスの不変条件を厳密に適用し、正のアカウントの3つのステータス不変条件、ステータスエントリー（accounts、choices、bound values）の重複がないこと、内部値の合計がスクリプトのUTXOの値と一致することを確認するようになりました。

形式仕様とPlutus実装間の差異

監査では、形式仕様と実際のPlutus実装間で違いがあることが明らかになりました。具体的には、Isabelle、Haskell、Plutus Txに関する言語とその効率性の違いです。

形式仕様は形式手法の言語であるIsabelleを使用しますが、実際のMarlowe実装ではHaskellとPlutus Txが使用されています。Marloweチームは可能な限りIsabelleの仕様に従うように努力しましたが、言語の違いによるいくらかの逸脱は避けられませんでした。例えば、Marlowe実装においてIsabelleでは非効率な部分もあったため、より効率的なHaskell実装のために変更が余儀なくされる場合もありました。

社内の対応

この問題はコード分析とプロパティベースのテストによって緩和されました。

資金保存定理の証明

資金保存定理は資金の額のみを考慮して、その種類は不問とされていました。つまり、証明は、例えばコントラクトが20ADAと15Djedを受け取り、20Djedと15ADAを返済するといったケースを考慮していませんでした。

社内の対応

この問題は、Isabelleコードの改訂により解消されました。具体的には、新しいMultiAssets型を追加し、Isabelleコードを（インタープリターを変更せずに）リファクタリングして、資産が保存されていることを証明します。

セキュリティ強化のために組み込まれたMarloweの機能制限

Marloweは、特定のセキュリティリスクが発生しないようにするために、いくつかの制限を設けています。

• コントラクトは有限
• コントラクトは終了する
• コントラクトには一定の有効期限がある
• コントラクト終了時に資産が保持されることはない
• 値は保存される

これらの制限に加えて、Marloweには安全を確保するために一部のプログラミング言語構造が存在しません。

• 再帰は不可
• ループはサポートされない
• 関数またはマクロが定義されていない場合がある
• タイムアウトは数値定数でなければならない
• Case継続のみマークル化可能。Faustusプログラミング言語は上記の制限をいくらか緩和するが、Marloweのセキュリティを確保するためにコンパイルされる

セキュリティ分析ツール

Marloweチームが設計したmarlowe-cli run analyze分析ツールは、MarloweコントラクトとCardanoの台帳ルールとの互換性をチェックします。

Cardano台帳には、MarloweコントラクトがMarlowe言語的に有効であっても、オンチェーンで実行することを防ぐことができるような制限が組み込まれています。例えば、台帳はロール名とトークン名の長さに制限を課したり、Plutus実行コストを制限したりしています。こうしたルールのいずれかに違反している場合、コントラクトはたとえ正しく構築されていたとしてもオンチェーンで実行されません。同様に、Playgroundで実行できても、台帳の制限に違反している限りオンチェーンで実行されることはありません。台帳設計の組み込み制限の詳細はこちらをご覧ください。

主要ポイント：Playgroundは言語に関連するものであり、RuntimeはMarloweコントラクトをCardanoブロックチェーンに実装するためのものです。Marloweを別のブロックチェーンに実装する場合、Playgroundは使用できますが、Runtimeを別のブロックチェーンで使用することはできません。

注：データがオンチェーンに適合しない場合コントラクトはロックされる可能性がありますが、Marloweスイートにはこのリスクを評価するツールが含まれています。これらのツールはコントラクトをデプロイする前に使用します。

トランザクションの検証

UTXOの支出の検証には、2種類のPlutusバリデータースクリプトが関与します。

• セマンティクスバリデーター
• 支払いバリデーター

セキュリティ慣行では、トランザクションの内容と意味を確認し、十分に理解しない限り、トランザクションに署名しないこととされています。Marlowe環境では、これはMarloweコントラクト、そのインプット、ステータスを検証することを意味します。また、使用されているロールミントポリシー（適用される場合）とMarloweバリデーターが正しいものであることを確認することも意味します。

以下のセキュリティに関する考慮事項は、バリデーターとスクリプトタイプの両方に適用されます。

セマンティクスバリデーター

Marloweトランザクションに署名する前に、次のコンセプトをよく理解しておくことが必要です。

• トランザクションはMarloweコントラクトを作動させるか
• ロールミントポリシーは何か（適用される場合）
• ロールトークンはどのように配布されたか（適用される場合）
• 現在のコントラクトとそのステータスとは
• コントラクトにはどのようなインプットが適用されているか
• トランザクションで他に何が発生しているか

トランザクションはMarloweコントラクトを作動させるか

Plutusバリデータースクリプトは指定されたバージョンのすべてのMarloweコントラクト用のユニバーサルインタープリターです。つまり、MarloweコントラクトのUTXOはスクリプトハッシュに存在します。トランザクションが、支払い部分としてMarloweスクリプトハッシュを持つアドレスから使用されていることを検証することで、真のMarloweバリデーターが特定のUTXOの支出を検証するために実行されることを確認することができます。Marloweバリデーターのスクリプトハッシュは、このリポジトリ内のMarloweスクリプトのソースコードが信頼できると仮定して、バリデーターをコンパイルしてハッシュを計算することで、第一原理から計算することができます。

ロールミントポリシーは何か（適用される場合）

ミントポリシーは特定のトークンタイプのトークンを作成するためのルールセットであり、ミントポリシーのハッシュによって識別されます。これは、ミントポリシーIDと呼ばれます。ミントポリシーは、新しいトークンを作成できるかどうか、または作成されたトークンがすべてとなるかどうかを決定します。

例えば、貸し手や借り手などのMarloweコントラクトの当事者は、次の2つの方法で表現できます。

• アドレスで：アドレス型の各当事者は、いずれかの当事者のウォレットによって保持されていると思われる公開鍵と秘密鍵のペアのインスタンスに対応します。アドレスは、ロールよりも簡単で安価に当事者を表すことができます。自分自身を認証するためには、アドレスで表される当事者は、単に認証を必要とするトランザクション（つまり、当事者のデポジットまたは選択を実行するトランザクション）に署名すればいいのです。
• ロールトークンで：ロール型の各当事者は、オンチェーンに保存されているトークンに対応します。コントラクトがロールトークンを認証として使用するためには、ロールトークンのミントポリシーIDがロールトークンとして使用するトークンのミントポリシーIDであることをコントラクトで宣言する必要があります。この場合、ミントポリシーIDで識別されるトークンの各資産名は、異なる当事者を表します。トランザクションを認証するために、ロールトークンの所有者は、ロールトークンの所有者の認証を必要とするトランザクションの一部として、そのトークンを含めればいいのです。同じ資産名を持つトークンが複数存在する可能性があるため、当事者の資産名を持つロールトークンの全インスタンスを所有していない限り、厳密に言えばロール当事者を所有することはありません。

ロールトークンはどのように配布されたか

コントラクトが当事者を表すためにアドレスのみを使用するのであれば、ロール用のミントポリシーは問題になりません。アドレスの欠点は、証明可能な転送ができないことです。アドレスの秘密鍵を知ってしまうと、忘れたり削除したりしたことを示すことができません。アドレス受信者にとってみれば、そのアドレスは常に安全ではなくなります。安全なアドレスを取得する唯一の方法は、自分で生成することです。

ロールの利点は、トークンはチェーンでネイティブ資産として扱われるため、ADAやその他の資産のように転送できることです。しかし、正しいミントポリシーIDと資産名を持っていれば誰でもそれが示す当事者として行動することができるため、そのようなトークンを所有する唯一の人物であることを確実にしなければなりません。さもなければ、その当事者を完全に掌握していることにはなりません。

もちろん、ロールトークンを自分でミントすることで、確実にそのトークンの唯一の所有者になることもできます（Marlowe Runtimeは、コントラクト作成プロセスの一環として安全にこれを行います）。ロールトークンやコントラクトが他者によって作成された場合、以下を確認する必要があります。

• 当事者をコントロールする既存のトークンをすべて確保している
• これ以上対象トークンが作成されることはない（ミントポリシーで許可されていないため）

ミントポリシーがシンプルなものである場合、これを確認する最も簡単な方法は、Marloweスキャナーを使ってコントラクトのロールミントポリシーIDを見つけることです。それから、Cardanoエクスプローラーでミントポリシーを支えるポリシーがどのようなものであるか（これ以上のロールを作成させないように）、さらに、すでに作成されているロールの現在の分布状況を確認します。

現在のコントラクトとそのステータスとは

コントラクトのトランザクション前のステータスは、Marloweスクリプトアドレスから支出されたUTXOに関連付けられたPlutusデータで定義されます。このデータはトランザクションで指定される必要があり、以下を含んでいる必要があります。

• コントラクト内のアカウント残高
• コントラクト実行におけるこの時点までの選択履歴
• コントラクトのバインド変数の現在の値
• コントラクトのうち履行すべき部分

このデータは、未署名のトランザクションボディから抽出して、Plutus.V2.Ledger.Api.fromData関数を使用してLanguage.Marlowe.Core.V1.Semantics.MarloweDataに逆シリアル化することができます。

あるいは

• コマンドラインツール'marlowe log --show' contractは、コントラクトのオンチェーン履歴を表示します。
• このオンラインツールも、オンチェーンのコントラクトとステータスを表示することができます。
• REST APIはmarlowe log --showで取得されるものと同じ情報を提供します。

コントラクトにはどのようなインプットが適用されているか

MarloweスクリプトアドレスのUTXO使用に関連するPlutusリディーマーは、トランザクションボディで指定されたトランザクションのスロット有効期間とともに、コントラクトに適用されるインプットを定義します。インプットは、ゼロ以上のデポジット、選択、通知のシーケンスです。Marlowe PlaygroundやMarlowe-cli run prepareなどのツールを使用して、このインプットをコントラクトに適用した結果を分析することができます。

このリディーマーは、未署名のトランザクションボディから抽出して、Plutus.V2.Ledger.Api.fromData関数を使用してLanguage.Marlowe.Scripts.MarloweInputに逆シリアル化することができます。コマンドラインツールmarlowe-cli util slottingは、有効期間内に指定されたスロットとコントラクト内のPOSIX時間との関係を計算します。

トランザクションで他に何が発生しているか

未署名のトランザクションには、Marloweコントラクトに指定されている以外の支出や支払いが含まれる場合があります。これは、cardano-cli transaction viewツールで調べることができます。

通貨ポリシー

通常、単一のミントイベントとロールごとのトークンを強制する通貨ポリシー（Marlowe Runtimeでサポートされているものと同様のもの）を使用する必要があります。これらのポリシーは、ロールトークンが真のNFTであり、そのためロールトークンの保持者はコントラクトで当事者として行動できる唯一であることが検証可能であると確認できます。

特定のロールトークンのコピーを複数ミントする通貨ポリシー、またはオープンミントポリシーを持つポリシーは、非標準ユースケースをサポートしています。例えば、各ロールトークンのコピーを2つミントして同じ当事者に配布すると、当事者は、「ホット」なロールトークンを入れたウォレットにアクセスできなくなった場合のバックアップとして、コールドストレージにトークンを1つ入れておくことができます。いくつかの新しいクラウドソーシングコントラクトでは、多くの参加者にロールを割り当てる場合があります（同じロールトークンを使用。トークンはコントラクト開始後にミントされる場合もあり得る）。さらに、Plutusコントラクトのロールトークン用ミントポリシーは、1つ以上のMarloweコントラクトの操作と調整できます。

ロールトークン

トールトークンは、Marloweトランザクションのデポジットと選択を承認できます。ロールトークンの使用の承認は公開鍵の承認よりも柔軟です。これは、ロールトークン（およびMarloweコントラクトへの参加）がウォレット間または他者へ転送できるためです。

Marloweバリデータースクリプトは、新しいユースケースを可能にするために、ロールトークンに対して特定の通貨ポリシーを適用することはありません。しかし、ロールベースのMarloweコントラクトにおける承認のセキュリティは、ロールトークンの通貨ポリシーに決定的に依存しています。これは、通貨ポリシーとオンチェーンでのトークンの支払いの両方を、Marloweコントラクトに参加する前に慎重に精査する必要があることを意味しています。シンプルなスクリプトの通貨ポリシーを検証するには、ブロックチェーンからスクリプトを取得して調査します。Plutusスクリプトによる通貨ポリシーを検証するには、スクリプトのPlutusソースコードを取得、調査し、ソースコードをハッシュして通貨ポリシーIDを確認します。

謝辞：本稿執筆にあたり、Joseph Fajen、Brian Bush、Omer Husainの諸氏から貴重なご意見をいただきました。