形式検証(ソフトウェア検証)がいよいよ流行りそうな気配を見せています。
もともと形式検証は「理論的には可能だが実用的には時間と手間がかかりすぎる」ものだったのですが、近年のAIの爆発的な性能向上によって形式検証も突然実用の領域に入ってきました。
しかし実際に形式検証をやってみると、周辺環境がまだまだ未成熟なことがよくわかります。
特に問題なのが結果の管理です。どのバージョンのどのAPIについて、何を検証したのか、検証コードや実行ログはどこにあるのか、追加した命題と証明はどこで管理しているかなど、形式検証を通してさまざまなデータが出てきますが、できればそう言った情報をそのクレートを使うユーザー全員が確認できる形にしておきたいところです。
proofs.rsでは、形式検証の(といいつつ実は形式検証に限らないのですがそれを含めたさまざまな)結果をcrates.ioのクレートやAPIに紐づけて公開できます。今回は小さなクレートをKaniで検証して、実行ログと一緒に投稿してみます。
検証するクレートを用意する
proofs.rs は crates.io に登録された crate に対して誰でもその検証結果のレポートを提出できます。
逆にいうと、検証対象は必ず crates.io に登録されていなければなりません。
crates.io に登録されている検証がしやすそうなおもちゃの crate ということで、今回はeven-or-odd 0.1.0を検証対象としたいと思います。
even-or-odd は is_even と is_odd の二つの関数だけを提供する crate です。とても検証しやすそうですね。
ということで、まずは crate を github 上で fork します。
https://github.com/nyuichi/even-or-odd-verification
今回は練習ということで、 is_even だけの検証を行います。
Kaniで検証する
今回は検証ツールとして kani を採用します。
kani は rust で有界モデル検査を行うためのツールで、contract の記述にrustの関数がそのまま使えて大変便利です。AWSでも使われているそうです。
欠点としてはあくまで有界な範囲での検査しかできず、たとえば任意の長さの Vec を受け取る関数の検証ができないと言った制約があります。今回は関係ないですね。
まず、Kaniをインストールします。
cargo install --locked kani-verifier
cargo kani setup
今回使用したバージョンは次のとおりです。
Kani Rust Verifier 0.68.0 (cargo plugin)
CBMC 6.11.0
検証したい関数はis_evenです。もともとの実装はジェネリックですが、今回はu32で呼び出した場合のすべての入力を対象にします。
src/lib.rsにcontractとproof harnessを追加します。
#[cfg_attr(kani, kani::ensures(|result: &bool| *result == (number % T::from(2) == T::from(0))))]
pub fn is_even<T> (number: T) -> bool where
T:
Copy +
std::ops::Rem<Output = T> +
std::cmp::PartialEq<T> +
From<u8>
{
number % T::from(2) == T::from(0)
}
#[cfg(kani)]
mod verification {
#[kani::proof_for_contract(crate::is_even)]
fn verify_is_even_u32() {
let number: u32 = kani::any();
crate::is_even(number);
}
}
ensuresに書いたのは、戻り値がtrueであることと、入力を2で割った余りが0であることが一致する、という条件です。kani::any::<u32>()がu32型の全ての値を(仮想的に)動いてくれるため、これが通れば全入力に対する検証が完了したということになります。
では実際に kani で検証します。function contractsを使うので、-Z function-contractsを付けます。
cargo kani -Z function-contracts
出力のうち、事後条件のチェックは次のようになりました。
Check 11: is_even::<u32>::{closure#2}.assertion.1
- Status: SUCCESS
- Description: "|result: &bool| *result == (number % T::from(2) == T::from(0))"
- Location: src/lib.rs:12:18 in function is_even::<u32>::{closure#2}
サマリーはこんな感じ。
SUMMARY:
** 0 of 99 failed
VERIFICATION:- SUCCESSFUL
Verification Time: 0.2364988s
Manual Harness Summary:
Complete - 1 successfully verified harnesses, 0 failures, 1 total.
ここまでの内容でコミット & push しておきます。
git add src/lib.rs Cargo.toml Cargo.lock .gitignore
git commit -m 'Verify is_even with Kani'
検証結果を proofs.rs に投稿する
投稿にはcargo-proofsを使います。crates.ioからインストールします。
cargo install cargo-proofs --locked
proofs.rs にログインします。これは(このワークスペースに限らない)グローバルな設定です。デフォルトだとブラウザ認証です。
cargo proofs login
投稿用の設定ファイルを生成します。 proofs.toml というファイルが出来上がります。
cargo proofs init --tool kani --tool-version 0.68.0 --title 'Correctness of is_even for all u32 inputs'
proofs.tomlには、検証した性質と範囲を次のように設定します。 trusted_assumptions にはこのレポートで信頼する範囲(たとえばkaniの正しさ、など)、limitations には今回の検証で妥協せざるを得なかった範囲 (たとえば kani は generics に対応していないので諦めた、など)を記述します。どちらも検証上の妥協ですが、前者はこのレポートを作るにあたっての前提条件、後者はこのレポートを作っている最中に見つかった課題、という感じで、後者はできればレポートの更新時には直していきたい、というニュアンスを込めておきます。
[report]
title = "Correctness of is_even for all u32 inputs"
explanation = "For every u32 input, is_even returns true exactly when the input is divisible by two. The verification fork retains the function body from even-or-odd 0.1.0 and adds a Copy bound to reuse the input in the postcondition; u32 already satisfies this bound. The contract harness covers all u32 values without input assumptions."
trusted_assumptions = "The result relies on Kani and CBMC correctly modeling and checking Rust u32 operations. No user-defined stubs or assumed helper contracts are used."
limitations = "Only is_even instantiated with u32 is covered. Other instantiations of this generic API, custom trait implementations, and is_odd are not verified. Equivalence of the entire verification fork to the crates.io release is not formally proved."
environment = "Kani 0.68.0, x86_64-unknown-linux-gnu; cargo kani -Z function-contracts."
[tool]
name = "kani"
version = "0.68.0"
次に公開用の実行記録を作るため cargo proofs run を実行します。
もう一度 kani が走ります。その際の標準出力・標準エラーなどがSARIF形式で保存されます。
実際の検証作業時には最初からこっちのコマンドを打つことになると思います (二度手間が防げるため)。
cargo proofs run -- cargo kani -Z function-contracts
出力結果
Recording run b46304e8-8a30-4616-ab3a-9e22566b3577 at "2a31ef64bbff220d9fcf2e1d4b13fb04934a5621"
..
SUMMARY:
** 0 of 99 failed
VERIFICATION:- SUCCESSFUL
Verification Time: 0.1186479s
Manual Harness Summary:
Complete - 1 successfully verified harnesses, 0 failures, 1 total.
Saved run b46304e8-8a30-4616-ab3a-9e22566b3577: /home/yuichi/.local/share/cargo-proofs/e6ff1fb4d4b94303b9b10c6d8dfa19034ae33b2f067a3be11a9d2b87aa5dce62/runs/b46304e8-8a30-4616-ab3a-9e22566b3577
これで検証器の実行が保存されました。
次に、投稿内容を確認します。
cargo proofs publish --dry-run
こんな感じの出力になります(抜粋)。
even_or_odd::verification::verify_is_even_u32 → even_or_odd::is_even
precondition: true
evidence: https://github.com/nyuichi/even-or-odd-verification/blob/2a31ef64bbff220d9fcf2e1d4b13fb04934a5621/src/lib.rs#L25-L29
Report: Correctness of is_even for all u32 inputs
1 claims; 0 removal(s).
対象がeven_or_odd::is_evenになっていて、ソースのリンクも実行したコミットを指しています。
問題ないので公開します。
cargo proofs publish
even_or_odd::verification::verify_is_even_u32 → even_or_odd::is_even
precondition: true
evidence: https://github.com/nyuichi/even-or-odd-verification/blob/2a31ef64bbff220d9fcf2e1d4b13fb04934a5621/src/lib.rs#L25-L29
Report: Correctness of is_even for all u32 inputs
1 claims; 0 removal(s).
Published report #5, revision 1: https://proofs.rs/report/5
最後の行にレポートの URL が出ていますね。実際のレポートはこちら↓。
Correctness of is_even for all u32 inputs — レポート #5
レポートを見てみるとわかる通り、even-or-odd 0.1.0のis_evenに対するclaimが1件含まれています。検証コードは公開リポジトリにあり、レポートからは検証に使ったコミットと実行記録を辿れます。
まとめ
even-or-oddのis_even::<u32>をKaniで検証し、proofs.rsに結果を投稿しました。
今回のように crate 全体ではなく特定のAPI・型に絞った部分的な検証結果でもレポートを公開できます。
検証したい crate に依存先がある場合、その依存先の検証結果としてどのレポートを信頼するかという情報を記録することもできます。
みんなで形式検証してより安全なソフトウェアを構築しましょう。