Verus で正しさが数学的に証明できる Rust コードの開発

本ブログは 2026 年 8 月 31 日に公開された Amazon Science Blog “Developing provably correct Rust code with Verus” を翻訳したものです。

コードをその機能の数学的な仕様に照らして自動的に検査する「プログラム検証ツール (program verifier)」である Verus が、ソフトウェアプロジェクトのセキュリティ保証をどのように高めるのかを紹介します。

オープンソースや企業のソフトウェアプロジェクトの多くが Rust プログラミング言語を採用しており、いくつかの事例は Amazon 社内にもあります。Rust が選ばれているのは、C 言語に匹敵するパフォーマンスと柔軟性を備えつつ、洗練された型システムによってさまざまなバグやセキュリティの脆弱性を自動的に防ぐからです。その結果、平均的なコードよりも正しく安全で、しかも高速なコードが得られます。

しかし、「より正しく安全である」ことは「実際に正しく安全である」ことと同じではありません。例えば C では、配列の範囲外アクセス (out-of-bounds access)、つまり配列に割り当てられたメモリの境界を越えたインデックス指定は、予測できない結果を招く危険な誤りです。Rust では範囲外アクセスが起きるとプログラムが停止するため、確かに安全性は高まりますが、本当に正しいプログラムであれば、そもそも範囲外アクセスは起こりません。同様に Rust は、プログラムが期待どおりの結果を計算することや、自身がアクセスできる機密情報を漏洩しないことまでは保証できません。ここで役立つのが Verus です。

配列の範囲外アクセスは、予測できない結果を招く危険な誤りです。正しいプログラムであれば、これを許しません。

Verus とは

Verus は、Rust 向けのオープンソースの自動プログラム検証ツール (program verifier) です。プログラム検証ツールは、コードがどのように振る舞うべきかを記述した形式的な数学的仕様を受け取り、あらゆる入力に対してコードがその仕様に一致することを機械的に検査します。

例えば、ソート済み配列から特定の値を探すために、最適化した二分探索アルゴリズムを実装したコードがあるとします。仕様には、コードがインデックスを正常に返した場合に、配列内の対応する要素が目的の値と一致することを記述できます。検証ツールは、あらゆる入力配列と目的の値についてこの仕様が成り立つことを検査します。

一方、従来のテスト手法では、いくつかの特定の配列を試すことはできても、コーナーケースを見落とすおそれがあります (目的の値が配列の最後の要素である場合や、そもそも存在しない場合など)。プログラム検証で重要なのは、コードが仕様に一致することを示す数学的な証明を構築する点です。Verus のような自動プログラム検証ツールでは、証明構築のうち退屈で低レベルな手順の多くをツールが自動的に処理し、人間の開発者は高レベルな指示を与えます。例えば、帰納的証明の設定やループ不変条件 (loop invariant) の提示などです。以下で説明するように、最近ではこうした高レベルな手順も多くの場合 AI で自動化できます。

Amazon は Rust Foundation の創設メンバーであることを誇りに思っており、さまざまなプロジェクトで Rust を幅広く活用しています。例えば、AWS Lambda と AWS Fargate を支える Firecracker、Amazon のサーバーレス分散 SQL データベース、そして Nitro Isolation Engine などです。Nitro Isolation Engine は、Amazon Web Services (AWS) の仮想マシン割り当てを管理するソフトウェアである Nitro Hypervisor のために、仮想マシンの分離を強制するものです。Amazon の Rust に対する熱意と、10 年以上にわたる自動推論への取り組みを踏まえれば、Amazon が書く Rust コードにさらに強力な保証を与えるために Verus を採用するのは自然な流れです。実際に Amazon は、Nitro Isolation Engine が使用する主要なプリミティブや、Amazon 社内の複数の重要なインフラストラクチャについて、Verus を用いて正しさを証明してきました。こうしたユースケースは今後の記事で取り上げる予定です。まずは、Verus で Rust コードを検証するとはどういうことなのかを詳しく見ていきましょう。

Verus による Rust コードの検証

Verus を使うと、Rust 開発者は既存の Rust コードに対する仕様 (および証明) を Rust のソースファイルに直接追加できます。先ほどの二分探索の例を発展させて、探索関数の既存の Rust 実装に対する次の Verus 仕様 (Rust のアノテーションとして記述) を見てみましょう。

Rust のアノテーションとして記述された、探索関数の Rust 実装に対する Verus 仕様。

事前条件 (precondition) は requires キーワードで示され、関数の実行前に真でなければならない条件を記述します。この例ではコードが二分探索を実装しているため、配列がソート済みであることを要求します。事後条件 (postcondition) は ensures キーワードで示され、関数の実行後に真でなければならない条件を記述します。この例では、関数が Some(index) を返す場合に index が配列の範囲内にあり、そのインデックスにある配列要素の値が、探していた値と一致することを示しています。

重要なのは、関数が None を返す場合には目的の値が配列内に存在しないことも示している点です。この 2 つ目の条件がなければ、常に None を返す実装でも仕様を満たしてしまいます。なお、通常の Rust コンパイラはこれらの Verus アノテーションを無視します。そのため、Verus のアノテーションが付いたコードは、Rust のビルドツールである Cargo を使うプロジェクトを含め、検証済みのプロジェクトでも未検証のプロジェクトでも利用できます。

この例は、Verus が採用している重要な設計上の判断も示しています。これは、他の多くの Rust 検証手法とは異なる点です。Verus では、開発者が Rust に似た構文を使い、自分のソースコード内に仕様と証明を記述します。証明が失敗すると、ソースレベルで表現された Rust スタイルのエラーメッセージが表示されます。このアプローチにより、証明と実際のコードの同期が保たれ、開発者は仕様や証明のためにまったく新しい言語やツールを学ぶ必要がなくなります。また、コードを書いた開発者、つまりそのコードを最もよく理解している人が、正しさを証明するプロセスにかかわることができます。

Verus は、高速で強力な自動化にも力を入れています。そのために、さまざまなソルバー (solver) を使用して、プログラムとその仕様から生成される証明義務 (proof obligation) を解消します。実際には、開発者は通常 1 秒未満でコードと証明に関するフィードバックを得られます。これは、対話的な開発ループ (VS Code のような対話的な開発環境に表示される「赤い波線」を含む) を実現できるほどの速さです。

プロジェクト単位で見ると、Verus は数千行のコードと証明を含む複雑なプロジェクトを、従来の一部の自動プログラム検証ツールが個々の関数を検証するのに要していた時間で検証できます。この強力な自動化と高速なフィードバックループは、人間に有用なのは言うまでもなく、AI エージェントが Verus の証明を作成する際にも役立ちます。自動化が進んでいればエージェントの作業は少なくなり、証明の修正と検証をよりすばやく繰り返せるからです。

Rust の型システムは強力な安全性保証を提供しますが、開発者が高性能なコードを書くうえで足かせになる場合もあります。そのため Rust では、明示的に unsafe とラベル付けしたコードも書けます。この unsafe コードも、Rust が安全なコードに求めるすべての要件を満たす必要がありますが、コンパイラはそれらの要件を機械的に検査しなくなります。正しく実装する責任は開発者に委ねられます。しかし Verus を使えば、unsafe な Rust コードの安全性を数学的に証明でき、機械的に検査された安全性保証を取り戻せます。

同様に Rust は「恐れ知らずの並行性 (fearless concurrency)」で知られています。これは、開発者が並行コード、つまり少なくとも一部が並列に実行されるプログラムを書くときに、他のプログラミング言語では許容されてしまうさまざまな誤りを型システムが防ぐという意味です。Verus はこの基盤の上に構築されており、開発者は並行コードが安全であるだけでなく正しいことまで証明できます。

例えば、並行実行には一般にロックが用いられます。ロックは、プロセッサスレッドが現在操作しているデータ項目への排他的アクセスを与えるものです。Verus では、開発者がロックに不変条件 (invariant) を付与できます。つまり、ロックを取得した側はその不変条件を満たす値を得られ (例えば、その値は常に偶数である)、ロックを解放するときには、ロックで保護されている値がその不変条件を依然として満たしていることを証明しなければなりません。さらに Verus は、ロックの実装そのものが正しいことの証明もサポートします。これは、高いパフォーマンスを実現するために複雑なカスタムロック方式に依存する Nitro Isolation Engine のようなプログラムでは特に重要です。

すべてのプログラム検証ツールと同様に、Verus の保証は次の要素が正しいことに依存します。Verus 自体、プログラムの意図された振る舞いを記述した「最上位」の仕様、基盤となるランタイム (Rust 標準ライブラリなど) に関する「最下位」の仮定、そしてソースコードを実行可能なプログラムへ変換するコンパイラのツールチェーンです。今後の記事では、これらのコンポーネントの正しさに対する確信をどのように高めているかを詳しく説明します。

オープンソースエコシステムにおける Verus

Verus は Amazon での利用に加えて、さまざまなオープンソースプロジェクトで興味深い性質を証明するために使われています。以下にいくつかの例を挙げます。

• Vest は、バイナリデータ形式の記述を受け取り、その形式のデータを解析およびシリアル化する Rust コードを自動生成します。生成物には、正しさとセキュリティに関する Verus の証明も含まれます。
• Verdict は、X.509 公開鍵暗号標準に対応した、正しさと安全性が証明された証明書検証ライブラリを提供します。ユーザーが指定した検証ポリシーもサポートします。
• CapybaraKV プロジェクトは、永続メモリログ (persistent-memory log) の正しさとクラッシュ安全性を検証します。永続メモリログは、システムがクラッシュしたり予期せず電源を失ったりしても、データを整合性のある状態で保持します。
• Atmosphere マイクロカーネルは、Rust で開発され、Verus によって正しさが検証されたマイクロカーネル (最小構成のオペレーティングシステム) です。
• Anvil は、クラウドコンピューティングを管理するオープンソースシステムである Kubernetes のコントローラーについて、正しさと「活性 (liveness)」を証明します。妥当な仮定の下で、コントローラーが最終的にシステムを安定した状態へ導くことを示します。
• CortenMM メモリ管理システムは、スケーラブルなロックプロトコルを備えた新しいトランザクショナルインターフェイスを提供しており、その並行コードの正しさは Verus で検証されています。

Verus 自体は、各地の学術界と産業界の研究者が協力して開発を進めている、無償のオープンソースプロジェクトです。

本ブログは Security Solutions Architect の 中島 章博 が翻訳しました。