Rust検証技術、低レベルなシステムコードに適用

 (github.com/verus-lang)
1 ポイント 投稿者 GN⁺ 2024-05-06 | 1件のコメント | WhatsAppで共有
  • VerusはRustで書かれたコードの正しさを検証するツールで、開発者がコードが果たすべきことを仕様として記述すると、実行可能なRustコードがあらゆる実行でその仕様を満たすかを静的に確認する
  • ランタイム検査を追加せず、強力なソルバーを使ってコードが正しいことを証明する方式で、現在はRustの一部のみをサポートしている
  • 一部のケースでは、標準のRust型システムを超えて、raw pointerを操作するコードの正しさまで静的に検査できる
  • プロジェクトは活発に開発中であり、機能が壊れていたり不足していたりする場合があり、ドキュメントもまだ完全ではないため、利用者はZulipで助けを求める準備が必要
  • ブラウザ向けのVerus Playground、インストール案内、チュートリアルとリファレンス、標準ライブラリAPIドキュメント、並行コード検証ガイド、サンプルとテストが学習・実験の導線として提供されている

Verusが検証するもの

  • VerusはRustコードの正しさを検証するツール
  • 開発者はコードが実行すべき動作を仕様として記述する
  • Verusは、実行可能なRustコードが可能なすべての実行でその仕様を常に満たすかを静的に検査する
  • ランタイム検査を追加する代わりに、ソルバーを使ってコードが正しいことを証明する
  • 現在の対応範囲はRustのサブセットで、対応範囲を広げる作業が進められている
  • 一部のケースでは、標準のRust型システムを超えて、たとえばraw pointerを操作するコードの正しさを静的に確認できる

開発状況と利用時の注意点

  • Verusは活発に開発中のプロジェクト
  • 機能が壊れていたり不足していたりする場合がある
  • ドキュメントはまだ完全ではない
  • Verusを試すには、Zulipで助けを求める準備が必要
  • Verusコミュニティは複数の研究論文を発表しており、産業界と学術界のさまざまなプロジェクトがVerusを利用している
  • 関連一覧はpublications and projectsページで確認できる

始め方と開発ツール

  • ブラウザでVerusを試すには、Verus Playgroundを利用できる
  • より本格的な開発には、インストール案内に従う必要がある
  • 学習は Tutorial and referenceから始められる
  • Verusコード向けの自動フォーマッタverusfmtもサポートしている

ドキュメントと学習資料

サンプルとコミュニティ参加

  • Verusの利用例は、ドキュメント以外にも複数の出発点を提供している
    • Publications and projects: Verusを利用する出版物とプロジェクト
    • Videos, slides, and exercises: 1日版Verusチュートリアルの動画、スライド、演習問題
    • Standalone examples: 小さく具体的なタスクでVerusを使う独立したサンプル
    • Small and medium-sized examples: さまざまなVerus機能を示すサンプル
    • Unit tests: Verusの構文と機能の例を含むテスト
  • イシュー報告と議論はGitHubまたはZulipで行える
  • 機能要望とオープンな対話にはGitHub discussionsを使い、既存機能の再現可能なバグはGitHub issuesに置くという運用を採っている
  • コードで貢献したい場合は、Verusへの貢献の案内を参照できる

関連記事

1件のコメント

 
GN⁺ 2024-05-06
Hacker News の意見

  • Verus で形式検証済みの Kubernetes コントローラーを書いてみた
    基本的には「いつかコントローラーがクラスタを要求された目標状態へ調整する」といった ライブネス性質を証明できる
    ただし目標状態が素早く変わる場合、非同期性、失敗などを考えると、「正しさ」を仕様化すること自体にも微妙な点が多い
    コード: [https://github.com/vmware-research/verifiable-controllers/](https://github.com/vmware-research/verifiable-controllers/）、関連論文は OSDI 2024 に掲載予定

    • 単体テストより何を多くしてくれるのか気になる

  • Verus へ進む小さな足がかりとして、Rust の debug_assert を事前条件と事後条件に付けてみることができる
    Rust コンパイラはデフォルトでプロダクションビルドではこれを取り除く
    Verus チュートリアルの検証例では requires と ensures で入力範囲と結果条件を書き、ランタイム検査版では debug_assert(-16 <= x1)、debug_assert(x8 == 8 * x1) のように同じ条件を実行中に確認する形になる

    • 現在の Verus 構文の一つの問題は、コード全体を手続きマクロで包む必要がある点
      Creusot のような他の Rust 向け証明/検証/契約式設計ツールは属性ベースの構文を使っており、一般により軽量で Rust らしく感じられる
      将来の Verus リリースでこうした方式も可能になるとよい
    • こういう assert をもっと多くの人が使うとよいと思う
      ドキュメント化ツールとして優れていて、型システムとテストを非常によく補完する
    • "contracts" クレートも試せる: https://docs.rs/contracts/latest/contracts/
    • Verus の例は、自分が Clojure コードを書くやり方に似ている
      ほとんどの関数に 事前条件と事後条件を付け、JVM にはプロダクションビルドでそれらを簡単に取り除けるフラグがある

  • 実際のコンピューターサイエンス経験が多くない立場として気になるのだが、README の「コードの正しさを検証する」における 検証と、他の場所で言う「証明」は何が違うのか？
    コンピューターサイエンス/数学の背景が強くない実務プログラマーが、コードについて「証明」を学ぶのに良い資料も知りたい
    さらに ゼロ知識証明がなぜそれほど重要で関連性が高いのかもよく分からない。たとえば x.com/ZorpZK のような話を聞いたが、なぜすごいのか理解できない

    • コード検証と関数型プログラミングを一緒に学ぶのに良い資料として Software Foundations がある: https://softwarefoundations.cis.upenn.edu
      ただし Verus と Software Foundations で使う Coq はアプローチが異なる
      Verus は SMT ソルバーという自動制約解決システムで性質を自動証明しようとし、Coq ははるかに多くの部分を手作業で証明する必要があり、自動化は限定的
      どちらにも長所と短所があり、自動化はうまくいくときは良いが、うまくいかないときはもどかしい
      ゼロ知識証明は少し別分野と見るのが妥当で、形式検証/証明の仕事をしている多くの人もゼロ知識証明には手を出していない。暗号学のプリミティブとして考えるほうがよい
    • ここでは 検証と 証明を同義語として使っており、最初の段落の後半でもそのことが明確になる
      ゼロ知識証明はオーバーヘッドが大きく、いわゆる「キラーアプリ」が不足しているため、実用的な用途や重要性、関連性はまだ大きくないが、概念としては興味深い
    • この文脈では「検証」と「証明」は同じ
      学習資料は自分もあればよいと思う。Dafny の文書はかなり良いが、形式的ソフトウェア検証はコンピューターサイエンス/数学の博士でない普通のプログラマーが使いやすい段階には、まだ達していないように思う
      例だけ見ると比較的簡単そうに見えるが、すぐに「証明できない」にぶつかり、その理由への答えは作者だけが知っていそうな深い実装詳細に入りがち
    • 自分の理解では、ゼロ知識証明は、何かを知っているという事実を、その内容を明かさずに証明できるようにする
      たとえばパスワードをサーバーに送らずにパスワードを知っていることを検証できるため、悪意あるサーバーや中間者攻撃者がパスワードを盗み見るのが難しくなる
      身元確認にもより良い選択肢を与えられる。政府発行の身分証を持っていることを証明しつつ、文書そのものをサーバーに渡さなくてよいので、「最大2年/3年/6か月保管」した末に結局流出する事態を減らせる
    • 「実務プログラマーがコードについて証明する」という表現は、まだ矛盾に近いと思う
      コードに関する証明は、まだ実務プログラマーが行うものではない
      Hoare 論理が良い出発点で、入門のコンピューターサイエンス授業でも時々教えられる
      Coq は学習曲線が急で、OCaml や似た言語に慣れていないと特に難しい。Why3 のほうが初心者にやさしいかもしれない: https://www.why3.org
      証明と検証は同じ意味の場合もあるが、証明はより対話的な印象で、検証はモデル検査や注釈付きプログラムの SMT 解決のように自動化できる印象がある

  • 似たプロジェクトを知らなかった人向けに言うと、Dafny は Rust にコンパイルできる「検証を意識したプログラミング言語」: https://github.com/dafny-lang/dafny

  • 本当に素晴らしく見える。既存のコードベースに証明を追加する方法についてのガイドや例があると、人々の役に立ちそうだ。
    例えば、テキストボックスが1つだけある最小限のGUIアプリが、HTTPリクエストでコンパイル時には分からず信頼できない配列を受け取り、バブルソートしてから表示するとしよう。
    バブルソートにはオフバイワンエラーで最後の要素がそのまま残るような意図的なバグがあり、単体テストはたまたまそのバグを見逃す。テストが不完全かもしれないと心配することが、証明へ向かう主な動機になり得る。
    そのうえで、単体テストを証明に置き換えながら、バグを発見して修正する過程を見せるとよさそうだ。
    証明コードそのものを詳しく説明する必要はなく、証明された数学的コードと証明されていない入出力コードの境界、証明とビルドに使うコマンドライン、実際に触れるzipアーカイブのような現実的な細部に焦点を当てればよい。
    実際のところ、標準入力から読み込み標準出力に書き出す程度でも十分そうだ。

  • 主要な貢献者の1人が、Zürich RustミートアップでVerusについて素晴らしい発表をしていた: https://www.youtube.com/watch?v=ZZTk-zS4ZCY
    この「ghost」コードがプログラム内にどれほどきれいに収まっているかが印象的で、Adaを少し思い出した。

  • RustにもC/C++、Common Lisp、Ada/SPARK2014のような標準がすでにあるのか気になる。
    そうしたものがないなら、Ada/SPARK2014向けに開発された検証ツールと比べると、動く標的を相手にすることになる。
    ベアメタルから高整合性の安全必須アプリケーションまで続くAda/SPARK2014の遺産も無視しにくい。

  • これとKaniの間にどんな関係があるのか気になる。互いに違う動き方をするのだろうか？
    https://github.com/model-checking/kani

    • モデル検査器は通常、限られた数の状態だけを探索するため、バグ発見に効率的で、プログラムに追加の注釈が不要な場合も多い。
      Verus、Dafny、F*、そして私のVCCのような自動SMTベースの検証器は、ほぼすべての関数とループに注釈を付ける必要があるが、プログラムの正しさについてより広い保証を提供する。
      CoqやLeanのような対話型証明器ベースのツールは、通常ユーザーによる誘導がより多く必要だが、より複雑な性質まで保証できる。

  • VerusはSPARKとどう比較されるのか気になる。
    同じ一般的な分類の検証器なのだろうか？ Ada用の検証器ではなくRust用の検証器である点以外に、Verusはどう違うのか？

  • Verusに詳しい人が、VerusとLean4の性能と表現力の違いを説明してくれるとありがたい。
    VerusはSMTベースの検証ツールで、Leanは対話型証明器であると同時にSMTベースのツールでもある、と理解している。
    ただし形式検証分野への理解は限られているので、ソフトウェア形式手法に詳しい人の見解を聞きたい。

    • LeanはCoqに似ている。
      例えばCoqの「Software Foundations」の本のように、Cコードに関する命題を立てて証明することはできるが、Leanでそれをしている人はほとんどいないようで、ツールも不足している。
      Lean4でプログラムを書き、そのプログラムについて証明することもでき、一部の人がごく少しずつ取り組んでいる。
      純粋数学を形式化し、それについて論文を出すことが、現在Lean4とCoqの主な使われ方だ。
      Lean/Coqが実際に記述して証明できるものの種類はより一般的だが、現実世界のプログラムにはそこまでの一般性は必ずしも必要ないかもしれない。