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

自動推論 Verusを用いた証明可能な正しいRustコードの開発 Verus "プログラム検証ツール"は、機能の数学的仕様に対してコードを自動的にチェックし、ソフトウェアプロジェクトにおけるセキュリティ保証の向上を支援します。Bryan Parno 著 2026年8月31日 7分 共有 リンクをコピー メール X LinkedIn Facebook Line Reddit QZone Sina Weibo WeChat WhatsApp 分享到微信 x 聞く • 10:11分 主要なポイント Verusは、Rust向けのオープンソース自動プログラム検証ツールであり、すべての可能な入力に対してコードを形式的な数学的仕様と照合して機械的にチェックします。これは、従来のテストを超えて、エッジケースを検出します。開発者は、Rustライクな構文を使用して、前提条件と事後条件をRustソースコードに直接注釈付けし、高速なフィードバックループ（1秒未満）を可能にし、AIエージェントが証明生成を支援できるようにします。Verusは、Rustの"unsafe"コードブロックとカスタムロッキングスキームを備えた並行コードの数学的検証を可能にし、AWSのNitro Isolation Engineのようなパフォーマンス重視の実装に対して、機械的にチェックされた安全性の保証を再確立します。Amazonは、クリティカルインフラストラクチャの主要なプリミティブの正確性を証明するためにVerusを使用しており、このツールは、証明書検証ライブラリ、データフォーマットパーサー、およびKubernetesコントローラーのような分散システムを含むオープンソースプロジェクトにも採用されています。この回答は役に立ちましたか？ Amazonを含む多くのオープンソースおよび業界のソフトウェアプロジェクトは、Rustプログラミング言語を採用しています。これは、Cプログラミング言語と同様のパフォーマンスと柔軟性を提供し、その巧妙な型システムがさまざまなバグやセキュリティ脆弱性を自動的に防止するためです。その結果、平均よりも正確で安全な高速コードが生まれます。しかし、「より正確で安全」は「実際に正確で安全」と同じではありません。例えば、C言語では、配列の境界外アクセス（割り当てられたメモリの境界を超えて配列にインデックスを付けること）は、予見不可能な結果をもたらす可能性のある危険な間違いです。Rustでは、プログラムは停止しますが、これは明らかに安全ですが、正しいプログラムはそもそも境界外アクセスを実行することはありません。同様に、Rustはプログラムが期待通りの結果を計算することや、アクセス権を持つ秘密情報を漏洩しないことを保証できません。そこでVerusが登場します。配列の境界外アクセスは、予見不可能な結果をもたらす可能性のある危険な間違いです。正しいプログラムはそれを許可しません。Verusとは何か？ Verusは、Rust向けのオープンソース自動プログラム検証ツールです。「プログラム検証ツール」は、コードがどのように動作すべきかの形式的な数学的仕様を入力として受け取り、すべての可能な入力に対してコードがその仕様に一致するかどうかを機械的にチェックします。例えば、コードは特定の値をソート済み配列内で検索するために最適化されたバイナリ検索アルゴリズムを実装しているかもしれません。仕様では、コードが正常にインデックスを返した場合、配列内の対応する要素がターゲット値と一致すると述べられているかもしれません。検証ツールは、この仕様がすべての可能な入力配列とターゲット値に対して成り立つかどうかをチェックします。対照的に、従来のテスト手法では、いくつかの特定の配列を試すことはできますが、エッジケース（例えば、ターゲット値が配列の最後の要素である場合や、存在しない場合など）を見逃す可能性があります。プログラム検証の重要な側面には、コードが仕様に一致することを示す数学的証明の構築が含まれます。Verusのような自動プログラム検証ツールでは、ツールが証明構築の多くの退屈で低レベルなステップを自動的に処理する一方、人間の開発者は高レベルのガイダンス（例えば、帰納的証明の設定やループ不変条件の供給）を提供します。以下で議論するように、最近では、これらの高レベルのステップさえもAIによって自動化できることがよくあります。Amazonでは、Rust Foundationの設立メンバーであることを誇りに思っており、AWS LambdaとAWS Fargateの基盤となっているFirecracker、分散SQLデータベース、およびAmazon Web Services（AWS）の仮想マシン割り当てを管理するソフトウェアであるNitroハイパーバイザーの仮想マシン分離を強制するNitro Isolation EngineなどのプロジェクトでRustを広く使用しています。AmazonのRustへの熱意と、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"コードブロックの安全性を数学的に証明できます。