Move言語のセキュリティについて深く掘り下げる:言語機能、操作メカニズム、自動監査

###イントロダクション

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

この記事では、言語の特性、実行メカニズム、検証ツールの三つの観点からMove言語の安全性の問題について探討します。

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

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

場合によっては、意味解析および静的解析ツールを利用して、安全規則にコードが準拠していることを確認し、信頼できないコードと相互作用しても、いくつかの証明可能な論理規約が変わらないようにすることができます。

これらのソリューションは見た目が良さそうで、実行時のオーバーヘッドを回避し、セキュリティ問題を事前に発見できる。しかし残念ながら、プログラミング言語がこれらの方法で得られるセキュリティは非常に限られており、主に二つの理由がある。第一に、動的ディスパッチ、共有可変性、リフレクションなどの非線形ロジックの特性により、静的分析ツールを使用できないことが多く、セキュリティ不変条件のルールに違反し、ハッカーに広範な攻撃面を提供してしまう。第二に、ほとんどのプログラミング言語は、セキュリティ関連の静的ツールや表現力のある規約化言語を使って拡張することが難しい。これらの二つの拡張は非常に重要で、事前に定義することができる。

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

Move言語の特性をよりよく理解するために、サンプルプログラムを見てみましょう:

動く モジュール 0x1::TestCoin { 0x1::signerを使用します。

const ADMIN: アドレス = @0x1;

構造体 Coin はキーを持ち、ストア {
    値: U64
}

struct Info はキーを持っています {
    total_supply:U64
}

specモジュール{
    不変式 forall addr: 存在するアドレス<coin>(addr):
        グローバル<info>(ADMIN).total_supply >= グローバル<coin>(addr).value;
}

公共の楽しみinitialize(account: &signer) {
    assert!(signer::address_of(account) == 管理者, 0);
    move_to(account、情報 { total_supply: 0 })
}

公共の楽しみ mint(account: &signer, amount: u64): Coin acquires Info {
    assert!(signer::address_of(account) == 管理者, 0);
    
    let supply = borrow_global_mut<info>(ADMIN);
    supply.total_supply = supply.total_supply + 金額;
    
    コイン { 値: 金額 }
}

公共の楽しみvalue(coin: &Coin): U64 {
    コイン.バリュー
}

公共の楽しみvalue_mut(coin: &mut Coin): &mut u64 {
    &mut coin.value (英語)  
}

}

a) モジュール(Module): 各Moveモジュールは、一連の構造体タイプとプロセス定義で構成されています。モジュールは、タイプ定義をインポートし、他のモジュールで宣言されたプロセスを呼び出すことができます。モジュールの完全修飾名は、モジュールコードが格納されている16バイトのアカウントアドレスから始まります。アカウントアドレスは、同名のモジュールを区別するための名前空間として機能します。

b) 構造体(Structs):このモジュールは、ユーザーに配布されるトークンを表すCoin構造体と、トークンの総量を記録するInfo構造体の2つの構造体を定義しています。これらの2つの構造体はリソースタイプとして定義され、永続的なグローバルキー/バリューストレージに保存できます。

c) プロセス(function): コードは初期化プロセス、安全プロセス、および非安全プロセスを定義しています。Coinを作成する前にinitializeプロセスを呼び出し、シングルトンInfoの値total_supplyをゼロに初期化する必要があります。signerは、Move外部ロジックによって検証されるユーザーを示す特別なタイプです。アサーションは、指定された管理者アカウントのみがこのプロセスを呼び出せることを保証します。mintプロセスは、管理者が新しいトークンを作成することを許可し、同様にアクセス制御があります。value_mutプロセスはCoinの可変参照を受け取り、valueフィールドへの可変参照を返します。

契約の構造は他のスマートコントラクト言語と似ていますが、リソースタイプとグローバルストレージはMove言語におけるストレージとリソースの安全性の重要なメカニズムです。

グローバルストレージは、Moveプログラムが永続的なデータを保存することを許可します。これらのデータは、それを持つモジュールによってプログラム的にのみ読み書きでき、公共の台帳に保存されていますが、他のモジュールのユーザーはそれを見ることができます。グローバルストレージ内の各キーは、完全修飾型名とその型の値を保存するアカウントアドレスで構成されています。グローバルストレージはすべてのモジュール間で共有されていますが、各モジュールはその宣言されたキーに対して排他的な読み書きアクセス権を持っています。

リソースタイプを宣言するモジュールは次のことができます: • move_to命令を使用して値をグローバルストレージに公開する • move_from命令を使用してグローバルストレージから値を削除します • borrow_global_mut命令を使用して、グローバルストレージ内の値への参照を取得します。

モジュールは、その制御下にあるグローバルストレージに強制的な制約を課すことができます。たとえば、ADMINアカウントアドレスのみがInfoタイプの構造体を保持できるようにするために、initializeプロセスを定義し、このプロセスはInfoタイプでmove_toを使用し、ADMINアドレスでmove_toを呼び出す前提条件を強制します。

以下は、このモジュールのコードの安全性を保証するための2つの静的検査特性メカニズムです: 不変条件の簡約とバイトコード検証器

a) 不変量チェック(規約チェック): モジュール第10行は静的チェックの不変量を示しています——システム内のすべてのCoinオブジェクトの値フィールドの合計は、ADMINアドレスに保存されているInfoオブジェクトのtotal_valueフィールドと等しくなければなりません。不変量は形式的検証の用語であり、状態の保存性を示します。この保存特性はモジュールのすべての可能なクライアントに適用されます。

b) バイトコード検証器: セキュリティタイプと線形化は、バイトコード検証器の主要な検証範囲です。他のモジュールは0x1::TestCoin::Coinによって制御されるグローバルストレージユニットにアクセスできませんが、それらは独自のプロセスと構造の宣言でこのタイプを使用できます。

Moveには、バイトコードレベルで強制的に適用される型システム(を持つバイトコード検証器)があり、モジュールの所有者が望ましくない結果を防ぐことができます。構造型Coinを宣言したモジュールのみが可能です: • Coinタイプの値を作成する • "Coin"タイプの値をそのコンポーネントフィールドに「アンパック」する • Rustスタイルの可変または不変の借用を通じてCoinフィールドへの参照を取得する

バリデーターは、構造体のデフォルトを線形に強制し、構造体を宣言したモジュールの外で線形にコピーおよび破棄を防ぐことを保証します。同時に、バリデーターは一部のタイプの一般的なメモリ問題に対して強制チェックを行います。

検出プロセスには主に3つのタイプがあります:

1. 構造体の合法性チェック: バイトコードの完全性を保証し、エラーの不正参照、重複リソースエンティティ、および不正なタイプ署名を検出します。
2. プロセスロジックの意味検出: パラメータタイプのエラー、ループインデックス、空のインデックス、重複定義変数などを含む
3. リンク時エラー、不正な内部プロセス呼び出し、またはリンクの宣言と定義が一致しないプロセス

バリデーターは最初にCFG(制御フローグラフ)を作成し、次にスタック内の呼び出し元のアクセス範囲を検出して、コントラクトの呼び出し元が呼び出し先のスタックスペースにアクセスできないことを保証します。同時に型をチェックするために、各Valueスタックは対応するTypeスタックを維持します。

次はリソースチェックと参照チェックです。リソースは主に二重使用不可、消失不可、必ず帰属があるなどの制約をチェックします。参照チェックは動的分析と静的分析を組み合わせ、Rustの型システムに似た借用チェック機構を使用します。

最後にリンクの確認が必要で、リンクオブジェクトと声明が一致しているか、プロセスのアクセス制御などを再度確認する必要があります。

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

2. Moveの運用メカニズム

まず、Moveプログラムは仮想マシン内で実行され、実行中にシステムメモリにアクセスできません。これにより、Moveは信頼できない環境で安全に実行でき、破壊や悪用されることはありません。

次に、Moveプログラムはスタック上で実行されます。グローバルストレージはメモリ(ヒープ)とグローバル変数(スタック)に分かれています。メモリは一次ストレージであり、その単位はメモリ単位を指すポインタを保存できません。グローバル変数はメモリ単位を指すポインタを保存するために使用されますが、インデックス方式は異なります。グローバル変数にアクセスする際、コードはアドレスとそのアドレスにバインドされたタイプを提供します。このような区分は操作を簡素化し、Move言語の意味をより形式化しやすくします。

Moveバイトコード命令はスタック式インタプリタで実行されます。スタック式仮想マシンは実装と制御が容易で、ハードウェア環境の要求が少なく、ブロックチェーンシーンに適しています。レジスタ式インタプリタに対して、スタック式インタプリタは変数間のコピーや移動をより容易に制御および検出できます。

Moveにおいて、リソースとして定義された値は、破壊的な移動によってのみ移動され、(以前にその値が保存されていたストレージの位置を無効にします)。ただし、整数(のような特定の値はコピーされることができます。

Moveプログラムがスタック上で実行されるとき、その状態は⟨C, M, G, S⟩の四元組であり、呼び出しスタック)C(、メモリ)M(、グローバル変数)G(、そしてオペランド)S(で構成されています。スタックはまた、関数テーブル)モジュール自体(を維持しており、関数本体を含む命令を解析します。

コールスタックには、プロセスの実行に関するすべてのコンテキスト情報と命令番号が含まれています。Call命令を実行すると、新しいコールスタックオブジェクトが作成され、呼び出しパラメータがメモリとグローバル変数に保存され、その後インタープリターが新しいコントラクトの命令を実行します。分岐命令に遭遇すると、プロセス内部で静的ジャンプが発生します。モジュール内のプロセスは循環を持たず、モジュールに動的割り当てがないため、実行中の関数呼び出しの不変性が強化されます：procedureの実行プロセスのcall frameは必ず隣接し、再入可能性を回避します。呼び出しreturnで呼び出しを終了し、戻り値はスタックのトップに置かれます。

MoveVMのコードを研究すると、MoveVMはデータストレージと呼び出しスタック)のプロセスロジック(を分離していることが見えてきます。これはEVMとの最大の違いです。EVMでは、ERC20トークンを実装するためには、1つのコントラクト内でロジックを記述し、各ユーザーの状態を記録する必要がありますが、MoveVMでは、ユーザーの状態)はアカウントアドレス下のリソース(として独立して保存され、プログラムの呼び出しは権限およびリソースに関する強制的なルールに従う必要があります。これは一定の柔軟性を犠牲にしますが、安全性と実行効率)の面で並行実行(の実現に大きな向上をもたらします。

! [ムーブセキュリティの説明:スマートコントラクト言語のゲームチェンジャー])https://img-cdn.gateio.im/webp-social/moments-69101617731b12c40620802eecf76caf.webp(

) 3. プルーバーを移動

最後に、Moveが提供する自動監査ツールであるMove proverを見てみましょう。

Move Proverは、推論に基づいた形式的検証ツールです。それは形式的な言語を使用してプログラムの動作を記述し、推論アルゴリズムを使用してプログラムが期待通りであるかどうかを検証し、開発者がスマートコントラクトの正確性を確保し、取引リスクを減少させるのを助けます。簡単に言えば、形式的検証とは数学的手法を用いてシステムにバグがないことを証明することです。

現在の主流な自動ソフトウェア検証アルゴリズムは、満足性モデリング理論ソルバー###SMT solver(に基づいています。SMT solverは実際には式ソルバーです。上位のソフトウェア検証アルゴリズムは、検証目標を式に分解し、SMT solverに解決を依頼し、結果に基づいてさらに分析し、最終的に検証目標が成立するか反例が見つかるかを報告します。

基本的な検証アルゴリズムは演繹的検証)deductive verification(であり、他にも境界モデル検査、k帰納法、述語抽象、パス抽象などの検証アルゴリズムがあります。

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

Move Proverの全体アーキテクチャは以下の通りです:

まず、Move Proverはプログラム入力仕様)specification(を含むMoveソースファイルを受け取ります。Move Parserはソースコードから仕様を抽出します。Moveコンパイラはソースファイルをバイトコードにコンパイルし、仕様システムと共に検証者オブジェクトモデル)Prover Object Model(に変換します。

このモデルはBoogie中間言語に翻訳されます。BoogieコードはBoogie検証システムに渡され、「検証条件生成」が行われます。検証条件はZ3ソルバー)、Microsoftによって開発されたSMTソルバー(に渡されます。

VCがZ3に渡された後、検証器はSMT式)のプログラムコードが仕様(を満たすかどうかをチェックします。もし満たしていれば、仕様が成立することを示します。そうでない場合は、条件を満たすモデルを生成し、Boogie形式に変換して診断報告書を発行します。診断報告書は、標準コンパイラのエラーに似たソースレベルのエラーに復元されます。

! [ムーブアン]