Verusを用いた証明可能な正しいRustコードの開発

Verus を使った証明可能な正しい Rust コードの開発

Amazon を含む多くのオープンソースおよび業界のソフトウェアプロジェクトでは、Rust プログラミング言語が採用されています。これは、Rust が C プログラミング言語に似たパフォーマンスと柔軟性を提供し、その巧妙な型システムがさまざまなバグやセキュリティ脆弱性を自動的に防止するためです。その結果、平均よりも正確で安全な高速コードが生まれます。

しかし、「より正確で安全」であることは、「実際に正確で安全」であることと同じではありません。例えば、C 言語では、配列の境界外アクセス（割り当てられたメモリの境界を超えて配列にインデックスを付けること）は、予見不可能な結果をもたらす可能性のある危険な間違いです。Rust では、プログラムは停止しますが、本来、正しいプログラムは境界外アクセスを一切行わないはずです。同様に、Rust はプログラムが期待通りの結果を計算することや、アクセス可能な秘密情報を漏洩しないことを保証できません。そこで Verus の出番です。

配列の境界外アクセスは、予見不可能な結果をもたらす可能性のある危険な間違いです。正しいプログラムであれば、それを許容しないはずです。

Verus とは何か？

Verus は、Rust 用のオープンソースの自動プログラム検証ツールです。「プログラム検証ツール」とは、コードがどのように動作すべきかについての数学的な形式仕様を入力として受け取り、すべての可能な入力に対してコードがその仕様に適合しているかを機械的にチェックするものです。

例えば、コードは特定の値をソート済み配列内で検索するために最適化されたバイナリサーチアルゴリズムを実装しているかもしれません。仕様では、コードがインデックスを正常に返した場合、配列内の対応する要素がターゲット値と一致すると述べられているかもしれません。検証ツールは、この仕様がすべての可能な入力配列とターゲット値に対して成り立つことをチェックします。

対照的に、従来のテスト手法では、いくつかの特定の配列を試すことはできますが、コーナーケース（例えば、ターゲット値が配列の最後の要素である場合や、存在しない場合など）を見逃す可能性があります。プログラム検証の重要な側面は、コードが仕様に適合しているという数学的な証明を構築することです。Verus のような自動プログラム検証ツールでは、ツールが証明構築の退屈で低レベルなステップの多くを自動的に処理しますが、人間の開発者は高レベルのガイダンス（例えば、帰納的証明のセットアップやループ不変条件の供給）を提供します。以下で説明するように、最近では、これらの高レベルのステップさえも AI によって自動化できることがよくあります。

Amazon では、Rust Foundation の設立メンバーであることを誇りに思っており、Firecracker（AWS Lambda および AWS Fargate を支えるもの）、サーバーレス分散 SQL データベース、そして Amazon Web Services (AWS) の仮想マシン割り当てを管理するソフトウェアである Nitro ハイパーバイザーの仮想マシン分離を強制する Nitro Isolation Engine のようなプロジェクトで Rust を広範に使用しています。Rust に対する Amazon の熱意は、10 年以上にわたる自動推論の研究 と相まって、Verus を採用して記述している Rust コードにさらに強力な保証を与えることを自然なものにしています。実際、Nitro Isolation Engine で使用されている主要なプリミティブや、Amazon 内で使用されている多くの重要なインフラストラクチャの正確性を証明するために Verus を使用してきました。これらのユースケースについては、今後の投稿で詳しく説明しますが、まずは Verus を使って Rust コードを検証することの意味について、さらに詳しくお伝えしたいと思います。

Verus による Rust コードの検証

Verus を使用すると、Rust 開発者は既存の Rust コードに対して、Rust ソースファイル内に直接仕様（および証明）を追加できます。バイナリサーチの例を拡張するために、検索関数の既存の Rust 実装に対する以下の Verus 仕様（Rust アノテーションとして記述）を検討してください。

検索関数の Rust 実装に対する Verus 仕様（Rust アノテーションとして記述）。

前提条件（requires キーワードで示される）は、関数が実行される前に真でなければならない条件を述べます。この場合、コードはバイナリサーチを実装しているため、配列がソートされていることを要求します。事後条件（ensures キーワードで示される）は、関数が実行された後に真でなければならない条件を述べます。この場合、関数が Some(index) を返した場合、index は配列の境界内であり、そのインデックスの値が探している値と一致すると述べています。

重要なのは、関数が None を返した場合、ターゲット値が配列に存在しないことも示している点です。この 2 番目の節がないと、仕様は常に None を返す実装によって満たされてしまう可能性があります！通常の Rust コンパイラはこれらの Verus アノテーションを無視するため、Verus でアノテーションされたコードは、検証済みプロジェクトと未検証プロジェクトの両方で、Rust のビルドツールである Cargo を使用しているものも含めて、消費できます。

この例は、Verus が行う多くの他の Rust 検証アプローチとは一線を画す、重要な設計上の決定も示しています。Verus では、開発者が Rust ライクな構文を使用して、ソースコード内に仕様と証明を記述します。証明が失敗すると、ソースレベルで表現された Rust スタイルのエラーメッセージが表示されます。このアプローチにより、証明は実際のコードと同期したままになり、開発者は仕様と証明のために全く新しい言語やツールを学ぶ必要がなくなります。また、コードを書いた開発者（したがって、コードを最もよく知っている人）が、それを証明するプロセスに関与できるようになります。

Verus は、高速で強力な自動化を提供することにも重点を置いています。そのために、プログラムとその仕様から生成された証明義務を処理するために、さまざまなソルバーを使用しています。実際には、これは開発者が通常、コードと証明に関するフィードバックを 1 秒未満で得られることを意味し、インタラクティブな開発ループ（VS Code のようなインタラクティブ開発環境内で「赤い波線」が表示されることなど）を提供するのに十分な速度です。

プロジェクトレベルでは、Verus は、以前の自動プログラム検証ツールが個々の関数を検証するのにかかった時間で、数千行のコードと証明を持つ複雑なプロジェクトを検証できます。この強力な自動化と迅速なフィードバックループは、明らかに人間を助けますが、AI エージェントが Verus 証明を開発するのを助けることにもなります。なぜなら、自動化によりエージェントの作業量が減り、証明のイテレーションをより速く行えるからです。

Rust の型システムは強力な安全保証を提供しますが、時には開発者が高性能コードを書くことを妨げることがあります。そのため、Rust は開発者が明示的にラベル付けされた「unsafe」コードを書くことも許可しています。このコードは、依然として Rust の安全なコードに対するすべての期待を満たす必要がありますが、コンパイラはそれらの期待を機械的にチェックしなくなります。それを正しく行うのは開発者の責任です。しかし、Verus を使用すると、開発者は unsafe Rust コードの安全性を数学的に証明し、機械チェックされた安全保証を再確立できます。

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

例えば、並行実行には通常ロックが伴います。ロックは、プロセッサのスレッドに、現在操作しているデータ項目への排他的アクセスを許可します。Verus は、開発者がロックに不変条件プロパティを追加できるようにします。これは、ロックを取得した人が不変条件のプロパティを満たす値（例えば、値が常に偶数である）を取得し、ロックを解放する際には、ロックの後ろにある値が依然としてそのプロパティを満たすことを証明しなければならないことを意味します。さらに、Verus はロック実装自体が正しいという証明もサポートしています。これは、高いパフォーマンスを達成するために複雑でカスタムなロックメカニズムに依存する Nitro Isolation Engine のようなプログラムにとって特に重要です。

すべてのプログラム検証ツールと同様に、Verus の保証は、Verus 自体の正確性、プログラムの意図された動作の「トップレベル」仕様、基盤となる実行時（例えば、Rust 標準ライブラリ）に対して行われる「ボトムレベル」の仮定、そしてソースコードを実行可能プログラムに変換するコンパイラツールチェーンに依存します。今後の投稿では、これらのコンポーネントに対する信頼を高める方法について、さらに詳しく説明します。

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

Amazon での使用に加えて、Verus はさまざまなオープンソースプロジェクトで興味深いプロパティを証明するために使用されてきました。以下に例を挙げます。

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

Verus 自体は、学術界および産業界の研究者による分散コラボレーションによって開発された、無料のオープンソースプロジェクトです。