Move言語の安全性分析:スマートコントラクト言語のゲームルールを変える者

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

この記事では、言語の特性、実行メカニズム、検証ツールの3つの側面からMove言語の安全性の問題について考察します。

1. Move言語のセキュリティ特性

既存の多くのプログラミング言語とは異なり、Move言語の設計目標は、不正なコードと安全に相互作用できるプログラムを記述することをサポートし、同時に静的検証をサポートすることです。この目標を達成するために、Moveは柔軟性の考慮に基づく非線形論理を放棄し、動的ディスパッチや再帰的外部呼び出しをサポートしません。その代わりに、ジェネリクス、グローバルストレージ、リソースなどの概念を導入して代替的なプログラミングモデルを実現しています。たとえば、Moveは動的スケジューリングや再帰呼び出しの特性を省略しており、これらの特性は他のスマートコントラクト言語では高コストな再入可能性の脆弱性を引き起こす可能性があります。

Moveのコアセキュリティ機能には、以下が含まれます:

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

2. 構造体(Structs):リソースタイプとして定義でき、永続的なグローバルキー/バリューストレージに保存できることを示します。

3. 过程(Function):モジュールの動作ロジックを定義します。

4. グローバルストレージ: Moveプログラムが永続データを保存することを許可し、これらのデータはそれを所有するモジュールによってプログラム的に読み書きされることのみができます。

5. 不変量チェック:静的チェックの不変量を定義でき、システム状態の保存性を確保します。

6. バイトコードバリデーター:バイトコードレベルで型システムを強制し、不正な操作を防ぎます。

Moveはこれらの特性によってコンパイル時にコードの安全性を保証します。次に、Moveの実行メカニズムを分析し、MoveVMがどのように実行時の安全性を保証するかを見ていきます。

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

2. Moveの運用メカニズム

Moveプログラムは仮想マシン上で実行され、実行中にシステムメモリにアクセスできないため、信頼できない環境で安全に実行できます。Moveプログラムはスタック上で実行され、グローバルストレージはメモリ(ヒープ)とグローバル変数(スタック)の2つの部分に分かれています。メモリは一次ストレージであり、メモリユニットへのポインタを格納することはできません。グローバル変数はメモリユニットへのポインタを格納するために使用されますが、インデックス方式はメモリとは異なります。

Moveのバイトコード命令は、スタック型インタプリタ内で実行されます。スタック型仮想マシンは実装と制御が容易で、ハードウェア環境に対する要求が低く、ブロックチェーンのシナリオに適しています。レジスタ型インタプリタに比べて、スタック型インタプリタは変数間のコピーや移動の制御と検出が容易です。

Moveプログラムの実行中、その状態は⟨C, M, G, S⟩の4つのタプルで構成されています。これには、呼び出しスタック(C)、メモリ(M)、グローバル変数(G)、オペランド(S)が含まれます。スタックは、関数体を含む命令を解決するために、関数テーブル(モジュール自体)も維持しています。

MoveVMはデータストレージとコールスタック(のプロセスロジック)を分離しており、これはEVMとの最大の違いです。MoveVMでは、ユーザーの状態(アカウントアドレス下のリソース)が独立して保存され、プログラムの呼び出しは権限とリソースに関連する強制ルールに従わなければなりません。これは一定の柔軟性を犠牲にしていますが、安全性と実行効率(において同時実行)を実現する上で大きな向上をもたらしました。

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

3. ムーブプロバー

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

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

Move Proverのワークフローは以下の通りです:

1. Moveソースファイルを入力として受け取り、このファイルにはプログラム入力仕様(specification)を設定する必要があります。

2. Move Parserはソースコードから仕様を抽出します。

3. Moveコンパイラはソースファイルをバイトコードにコンパイルし、規範システムと共同で検証者オブジェクトモデル(Prover Object Model)に変換します。

4. モデルをBoogie中間言語に翻訳します。

5. Boogie検証システムは、入力に対して「検証条件生成」(verification条件generation)を実行します。

6. 検証条件をZ3ソルバー(マイクロソフトが開発したSMTソルバー)に渡す。

7. Z3はSMT式(のプログラムコードがspecification規格)を満たしているかどうかを確認します。

8. もし満たすことができない場合は、規範が成立していることを示します。それ以外の場合は、条件を満たすモデルを生成し、Boogie形式に変換して診断報告を発行します。

9. 診断報告をソースコードレベルのエラーに復元する。

MoveはMove Specification Languageを使用してシステムの仕様を記述します。この言語はMoveのサブセットであり、プログラムの正しい動作を静的に記述することをサポートし、生産に影響を与えません。ビジネスコードと形式的検証コードを分離するために、専門の規約化ファイルを独立して作成することができます。

Move Proverは、開発者がスマートコントラクトの正確性を確保するのに役立つ便利なツールです。これは形式的な言語を使用してプログラムの動作を記述し、推論アルゴリズムを使用してプログラムが期待通りであることを検証します。これにより取引リスクが軽減され、開発者はスマートコントラクトを生産環境に自信を持ってデプロイできるようになります。

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

4. まとめ

Move言語は安全性の設計において非常に優れており、言語の特性、仮想マシンの実行、そして安全ツールの面で包括的に考慮されています。言語の特性は一部の柔軟性を犠牲にし、強制的な型チェックと線形論理を導入することで、コンパイルチェックと形式的検証の自動化及び安全な検証可能性を容易にしています。MoveVMの設計は状態とロジックを分離し、ブロックチェーン上の資産安全管理のニーズにより適合しています。

言語の観点から、MoveはEVMに一般的な再入、オーバーフロー、Call/DeleGateCall注入などの脆弱性を効果的に回避できます。しかし、認証、コードロジック、大整数構造のオーバーフローなどの問題には、開発者の注意が必要です。Move Proverは全体的な意図が疎かである場合、機能しない可能性があります。

Move言語は安全性の面でプログラマーに多くの配慮をしていますが、完全に安全な言語やプログラムは存在しません。Moveスマートコントラクトの開発者には、第三者のセキュリティ会社による監査サービスの利用をお勧めし、仕様の一部コードの作成と検証を第三者のセキュリティ会社に任せることを推奨します。

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