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

 (github.com/verus-lang)
1 ポイント 投稿者 GN⁺ 2024-05-06 | 1件のコメント | WhatsAppで共有

Rustコードの正確性を検証するためのVerusツール

  • VerusはRustで書かれたコードの正確性を検証するためのツールです
  • 開発者は、コードが満たすべき仕様を記述し、Verusは実行可能なRustコードがあり得るすべての実行パスで常に仕様を満たすかを静的に検査します
  • ランタイム検査を追加する代わりに、Verusは強力なソルバーに依存してコードが正しいかどうかを証明します
  • Verusは現在Rustのサブセット（拡張中）をサポートしており、場合によっては開発者が標準のRust型システムを超えて、コードの正確性を静的に検査できるようにします（例: 生ポインター操作）

Verusの現在の状態

  • Verusは活発に開発中です
  • 機能が壊れたり欠落したりする可能性があり、ドキュメントも依然として不完全です
  • Verusを試すには、Zulipでヘルプを求める準備ができている必要があります

Verusを使ってみる

  • ブラウザでVerusを試すには、Verus Playgroundを訪れてください
  • より複雑な開発向けには、インストール手順を参照してチュートリアルとリファレンスから始め、以下の資料をご覧ください

Verusドキュメント

  • チュートリアルとリファレンス
  • Verus標準ライブラリのAPIドキュメント
  • 並行性コード検証のためのガイド
  • プロジェクトの目標
  • Verusへの貢献
  • ライセンス

連絡・不具合報告・議論の開始

  • GitHubでイシューを報告したり議論を開始したり、リアルタイムのディスカッションや支援が必要な場合は、Zulipに参加してください
  • 既存機能の再現可能な問題（バグ）にはGitHub Issueを、機能要望や予定機能についてより開かれた議論にはGitHub Discussionsを使用します
  • 貢献は歓迎されます。コードで貢献したい場合は「Contributing to Verus」のヒントを参照してください

GN⁺の意見

  • Rustはシステムプログラミングに適した言語で、安全性と性能を保証できることでよく知られていますが、VerusはこうしたRustの長所をさらに強化できるプロジェクトのようです。特に、並行処理プログラミングの検証機能は非常に興味深く見えます

  • ただし、まだ開発の初期段階でサポートされるRust構文が限定的であるため、実際の本番環境で使うにはもう少し開発が必要なようです。しかし、静的解析で事前にコードの安全性を担保できることは重要であり、今後の発展可能性は高いと考えられます

  • 開発初期であるため、まだドキュメント不足やサポート構文の制限など、改善が必要な点があるものの、長期的にはRustエコシステムで重要な役割を果たすプロジェクトになると考えられます。特に、システムプログラミングやブロックチェーンなど信頼性が重要な分野での活用が高まると期待されます

関連記事

1件のコメント

 
GN⁺ 2024-05-06
Hacker Newsのコメント
  • Verus を使って正式に検証された Kubernetes コントローラーを作成した
    • コントローラーが最終的に要求された desired state にクラスタを調整するという liveness 性質を証明できる
    • 正確性を定式化するには微妙さやニュアンスが多くある（desired state 要件の急速な変化、非同期性、障害など）
    • コードは GitHub リンク にあり、OSDI 2024 に掲載予定の論文と接続されている
  • Verus への小さな一歩として、Rust の debug_assert を使って事前条件と事後条件を追加できる
    • Rust コンパイラは既定でプロダクションビルドからこれを削除する
    • Verus のチュートリアルの例と debug_assert を使ったランタイムチェックの例が提供されている
  • 「コードの正確性検証」と「コードの正確性証明」の違いに関する初心者向けの質問
    • CS/数学の背景が弱い実務のプログラマーのために、コード「証明」を学ぶための良い教材があるかどうか知りたい
    • 「ゼロ知識」証明がなぜ重要なのか、なぜこれがそれほど関係しているのか非常に気になっている
  • Rust 標準には、C/C++、Common Lisp、Ada/SPARK2014 のようなものがまだない
    • これは Ada/SPARK2014 など向けに開発された検証ツールと比較した場合の到達目標が異なることを示している
  • Dafny は Rust にコンパイル可能な「検証志向プログラミング言語」である (GitHub リンク)
  • 主要なコントリビューターの一人がチューリッヒ Rust ミートアップで Verus に関する優れたプレゼンを行った (YouTube リンク)
    • 「ghost」コードがプログラムにきれいに収まるのが印象的だった（Ada をわずかに想起させる）
  • Verus と SPARK の比較
    • 同じ種類の検証器か？ Verus が Ada 向けの検証器ではなく Rust 向けの検証器である点以外に、どんな違いがある？
  • Verus に精通した人が Verus と Lean4 の性能と表現力を比較してくれないか
    • Verus は SMT ベースの検証ツールで、Lean は対話型証明器かつ SMT ベースのツールだと理解している
    • ただし形式的検証分野への理解が限定的なので、ソフトウェア形式手法に詳しい人の意見を聞くとよいだろう
  • Verus と Kani の関連性はあるか？ どう違って動作するのか？ (Kani GitHub リンク)
  • 結果コードが依然としてバニラ Rust ツールでコンパイルできる有効な Rust コードとして維持されるような実装方法はあるだろうか？