RustのcoreおよびallocクレートをCoqへ翻訳して形式検証

 (formal.land)
1 ポイント 投稿者 GN⁺ 2024-05-16 | 1件のコメント | WhatsAppで共有
  • RustプログラムをCoqに移すcoq-of-rustが、標準ライブラリのcore・allocクレートまで扱い始めたことで、primitive関数ごとにCoq定義を手作業で書いていた負担を減らしつつある
  • 2つのクレートはunsafeや高度なRustコードが多い大規模コードベースであり、自動翻訳結果をコンパイル・検証可能な単位として扱うことが中核的な課題となった
  • 出力を入力Rustファイル単位に分割すると、allocは54ファイル171,783行、coreは190ファイル592,065行となり、並列コンパイルとデバッグがしやすくなった
  • implブロックのモジュール名衝突はwhere句の情報を含めることで緩和したが、現時点でもCoqでコンパイルできないファイルは全体の4%残っている
  • Option::unwrap_or_defaultの例では、自動翻訳された定義と単純な関数型定義の同値性を証明して利用する方式であり、自動化への信頼と証明時の検査の両方が必要になる

Rust標準ライブラリのprimitive処理

  • Formal Landは、RustプログラムをCoq形式証明システムへ翻訳するcoq-of-rustを開発中
  • 従来は、Rust標準ライブラリのprimitive構成要素を扱うために、関数ごとに動作を表すCoq定義を別途作る必要があった
  • この負担を減らすため、Rustのcoreおよびallocクレートをcoq-of-rustで翻訳した
  • 翻訳結果は次のパスで確認できる

初回翻訳の実行結果

  • coq-of-rustをallocとcoreに初めて実行すると、各クレート全体に対応する数十万行規模のCoqファイル2つが生成された
  • 大規模コードベースでもツールが動作することは確認できたが、生成されたCoqコードはそのままではコンパイルできなかった
  • エラーはまれだったものの、数千行ごとに1件程度発生する水準だった
  • cloc基準での入力Rustコード規模は次のとおり
    • alloc: Rustコード26,299行
    • core: Rustコード54,192行
  • 翻訳過程ではマクロ展開が起こるため、実際の翻訳対象は元の行数より大きい

生成されたCoqコードの分割

  • 最大の変更は、coq-of-rustの出力を入力Rustファイル1つにつきCoqファイル1つに分けたこと
  • この分割は、翻訳が定義順序に鈍感でcontext-freeだから可能だった
  • Rustファイル間には通常循環依存があるが、Coqではそれを許容しない。それでもこの翻訳方式ではファイル単位の分離が可能だった
  • 分割後の出力規模は次のとおり
    • alloc: Coqファイル54個、Coqコード171,783行
    • core: Coqファイル190個、Coqコード592,065行
  • ファイルを分けることで、生成コードの探索と保守が容易になった
    • コンパイルを並列化しやすい
    • 1ファイルずつ集中してデバッグできる
    • コンパイルできないファイルを除外しやすい
    • 単一ファイルのdiffを追跡しやすい

モジュール名衝突の修正と残るファイル

  • 一部のバグはimplブロックのモジュール名衝突に起因していた
  • 解決方法は、モジュール名により多くの情報を入れて一意性を高めることだった
    • 従来は欠けていたwhere句の情報を含めた
    • たとえばMapping<K, V>に対するDefaultトレイト実装では、KとVの両方がDefaultを実装していなければならないという条件がモジュール名に反映される
  • 現在Coqでコンパイルできないファイルは次のとおり
    • alloc/boxed.v
    • core/any.v
    • core/array/mod.v
    • core/cmp/bytewise.v
    • core/error.v
    • core/escape.v
    • core/iter/adapters/flatten.v
    • core/net/ip_addr.v
  • これは全ファイルの**4%**に相当する
  • コンパイルできるファイルの中にも、まだ処理できていないRust構成要素が公理化されているため、この比率だけで未サポート範囲の全体を判断するのは難しい

Option::unwrap_or_default翻訳の例

  • RustのOption::unwrap_or_defaultは、Some(x)ならxを返し、NoneならT::default()を呼び出す
  • coq-of-rustはこれをモナディック形式のCoq定義へ翻訳する
    • 入力引数と型をマッチさせる
    • Some分岐ではtuple fieldを取り出してコピーする
    • None分岐ではcore::default::Defaultトレイトのdefaultメソッドを呼び出す
  • 実際の検証では、自動生成された定義の代わりに、より単純な関数型定義を使う
    • Noneならcore.simulations.default.Default.defaultを返す
    • Some xならxを返す
  • 自動生成定義と単純定義が同値であることの証明はCoqOfRust/core/proofs/option.vにある
  • 元のRustコードが変われば、この証明を通じて変更が検出される
  • coreライブラリの翻訳は自動で行われたため、手書きの定義より生成定義のほうが信頼できる
  • ただしcoq-of-rust自体にも誤りや不完全さがありうるため、証明時点でコードが妥当か確認する必要がある

今後の課題

  • Rustプログラム検証において、標準ライブラリ形式化への信頼性は高まった
  • 次の目標は、依然として退屈な証明過程の単純化である
  • 特に、シミュレーションが元のRustコードと同値であることを示すには、次の作業が必要になる
    • 名前解決
    • 高水準型の導入
    • 副作用の除去
  • これらの段階を分けて扱うことが、今後の改善の方向性となる

関連記事

1件のコメント

 
GN⁺ 2024-05-16
Hacker News のコメント

  • 本当に印象的。
    このような自動翻訳は、信頼の対象をツールへ移すことになる。coq-of-rust 自体は Coq ではなく Rust で書かれているので、その再帰的な構造はかなり驚きだが、David A. Wheeler の “Countering Trusting Trust through Diverse Double-Compiling” (2009) [0] のように、2つ目のコンパイラで Ken Thompson の Trusting Trust 攻撃を回避する方法に、CompCert 的なアプローチを組み合わせれば、正しさの証明は可能に見える。
    検証するには、coq-of-rust で coq-of-rust 翻訳器を Rust から Coq に変換する。その翻訳は Rust で行われたものなので信頼しないとしても、Coq の中で望む正しさの性質、特に Rust プログラムを Coq に翻訳するときに意味論を保存することを証明すればよい。
    論文のように、生成された定義よりも関数型寄りの定義で証明するほうが簡単な可能性が高いので、標準ライブラリで行っているように定義間の同値性を証明する手順を踏めばよい。現在の coq-of-rust 翻訳器、特に lib/ [1] が Rust 6,350行なら、翻訳器全体を Coq で書き、生成されたものと同値であることを証明するのも現実的に見える。
    次に、証明済みの Coq 版 coq-of-rust 翻訳器を Rust 製の coq-of-rust ソースに対して実行すると、出力される Coq 定義は、最初に使った Rust 版 coq-of-rust 翻訳器の出力と一致するはずだ。
    余談だが、こうした取り組みに産業界の資金が付くのは良いことだと思う。暗号資産には冷笑的なほうだが、あちらの正確性への要求が Rust、Coq、知り合いの修士課程の学生への支援といった、自分の関心領域の改善を後押ししているのは事実だ。
    [0]: https://dwheeler.com/trusting-trust/wheelerd-trust.pdf
    [1]: https://github.com/formal-land/coq-of-rust/tree/main/lib

    • 著者の一人だが、実際にそうした手順は coq-of-rust の検証にとって良い方法になり得る。
      ただし、コード自体は短くても、入力の Rust コードをパースして型検査する部分は Rust コンパイラに依存している。したがって、その部分も検証するか、少なくとも証明抜きでも形式仕様を与える必要がある。rustc の API がかなり大きく不安定である点は障害だが、それでも信頼性を高める一つの方法にはなり得る。
    • 以前 SPARK Ada で働いていた頃を思い出す。サポート対象の Ada ターゲットがないプロジェクト、特に非常に小さなデバイスでは、Ada を C に変換してからそのターゲット向けにコンパイルすることがよくあり、そのおかげで SPARK 側でさまざまな形の静的解析を行えた。
      もちろん、出力物や変換器を検証しなければならない問題は生じたが、生成された C コードは検証目的ではかなり読みやすく、スタイルも制限されており、ツールへの信頼度も高かった。SPARK の静的解析は検証・確認プロセス全体の一部であり、テストや他の活動が追加の信頼層を提供していた。全体としては、かなりうまく機能したアプローチだった。
    • 暗号資産がこうしたことを助けている理由は、正確性の制約もあるが、コンピュータサイエンスに関心のある人々へ多くの富が移転したことも大きい。
      彼らがそのお金をコンピュータサイエンス研究に使うのは、自分たちの利益になるからだけでなく、趣味とつながった慈善活動でもあるからだ。
    • そのアプローチが、バイナリを作るのに使われる Rust コンパイラによる悪意あるペイロードの注入をどう防ぐのかはよく分からない。A を B でビルドし、B を A でビルドしてからバイナリを比較することはできるかもしれないが。
      別のアプローチは proof-carrying code だ。Rust コンパイラが、実行ファイルの出力が入力ソースコードの意味論と一致するという Coq 証明を一緒に出力する方式である。
      もちろん、Rust のサブセットコンパイラを、例えば借用チェッカや最適化なしで特定アーキテクチャの機械語として書き、そこからすべてをブートストラップすることもできる。

  • Coq のような半自動演繹証明システムで最初から最後まで検証されたプログラムの規模は小さい。ライブラリはコード同士の相互作用の度合いが低いので簡単かもしれないが、一般のプログラムはそうではない。
    実際、この方法で検証可能なプログラム規模の増加は、プログラム全体の平均規模の増加よりも遅かった。健全なソフトウェア検証、つまり仕様と100%一致することを示す作業は、核心的アルゴリズムの正しさ証明のような場面では確かに有用だが、うまくスケールしない。
    そのため、研究が非健全な方法へ移っていった面がある。100%保証のコストが 99.9999% 保証の10倍になることもあり、その確率差はソフトウェア以外の故障確率より小さくなる場合もある。物理システムはそもそも仕様と一致することを証明できず、仕様自体が現実と十分に合っていない確率もある。

    • 重要なのは、標準ライブラリの unsafe 部分と Rust の安全性保証を証明すれば、標準ライブラリだけを使うすべての安全な Rust コードについて、メモリ安全性やデータ競合がないことなどを推移的に証明できるという点だ。
      unsafe コードだけが正しいと証明するのは、すべての Rust コードを証明するよりはるかに少ない労力で可能だ。これは、Rust の安全性保証を語るときによく出る「unsafe コードはどうするのか」という批判への答えになる。Rust の型システムだけでは扱うのに十分強力でない隙間を、Coq のようなより強力なシステムで埋められる。

  • こうした試みでよく理解できない点がある。コードを Coq に手作業または半手作業で変換しなければならないなら、その過程でミスをする可能性のほうが、形式検証で得られる利点よりはるかに大きいのではないか？
    言い換えると、私たちが証明したことが依然として元のコードに対して有効だと、どうやって分かるのか？

    • 分からない。結局のところ、ハードウェア、コンパイラ、仕様、Coq の信頼カーネルなど、何かを信頼しなければならない
      形式検証はバグの可能性を完全になくすもののように語られることが多いが、実際にはバグの可能性を大幅に下げるものに近い。それでも Rust と Coq の間の自動翻訳は、信頼しなければならないものの複雑さを大きく減らすため、手作業の翻訳より好まれるべきだ
    • 妥当な限界ではあるが、それほど悪い限界ではない
      多くの場合、翻訳のバグは単に証明を不可能にする。そうなれば、誰かがなぜ証明が通らないのかを調べるうちに翻訳バグを見つけることになる
      本当の問題は、翻訳バグが元のコードのバグを正確に相殺する場合だ。体系的なリスクがないなら、2つのバグがこのように互いを打ち消す可能性はかなり低い
    • コードは coq-of-rust で自動翻訳される。翻訳で問題が見つかった場合は、coq-of-rust ツール側で一度修正すればよく、すべての翻訳結果が更新される

  • 関心のある読者へ：このブログ記事は、同じブログの他の記事より暗号資産関連の内容が直接的ではないため投稿したが、そこには技術的にもっと興味深い記事が多い
    特に最近の2本の記事は、同じアプローチを Rust ではなく Python に適用する内容を扱っている

  • 以前、形式検証された C コンパイラでファザーがバグを見つけたという講義 [1] を思い出す。形式検証がフロントエンドとバックエンドを含んでいなかったためだった
    Coq 自体や翻訳をどれほど信頼できるのかという疑問が出るのも分かるし、Rust の更新とどう同期するのかも疑問だが、完全な形式検証でさえ最初から最後まで 100% の正確性を意味するわけではない
    [1] https://youtu.be/Ux0YnVEaI6A

  • 形式検証の専門家ではまったくないが、Rust の基本ライブラリが形式検証され、unsafe コードを使わないなら、形式検証されたライブラリを使うすべての Rust プログラムは、メモリ処理の面では実質的に形式検証レベルの品質を持つことになるのだろうか？

    • Rust の安全性はバグとはほとんど関係がない
      Rust には独自の “safe” の定義があり、これはメモリ安全性の部分集合と見なせる。完全に安全な Rust コードでも、データ競合、デッドロック、メモリ枯渇などは起こり得るし、論理エラーは言うまでもない
    • ある程度はそれが理想だと思うが、ただし書きは多く、いくつかの条件がそろう必要がある
      第一に、unsafe Rust の意味論を形式化する必要がある。Ralf Jung による先駆的な RustBelt[1] の仕事は大きな進展だったが、まだ完全ではない。特にポインタの来歴が厄介な要素として明らかになっている
      第二に、その一部として借用チェッカーの形式モデルが必要になる。Stacked borrows[2] は良い試みだったが欠陥があり、Tree borrows[3] がそれを修正するかもしれないものの、さらに洗練された何かが出てくる可能性もある
      第三に、形式的なメモリモデルが必要だ。これは主にアトミック操作と同期の振る舞いに関するものであり、したがって Arc のような標準ライブラリの構成要素にとって非常に重要だ。Rust のメモリモデルは C++ と似ており、相互運用できるべきだという点は広く受け入れられているが、“out of thin air” 問題や seqlock のような欠けている機能が残っている。Linux カーネルが今も独自モデルを使っている理由の一つでもある
      第四に、安全性の保証がうまく合成されることを証明する必要がある。特に、unsafe Rust で書かれた健全なコードと safe Rust コードを合成しても、安全性の保証が維持されなければならない。これまで良い結果はあるが、システム全体について証明される必要がある
      第五に、そのような証明がすべてのコードに対して成り立つには、Rust に残っている健全性バグ[1]をすべて閉じる必要がある。こうした問題の多くは理論的なもの、あるいは敵対的なコード[5]でのみ実際に重要になるため、進捗は遅い
      これらすべてが終わっても、なお部分的な保証にすぎない。システムと接続する表面の非常に大きな部分が unsafe コードに基づいている。純粋な計算だけをするならともかく、例えばグラフィカル UI を作るなら、依然としてうまくいかない可能性のあるものは非常に多い
      それでも実用的な前進の道はあり、それは今日の脆弱性だらけのシステムという一般的な状態より、はるかに良い状況につながる
      [1]: https://people.mpi-sws.org/~dreyer/papers/rustbelt/paper.pdf
      [2]: https://plv.mpi-sws.org/rustbelt/stacked-borrows/
      [3]: https://www.ralfj.de/blog/2023/06/02/tree-borrows.html
      [4]: https://github.com/rust-lang/rust/issues?q=is%3Aissue+is%3Ao...
      [5]: https://github.com/Speykious/cve-rs
    • Rust の専門家ではないが、core のコードには unsafe がかなり多いように見える。そうなるのも当然だ
      https://github.com/search?q=repo%3Arust-lang%2Frust+unsafe+l...
      ここで示されている方法の Coq が、すべての unsafe 呼び出しを検証できるとは思わない

  • このアプローチは Aeneas や RustHornBelt とどう違うのか比較できますか？ポインタと可変借用はどう扱いますか？

    • RustHornBelt がどう動作するのかは分かりません。私たちは安全なコードに集中していますが、unsafe ブロックについても「ベストエフォート」で翻訳は生成します。
      Aeneas と比較すると、目標は非常に似ています。どちらも対話型定理証明器で Rust プログラムを検証しようとしているからです。ただし coq-of-rust では、証明対象となる純粋関数型バージョンのコードを手作業で書くか、反復的な作業なので GitHub Copilot の助けを借りて書き、それが自動翻訳結果と等価であることを証明します。Aeneas は関数型バージョンを直接生成することを目指しています。
      ポインタはすべて可変ポインタ、つまり * 型であるかのように扱います。Rust の借用チェッカー情報は使わず、そのおかげで翻訳は単純になりますが、そのコストは証明時に支払います。
      証明でポインタを推論するために、ユーザーがメモリの使われ方に応じて設計できるカスタムアロケータを提供できるようにしています。たとえばプログラムがグローバル可変変数を 3 つ使うなら、メモリを 3 項目を持つレコードにできます。これらの項目は、まだ割り当てられていない状態を表すため、最初は None です。
      この手法がどれほどスケールするかはまだ分かりませんが、少なくとも現時点では分離論理による推論を避けられます。検証したいプログラムの大半、特にアプリケーション側は、比較的「単純な」メモリ規律を持つことを期待しています。

  • 形式検証の仕様を書くのは、より複雑な プロパティベーステスト を使うのと似ていますか？複雑でないプログラムを超えると、プロパティベーステストを書くのもかなり難しく時間がかかるものですが。

    • 似ていますが、常に同じではありません。プロパティベーステストでは通常、システムのインターフェース、関数やプロシージャのレベル、またはそれより高いレベルで入力の記述を指定し、出力があるプロパティまたはプロパティの集合を満たすかをテストします。
      同じレベルで形式検証を行う場合も、かなり似て見えることがあります。しかし形式検証ツールはさらに深く踏み込めます。たとえば計算内部のシステム状態について、「このループ不変条件があるが、すべての反復で実際に維持されることを証明できるか？」あるいは「この計算中、どの中間計算でもアンダーフロー／オーバーフローが絶対に発生しないことを証明できるか？」といった問いに答えられます。
      前者は、ループの中核を別のプロシージャとして切り出し、多くの中間状態で実行して不変条件のプロパティをテストすれば、プロパティベーステストでも可能です。後者は、プログラムを行単位で個別に実行可能にするほど極端に分割しない限り、はるかに難しいです。

  • こういうことが可能だとは知りませんでした。
    こうした試みが、カーネル導入の重要部分で Rust 採用 を加速させられるのか気になります。

  • 誰か「検証」という概念をとても簡単に説明してもらえますか？なぜこの目的だけのために Coq のような言語全体が存在するのか、そしてより広い社会にどんな実質的な意味があるのか気になります。