Move言語のセキュリティ分析

イントロダクション

Moveは、MoveVMを実装したブロックチェーン環境でコンパイルして実行できるスマートコントラクト言語です。設計当初からブロックチェーンとスマートコントラクトの多くのセキュリティ問題を考慮し、RUST言語のいくつかのセキュリティ設計理念を参考にしています。安全性を主な特徴とする次世代のスマートコントラクト言語として、Moveの安全性はいかがなものでしょうか？それは、言語レベルまたは関連するメカニズムでEVM、WASMなどのコントラクト仮想マシンの一般的なセキュリティ脅威を回避できるのでしょうか？Move自体に特有のセキュリティ問題は存在するのでしょうか？

本稿では、言語の特性、実行メカニズム、検証ツールの3つの側面からMove言語の安全性の問題を探ります。

1. Move 言語のセキュリティ機能

バグのないコードを書くことは難しく、何度もテストを行っても完全に保証することはできません。信頼できないコードと相互作用する際に、重要な安全特性を維持するコードを書くことはさらに困難です。実行時にセキュリティを強制するためのさまざまな技術があり、サンドボックス、プロセス隔離、オブジェクトロックなどのプログラミングパターンがあります。また、コンパイル時に静的セキュリティを指定することもでき、強制的な静的型やアサーションチェックがあります。

時には、セマンティック分析や静的分析ツールを活用して、コードがセキュリティルールに準拠していることを確認することができます。これにより、信頼できないコードと相互作用する際も、いくつかの証明可能な論理規約を維持できます。これらの方法は一見良さそうですが、実行時のオーバーヘッドを回避し、セキュリティの問題を事前に発見することができます。しかし、これらの方法を通じてプログラミング言語が得られるセキュリティは極めて限られています。主に二つの理由があります。第一に、動的ディスパッチ、共有可能性、リフレクションなどの非線形ロジックのように、静的分析ツールで分析するのが難しい言語特性を持っていることが多いです。これらの特性はセキュリティ不変量ルールに違反し、攻撃者に広範な攻撃面を提供します。第二に、ほとんどのプログラミング言語は、セキュリティ関連の静的ツールや表現力のある規約化言語をサポートするように拡張することが難しいですが、これらの二つの拡張は非常に重要です。

Move言語の設計は、信頼できないコードとの安全な相互作用をサポートし、静的検証もサポートしています。これらの安全性の特性は、柔軟性を考慮した非線形ロジックをすべて放棄し、動的ディスパッチや再帰的外部呼び出しをサポートしないために実現されています。その代わりに、ジェネリック、グローバルストレージ、リソースなどの概念を使用して、代替的なプログラミングパターンを実現しています。例えば、Moveは動的ディスパッチと再帰的呼び出しの特性を省略しており、これらの特性は他のスマートコントラクト言語で高コストな再入侵脆弱性を引き起こす原因となっています。

Move言語の主なセキュリティ機能には次のものが含まれます:

• モジュール化:各Moveモジュールは、一連の構造タイプとプロセス定義で構成されています。モジュールは、他のモジュールで宣言されたタイプ定義をインポートし、プロセスを呼び出すことができます。

• 構造体:リソースタイプを定義する構造体であり、グローバルなキー/バリューストレージに保存できるデータを表現するために使用されます。

• プロセス: 初期化、安全、非安全プロセスを定義します。プロセスにはアクセス制御制限がある場合があります。

• グローバルストレージ: 永続的なデータを保存でき、所有するモジュールのみがプログラムで読み書きできます。

• 不変条件のチェック: 静的チェックの不変条件を定義し、システム内のリソースの完全性を確保できます。

• バイトコードバリデーター: バイトコードレベルで型システムを強制し、リソースの不適切な作成、アンパック、または参照を防ぎます。

これらの特性により、Moveはコンパイル時と実行時の両方で強力なセキュリティを提供できる。

! Move Securityの説明:スマートコントラクト言語のゲームチェンジャー

2. Moveの実行メカニズム

Moveプログラムは仮想マシン上で実行され、システムメモリに直接アクセスすることはできません。これにより、信頼できない環境でも安全に実行できることが保証されます。

Moveはスタックベースの実行モデルを採用しています。グローバルストレージは、メモリ(ヒープ)とグローバル変数(スタック)の二つの部分に分かれています。メモリは一次ストレージであり、メモリ単位を指すポインタを保存することはできません。グローバル変数は、メモリ単位を指すポインタを保存するために使用され、アドレスとタイプを介してアクセスされます。

Moveはスタック式インタプリタを使用してバイトコード命令を実行します。この方法は実装と制御が容易で、ハードウェアの要求が低く、ブロックチェーンのシナリオに適しています。レジスタ式インタプリタと比較して、スタック式インタプリタは変数間のコピーと移動をより簡単に制御および検出できます。

Moveプログラムの実行時の状態は四つ組⟨C, M, G, S⟩で、呼び出しスタック(C)、メモリ(M)、グローバル変数(G)、オペランドスタック(S)を含みます。呼び出しスタックはプロセスの実行コンテキスト情報と命令番号を含みます。Call命令を実行すると、新しい呼び出しスタックオブジェクトが作成され、パラメータが保存され、新しいコントラクトの命令が実行されます。分岐命令に遭遇した場合、プロセス内部で静的ジャンプが行われます。

MoveVMはデータストレージと呼び出しスタックを分離しており、これがEVMとの主な違いです。Moveでは、ユーザーの状態(アカウントアドレスのリソース)は独立して保存されており、プログラムの呼び出しは権限とリソースのルールに従わなければなりません。この設計は一定の柔軟性を犠牲にしますが、安全性と実行効率を向上させます。

! ムーブセキュリティの説明:スマートコントラクト言語のゲームチェンジャー

3. 移動プロバー

Move Proverは、推論に基づく形式的検証ツールであり、開発者がスマートコントラクトの正確性を確保し、取引リスクを軽減するのに役立ちます。それは、形式的言語を使用してプログラムの動作を記述し、推論アルゴリズムを通じてプログラムが期待通りであるかを検証します。

Move Proverは、演繹的検証アルゴリズムを使用して、既知の情報に基づいてプログラムの動作を推論し、それが期待通りであることを確認します。これにより、プログラムの正確性を確保し、手動テストの作業負担を軽減するのに役立ちます。

Move Proverの作業フローは次のとおりです:

1. Moveソースファイルを入力として受け取り、プログラム仕様を含みます
2. パーサーが仕様を抽出し、コンパイラーがソースコードをバイトコードにコンパイルします。
3. バリデーターオブジェクトモデルの生成
4. モデルをBoogie中間言語に翻訳する
5. Boogie検証システムが検証条件を生成する
6. 検証条件をZ3ソルバーに渡してチェックする
7. 診断レポートを生成し、ソースコードレベルのエラーに変換する

Moveは、Move言語のサブセットであるMove Specification Languageを提供し、プログラムの正しさの動作を静的に記述することをサポートします。仕様はビジネスコードとは独立して記述できます。

Move Proverは、開発者がスマートコントラクトの正確性を確保し、取引リスクを減少させるのに役立つ強力なツールです。形式的手法を使用してプログラムが期待通りに動作するかを検証し、開発者がスマートコントラクトをデプロイする際の自信を高めます。

! ムーブセキュリティの説明:スマートコントラクト言語のゲームチェンジャー

サマリー

Move言語は安全性に関して包括的な考慮がなされており、言語の特性、仮想マシンの実行、安全ツールの全てが強力な保障を提供しています。ある程度の柔軟性を犠牲にし、強制的な型チェックと線形論理を採用することで、コンパイル時のチェックと形式的検証の自動化を促進しています。MoveVMの設計は状態とロジックを分離しており、ブロックチェーン資産の安全管理のニーズにより適しています。

Move言語は、EVMで一般的な再入、オーバーフロー、Call/DeleGateCall注入などの脆弱性を効果的に回避できます。しかし、認証、コードロジック、大きな整数構造のオーバーフローなどの問題には、開発者の追加の注意が必要です。Move Proverは強力ですが、全体の設計上の不注意を完全に回避することはできません。

Moveは安全性に関して多くの考慮を行っていますが、完全に安全な言語やプログラムは存在しません。Moveのスマートコントラクト開発者には、引き続き第三者のセキュリティ会社による監査サービスを利用し、規範部分の作成と検証を専門のセキュリティチームに任せることをお勧めします。

! ムーブセキュリティの説明:スマートコントラクト言語のゲームチェンジャー