実務で使うツール
これは、本書で使用するすべてのソフトウェア保証ツールとRustライブラリの完全な一覧です。 いくつかについては深く経験しますが、大半は触りだけになります。 以下の各名称は、そのツールのホームページまたはドキュメントへのリンクです。
Rustのオープンな形式検証エコシステム
オープンソースの選択肢が幅広くそろっており、Rustの保証エコシステムは活況を呈しています。 Rust Formal Methods Interest Group (RFMIG) は検証ツールの一覧を管理しており、こちらから利用できます。これは、本書で扱うサンプルよりも包括的です。
中核となるツール群
静的保証
このカテゴリのほとんどのツールは、特定のバグが存在しないことを証明するために、ソースレベルのセマンティクスについて推論します。 これらのツールはコンパイラを信頼し、ひいてはそのバックエンドも信頼します。
rustc(Rustのみ、文字どおりコンパイラです！)kani経由のcbmc(Rustフロントエンド、基盤となるツールはC/C++にも対応)prusti* 経由のviper(基盤となるツールはRust、Python、Java、… に対応)。creusot* (Rustのみ)
動的保証
このカテゴリのほとんどのツールは、特定のバグを発見したりプログラムの振る舞いを観測したりするために、コンパイル済みの実行可能ファイルをテストします。 これらのツールは、信頼の連鎖からコンパイラを取り除きます。
valgrind* (x86、x86_64、ARM32、ARM64、MIPS、PPC)rr(x86、x86_64)cargo-fuzz経由のlibfuzzer(x86、x86_64、ARM64)qemu(x86、x86_64、ARM32、ARM64、MIPS、PPC、AVR、…)miri(Rustのみ)
運用上の保証
システムのライフサイクルを支援するツールです。
Rustエコシステム
crates.io でホストされているオープンソースのバイナリとライブラリです。
開発
clap- コマンドライン引数の解析。serde* - Rust構造体のシリアライズとデシリアライズ。tinyvec-!#[no_std]、#![forbid(unsafe_code)]のVec代替。micromath-!#[no_std]、#![forbid(unsafe_code)]の浮動小数点近似。lazy_static* - 実行時に初期化される静的変数。owo-colors- 組み込み向けのテキスト色付け。
テスト
criterion- マイクロベンチマーク用ツールセット。cargo-modules- プロジェクトのモジュールアーキテクチャのテキスト表示。cargo-audit- 既知の脆弱なバージョンをプロジェクトの依存関係グラフから検索。cargo-binutils- Linuxバイナリのプロパティと内容を調査。cargo-bloat- 実行可能ファイルのどの部分がサイズに寄与しているかを特定。siderophile* -unsafeコードが集中している箇所をプロジェクトのコールグラフから検索。cargo-tarpaulin* - コードカバレッジレポート (MC/DC対応を計画中)。
その他
xgadget* - ROP/JOPエクスプロイト開発。
* == 変更される可能性があります。本書は作業中です。
本書が成熟するにつれて、追加のツールが加えられる可能性があります。可能性は低いものの、ツールが削除されることもあります。