S15 Rustプログラム検証ゼミ知見まとめ

# S15 Rustプログラム検証ゼミ知見まとめ S15 Rustプログラム検証ゼミメモ https://hackmd.io/j1RCN2MGTyqagDTQ0wxavg ## ゴール Rust の SMT ベース静的検証器を作る ### 方針 - Rust Typed HIR → SMT-LIB2 の直接変換 - Symbolic execution の考え方をベースにする - 一般的な Symbolic execution の解説 - スライド Emina Torlak 2016 https://courses.cs.washington.edu/courses/cse403/16au/lectures/L16.pdf - A Survey of Symbolic Execution Techniques https://dl.acm.org/doi/pdf/10.1145/3182657 ACM Computing Surveys, 2018 ## 参考: Rust 半自動検証器 Verus 最近一番勢いのある Rust SMT ベース半自動検証器モデルケースとして参考になるかも - GitHub: https://github.com/verus-lang/verus - 充実した開発体制 - Microsoft Research も開発に関わっている - 多数の論文とプロジェクト: https://verus-lang.github.io/verus/publications-and-projects/ - OSDI 2024 の Distinguished Paper 2つ (Anvil・VeriSMo) が Verus を使う静的検証 - 充実したドキュメント - リファレンス: https://verus-lang.github.io/verus/guide/ - VerusDoc: https://verus-lang.github.io/verus/verusdoc/vstd/ - Rust doc っぽい見た目で、Verus の事前/事後条件も載っている - 充実したツール - Verus Playground: https://play.verus-lang.org - Verus Analyzer: https://github.com/verus-lang/verus-analyzer - VSCode で Rust Analyzer のようなノリで使える - 大まかなフロー 1. Rust に仕様のアノテーションを書く独自言語 →[Verus]→ 2. アノテーション付き Rust プログラム (内部で変換、ユーザーは直接触れない) →[Rust コンパイラ]→ 3. Typed HIR →[Verus]→ 4. SMT-LIB2 論理式 →[SMTソルバ]→ 検証 - 検証に失敗したらその位置を教えてくれる ![](https://raw.githubusercontent.com/verus-lang/verus/main/source/docs/verus-demo.png) - 可変参照を返す関数は未サポート - RustHorn 方式の預言を使うエンコーディングを検討中 - https://github.com/verus-lang/verus/discussions/35 ## Z3 SMT ソルバ - Z3 レファレンスがだいぶまとまっている https://microsoft.github.io/z3guide/docs/logic/intro - 基本機能 - `(declare-const 名前ソート)`: `ソート` の定数 (存在量化された変数) `名前` を導入する - `(assert 条件)`: `条件` を要請する - `(check-sat)`: これまでの `条件` を満たす (定数への) 割り当てが存在するかチェックする - 一般に SMT が確かめるのは (定数について) 存在量化の命題だが、否定 (ド・モルガン双対) を取ると全称量化の命題を検証できる - 特に ``` (declare-const 変数1 ソート1) ... (declare-const 変数k ソートk) (assert 仮定1) ... (assert 仮定n) (assert (not 帰結)) (check-sat) ``` は否定を取ると ``` ∀ 変数1: ソート1, ..., 変数k: ソートk. 仮定1 ∧ ... ∧ 仮定n ⇒ 帰結 ``` を検証してくれる (`unsat` で検証成功) - 便利機能 - `(simplify 式)`: `式` を簡約した結果 - ``` < (simplify (mod 8 -3)) > 2 ``` - `(display 式)`: `式` の糖衣構文を除いた結果 - ``` < (display (/ 2 3)) > (/ (to_real 2) (to_real 3)) ``` - その他 - `=` の否定の演算子は `!=` や `<>` ではなく `distinct` - 可変長引数で、pairwise distinct であることを表す - 整数除算/剰余は `div`/`mod` - Euclidean division (剰余が常に非負) であることに注意 - 例: `8 divmod -3 = (-2, 2)`, `-8 divmod 3 = (-3, 1)`, `-8 divmod -3 = (3, 1)` - Rust 等多くの言語は Truncated division (0方向への丸め) - 剰余の符号は割られる数の符号に一致 - 割る数 & 割られる数の abs が同じとき div & mod の abs が同じ - 例: `8 divmod -3 = (-2, 2)`, `-8 divmod 3 = (-2, -2)`, `-8 divmod -3 = (2, -2)` - Euclidean division による Truncated division の再現方法 - `m divTruncated n = sgn(m) * (abs(m) divEuclid n)`, `m modTruncated n = sgn(m) * (abs(m) modEuclid n)` - `sgn(n)` は `n` が正ならば `1`、負ならば `-1`、0 ならば `0` - SMT での実装方法: ``` (define-fun sgn ((n Int)) Int (- (> n 0) (< n 0))) (define-fun divt ((m Int) (n Int)) Int (* (sgn m) (div (abs m) n))) (define-fun modt ((m Int) (n Int)) Int (* (sgn m) (mod (abs m) n))) ``` ## Rust Typed HIR API 概要 - Nightly を使う必要がある - Nightly バージョンは `rust-toolchain.toml` で指定 - 最初の入口 → `TyCtxt` 入手 - [`rustc_driver::RunCompiler::new`](https://doc.rust-lang.org/stable/nightly-rustc/rustc_driver/struct.RunCompiler.html) - [`rustc_driver::Callbacks`](https://doc.rust-lang.org/stable/nightly-rustc/rustc_driver/trait.Callbacks.html) を実装 - [`Callbacks::after_expansion`](https://doc.rust-lang.org/stable/nightly-rustc/rustc_driver/trait.Callbacks.html#method.after_expansion) は Typed HIR 生成後 - 引数に `queries : &'tcx Queries<'tcx>`、 `queries.global_ctxt().unwrap().enter(|tcx : TyCtxt| ...)` で `TyCtxt` にアクセスできる - [`rustc_driver::Compilation::Stop`](https://doc.rust-lang.org/stable/nightly-rustc/rustc_driver/enum.Compilation.html#variant.Stop) を返せばいい - `TyCtxt` 入手 → 解析対象の [`LocalDefId`](https://doc.rust-lang.org/stable/nightly-rustc/rustc_span/def_id/struct.LocalDefId.html) を手に入れる - `LocalDefId` は [`DefId`](https://doc.rust-lang.org/stable/nightly-rustc/rustc_span/def_id/struct.DefId.html) のうち自分のクレート由来のもの - [`as_local`](https://doc.rust-lang.org/stable/nightly-rustc/rustc_span/def_id/struct.DefId.html#method.as_local) または [`expect_local`](https://doc.rust-lang.org/stable/nightly-rustc/rustc_span/def_id/struct.DefId.html#method.expect_local) で `DefId` から `LocalDefId` に変換 - 関数・データ型一覧: [`TyCtxt::mir_keys`](https://doc.rust-lang.org/stable/nightly-rustc/rustc_middle/ty/struct.TyCtxt.html#method.mir_keys) - MIR のキーは (Typed) HIR のキーにもなっている - エントリポイントの関数: [`TyCtxt::entry_fn`](https://doc.rust-lang.org/stable/nightly-rustc/rustc_middle/ty/struct.TyCtxt.html#method.entry_fn) - `LocalDefId` に対してTyped HIR 解析 - [`TyCtxt::thir_body`](https://doc.rust-lang.org/stable/nightly-rustc/rustc_middle/ty/context/struct.TyCtxt.html#method.thir_body) で Typed HIR にアクセス - 特に `let (stealThir, exprId) tcx.thir_body(id : LocalDefId).unwrap();` で `stealThir : Steal<Thir<'tcx>>` が手に入る - `let thir = stealThir.steal();` で Typed HIR `thir : Thir<'tcx>` が手に入る、ただし `steal` は一回しかできない - `let refThir = stealThir.borrow(); let thir = &*refThir` で Typed HIR への共有参照 `thir : &Thir<'tcx>` が手に入る ## 実装方法の例 - Symbolic execution の概要 - (ローカルな) 環境 - 構成要素 - .値環境: (プログラム変数名 ↦ (型 &) 値のマップ) のスタック - スタックにする理由: スコープを抜けるときに変数がごそっと捨てられるので / スコープ間で変数の名前が被ってもいいので ```rs let x = 7; let y = 3; { let x = true; print(x); // true print(y); // 3 } print(x); // 7 print(y); // 3 ``` - 値は論理変数による式で表される - 新しいスコープに入ったときに、スタックに空のマップを増やす - .仮定リスト: これまでの仮定の式のリスト - 基本操作 - `env[plc]` : 場所 (place) `plc` からの読み取り - 特に `plc` が単に変数 `x` のときが基本 - `env[plc := v]` : 場所 `plc` への割り当ての更新 - `env[pat := v]` : パターン `pat` への割り当ての追加(/更新) - `env + cond` : `env` の仮定リストに `cond` を加える - グローバルで論理変数環境: 論理変数名 ↦ ソートのマップを持つ - 論理変数名の名前被りに注意が必要、一意にする方法はいくつかありえる - 例えばソースコード中での出現の行/列番号をつけて区別する、等 - 例えばメインの関数は `execute(式, 実行前の環境) := ...; 実行結果の値, 実行後の環境` とすれば良い - 実装方針 - ミニマルな例を作ってこまめにテストする - 正例 (成功例) と負例 (失敗例) の両方を作る - if 等での分岐があるので、execute において環境は可変参照渡しでなくムーブ渡しのほうがおすすめ - assume の処理 ``` execute(assume p;, env) := (), env + p ``` - assert の処理 ``` execute(assert p;, env) := CALL_SMT(env の仮定たち ==> p); (), env + p ``` - 非決定的値の処理 ``` execute(nd::<T>(), env) := let X = (T 型の値のフレッシュな論理変数) in X, env ``` - 変数宣言 ``` execute(let pat = e;, env) := let (v, env') = execute(e, env) in (), env'[pat := v] ``` - 変数のシャドーイング (例: `let x = ...; let x = ...;`) に注意 - 基本的には単に上書きでいい - RustHorn 方式の預言 (後述) を使う場合は、上書きされる各プログラム変数 `x` について `resolve(env'[x])` - 代入 ``` execute(plc = e, env) := let (v, env') = execute(e, env) in (), env'[plc := v] ``` - RustHorn 方式の預言を使う場合、`resolve(env'[plc])` を行う - スコープ ``` execute({ e }, env) := let (v, env') = execute(e, env の値環境に空マップを push したもの) v, (env' の値環境から最上位を pop したもの) ``` - if 式の処理 ``` execute(if cond { e1 } else { e2 }, env) := let (v1, env1) := execute({ e1 }, env + cond) in let (v2, env2) := execute({ e2 }, env + not cond) in ite cond v1 v2, merge_if env cond env1 env2 ``` ただし、`merge_if` の定義は以下の通り ``` merge_if env cond env1 env2 := { .値環境 := { x |-> ite cond env1[x] env2[x] | env の各プログラム変数 x }, .仮定リスト := env の仮定 + { cond ==> p | p in env1 の仮定のうち env にないもの } + { not cond ==> p | p in env2 の仮定のうち env にないもの } } ``` なお、`ite cond v1 v2` は `v1 = v2 = v` のときに `v` に簡約しておくと良い最適化になる - while 式の処理 ``` execute(invariant inv_1; ... invariant inv_n; while cond { e }, env) := CALL_SMT(env の仮定 ==> inv_1); ... CALL_SMT(env の仮定 + inv_1 + ... + inv_n-1 ==> inv_n); let newenv = fresh(env) in let invenv = newenv + inv_1 + ... + inv_n in let _, env' = execute({ e }, invenv + cond) in CALL_SMT(env' の仮定 ==> inv_1); ... CALL_SMT(env' の仮定 + inv_1 + ... + inv_n-1 ==> inv_n); (), invenv + not cond ``` ただし `fresh(env)` は以下のように定義されるフレッシュな環境 ``` fresh(env) := { .値環境 := { x |-> (その型のフレッシュな論理変数) | e で更新されうる env の各プログラム変数 x } + { y |-> env[y] | e で更新されえない env の各プログラム変数 y }, .仮定リスト := [] } ``` `e` で更新されうるかの評価は上方近似であれば何でもいい - 可変参照の扱い: RustHorn 方式がおすすめ - 利点 - 講師が発明者 - ライフタイムの情報を使わなくてよい - 可変参照が first-class の値として扱える - かなり広いクラスの可変借用の操作を単一の方針で扱える - 特に、再借用や可変参照のネストなどを問題なくサポートできる - 参考になる資料 - 松下 PRO-2024-1 招待講演スライド https://shiatsumat.github.io/talks/pro-2024-1-invited-talk.pdf (特に24ページから) - 松下 JSSST 2020 RustHorn トーク https://www.youtube.com/watch?v=Ah_Bds6I_YI - Verus で RustHorn 方式の預言を導入するための議論 https://github.com/verus-lang/verus/discussions/35 - 特に https://github.com/verus-lang/verus/discussions/35#discussioncomment-4925078 - 可変参照は現在の値と将来の値の組で表現、借用開始時に預言をつくる ``` execute(&mut plc, env) := let X = (フレッシュな論理変数) in ((env[plc], X), env[plc := X]) ``` ここで `X` が預言 - 可変参照を更新するときは「現在の値」パートを更新する - ここでのエンコーディングだと `.0` の部分 - 可変参照を捨てるときに預言を解決する - `resolve(v)` : 論理値 `v` に含まれる預言を解決した仮定のリスト - 正確には、`v` に対応する Rust での型も加味する必要がある - 特に可変参照である変数 `x : &mut T` について、`resolve(env, x) := [env[x].1 == env[x].0]` - 発展: 一般には、データ構造の中に含まれる可変参照について再帰的に `resolve` を適用する - 例えば `Vec<&mut T>` だと全要素の `&mut T` の預言を解決する - データ (特に可変参照) を捨てるタイミングの解析 - 楽な方法: 単に変数がスコープを抜けるタイミングでそのなかの可変参照たちの預言を解決 - すなわち Lexical lifetime の時代に戻る - 例えば ```rs fn main() { let mut a : i32 = rand(); let mut b : i32 = rand(); { // このスコープが必要 let ma = &mut a; let mb = &mut b; let mc = if *ma >= *mb { ma // mb がスコープから抜けるので預言を解決 // すなわち mb.1 == mb.0 を仮定に追加 } else { mb // ma がスコープから抜けるので預言を解決 // すなわち ma.1 == ma.0 を仮定に追加 }; *mc += 7; // mc がスコープから抜けるので預言を解決 // すなわち mc.1 == mc.0 を仮定に追加 } assert!((a - b).abs() >= 7); } ``` - 大変な方法: プログラムを後ろからみて変数が使われなくなるタイミングを生存解析 - 実際ちょっと短期間で組むにはしんどいかも - 可変参照を細分化するときに預言を部分的に解決する - 例えば、`Vec::index_mut<'a, T>(v : &'a mut Vec<T>, i : usize) -> &'a mut T` を実行した後、`v.1 == v.0[i := res.1]` が仮定に追加される