# Real-Time Leak Checking in Miri ## 2024/11/05 ### 理論 低レベルのポインタ操作だけある単純な言語で形式的な理論を作ると楽しそう - Operational/graph の reachability / leak 概念 - Operationally reachable = ある操作列 (プログラム & 実行列と言ってもいい?) が存在して、そのメモリ(ブロック)にアクセスできる - Graph-reachable = 参照グラフ上で、そのメモリ(ブロック)にアクセスできる or exposed - Leaked は Reachable の否定 (Unreachable)、Operationally leaked と Graph-leaked の2種類 - 定理: Operationally reachable ⇔ Graph-reachable - 対偶から Operationally leaked ⇔ Graph-leaked - Graph-reachable → Operationally reachable - 証明: グラフの参照をたどるのに対応する read-only の操作をやれば簡単 - exposed なものについては、乱数 rand () と int2ptr を使うとアクセスできる - Operationally reachable → Graph-reachable - 操作が参照グラフの構造を破壊的に更新しうるので難しい - 証明: 任意の操作は (既にアロケートされたもののうちで) Graph-reachable なものを増やさないので、これを使うと帰納的に示せる - int2ptr は exposed なものしかアクセスしない (そうでないと UB になる) ので OK ### リーク発見アルゴリズムの最適化 - アイデア: 強参照 (ループがないことが保証されている)・弱参照に分ける - 強参照は DAG をなすので、その連結成分たちを考える - root を含む DAG から弱参照で辿れない DAG の頂上 (参照関係の極小元) が存在しないかチェックする - 参照を逆に辿っていく BFS とか？ - Rust だと所有権情報を使って強参照を絞り込める - Box や Unique は強参照 - 現実的に大体のところは強参照になってくれる？ - Rc, Arc は (Weak でなくても) 弱参照になる - BTree とかの木構造は NonNull みたい - 普通は HashMap 等の配列ベースのデータ構造を使うことのほうが多いから困らない？ - 強参照/弱参照の色分けを標準ライブラリについては導入してもいいかも - このアルゴリズムは将来的には LeakSanitizer みたいな実行時のチェックにも使えそう - 原理的には LLVM でも実装可能なはず - Rust ですでに LLVM ベースの各種サニタイザがあるらしい ## 2024/09/30 ## 2024/09/24 ## 2024/09/17 ## 2024/09/02 - Miri を直接改造して所有権検査を加える方針にしよう - Miri を fork したレポジトリを作った https://github.com/SoftwareFoundationGroupAtKyotoU/miri ## 2024/08/30 - アイデア - own してるメモリーがリークされないことを確認したい - 単純なテストや Miri では手が届かない - Drop の検証をしたい - https://doc.rust-lang.org/nomicon/dropck.html - may_dangle attribute の扱いが難しい - @southball - Iris は一旦置いときます - MIR を触ってみます - 参考 - RustHorn で MIR を操作するソースコード https://github.com/hopv/rust-horn/tree/master/rust-horn/src - 環境構築: https://rustc-dev-guide.rust-lang.org ## 2024/08/20 Miro: https://miro.com/app/board/uXjVKoUuhGI=/ Nola POPL 原稿 https://www.fos.kuis.kyoto-u.ac.jp/~ymat/papers/popl2025-nola.pdf を通して Higher-order state の基本について説明 Iris GitLab https://gitlab.mpi-sws.org/iris/iris Coq の流れを one-shot (`./tests/one_shot_once.v`) の例を通して説明 RefinedRust 論文も読んでおくと良いと思う https://plv.mpi-sws.org/refinedrust/paper-refinedrust.pdf Vec の検証例が詳しく書かれている、Dyro とも近い問題意識 ## 2024/08/06 松下 - Choi ミーティング Miro: https://miro.com/app/board/uXjVKsGX4-o=/ ### なぜオブジェクトを木構造で表現？ - Rust では部分オブジェクトに対する操作が一般にできる - 例: `struct a` のフィールド `f` からムーブ `a.f` / 更新 `a.f = o` (古いデータ `a.f` をdrop)、vector `v` の i 番目の要素を更新 - いちいちオブジェクト全体の所有権を考えて再配分を行うのは効率が悪い & 場合によってはそもそも難しい場合も (特に可変参照のように ghost data がある場合) ### Rust/Dyro での型定義 構文はちょっと適当 ```rs struct Unique<T> { pointer : NonNull<T>; @size : Uint; @own : for i in 0..size { pointer.offset(i) |-> T? } @free : Free(pointer[0..size]) } struct RawVec<T> { ptr : Unique<T>; cap : usize; + ptr.@size == cap } struct Vec<T> { buf : RawVec<T>; len : usize; + for i in 0..len { buf.ptr.@own[i].is_init() } } ``` ### Dyro でのオブジェクトモデル ```rs Vec<String> { buf : RawVec<String> { ptr : Unique<String> { pointer : 0xdead0000, @size : 5, @own : { 0xdead0000 |-> String { len : 6, ptr : 0xbeef0000, @own : 0xbeef0000..0xbeef0006 |-> "hello\n" }, 0xdead0001 |-> String { ... }, 0xdead0002 |-> Uninit(...), // ムーブ後 0xdead0003 |-> poison, 0xdead0004 |-> poison, }, @free : Free(0xdead0000..0xdead0005), }, cap : usize(5), }, len : usize(3), } ``` - 各オブジェクトは木構造を捨ててまとめると以下を持つ - byte value の列 - 所有権 (ヒープの部分領域 etc.) - 1バイトのデータは下のいずれか - 具体的な値 `0x00001111` - アクセス不可 `poison` - symbolic なアドレスのiバイト目 `(x + 7)@3` ### 検証例 ```rs fn pop<T>(v : Vec<T>) -> (T, Vec<T>) { let e = ptr::read(v.ptr.pointer.offset(v.len)); // v.len -= 1; (e, v) // v の Vec<T> の保証で違反 } // ptr::read/write も place からの読み取り/書き込みと同等に扱う ``` ### Dyro での動的検証 - ptr::read, write における所有権の扱いについて - Copyable な型については問答無用で所有権を複製できる - 非 Copyable 型についてはデフォルトではムーブする - それ以外の場合 (おそらくあまりない…？) はアノテーションを付ける - ムーブ、値のみ (所有権はソース側に残す)、...? - 基本方針: 所有権について特殊な操作をしたい場所では ソースコードにアノテーションを付けさせる - 所有権保証違反が検知される代表的な状況 - 未初期化/ムーブ後 のデータへの不正アクセス - 型で要請される保証を (関数から return する時点 etc. で) 満たしていないとき ### ひとまずの実装方針 - Vec, RawVec, Unique, NonNull, 整数の基本型 (i32, ...) をハードコードする (型宣言のほうは一旦サポートしない) - 型は適宜アノテーションを要求する (型推論は頑張らない) - 操作的意味論/動的検証器を組む - まずオブジェクトのための木構造のデータ型を定める - さらに補助データとして、アドレス から (対応する部分木のパス) へのマップを持つ - 例: 0xdead0001 |-> v.buf.ptr.@own[1] - そのモデルでコードを実行するインタプリタを組む - 適切な場所にチェックを挟む ### 長期的ゴール - Rust MIR を対象とする - Rust のアノテーション #[...] - alloc のアドレスを symbolic に扱う - フレッシュなアドレス変数 x を取ってきて x + オフセット (x + 7 等) の形でアドレスを表現しておく - アドレス変数達への任意の値割当について、動的検証で得られた結果が使える - 特に、任意のアロケータでの動作の正しさが言える - Vec etc. の検証で各要素を symbolic に扱う - 一般により static な検証への移行が考えられる - ベースとして dynamic な検証でのモデルが活用できるはず - Functional な仕様を入れてもいいかも - 例: Vec::pop で出てくるのは元の Vec の最終要素 (と所有権情報を含めて/木構造として一緒) ### 形式化メモ #### 具体的モデル ```rs bv : ByteValue ::= 0bBBBBBBBB /* simple byte, each B is 0 or 1 */ | poison /* poison value */ bvs : ByteSequence ::= [bv_0, ..., bv_n-1] addr : AddressValue ::= bv ``` ```rs obj : Object ::= { fld_i : obj_i.., !ofld_j : own_j.. } /* Struct */ | bvs /* Raw byte sequence */ own : Ownership ::= addr |-> obj /* Object at an address */ ``` ```rs raw : Object -> ByteSequence /* Raw byte sequence for object */ raw { fld_i : obj_i.., !ofld_j : _.. } := concat (raw obj_i..) raw bvs := bvs ``` #### 検証用のパラメトリックなモデル ```rs addri : AddressId ::= n : Nat aaddr : AbstractAddress ::= addri @ o /* addri : AddressId, o : Int is offset */ abv : AbstractByteValue ::= bv : ByteValue | aaddr @ i /* i-th (0-7) byte of aaddr : AbstractAddress */ ``` ## 2024/08/02 田辺先生・関山先生 (Rust との Interoperability に興味がある) と議論 ### Dyro について - 一般に動的検証の嬉しさは？ - 特定の入力に対しては正しさを厳密に保証できる - 現実的に、多くの場合、代表的な入力パターンで正しければほかの入力でも正しいことが多い - バグに早く気づくことができる - ユニットテストと似ているが、より深い性質まで見ることができる - Dyro はある種の動的な篩型検査・借用検査を行う - 例: `Vec::index_mut` - 単純に safe/unsafe の境界部分で検査するわけではない - `unsafe { ... }` は `unsafe` な機能を使っているマーカーであり、その影響はもう少し先で検査しないといけない可能性がある (関数/スコープから出るタイミングなど) - `safe` な部分の functional な挙動に `unsafe` 機能の使用の正しさが依存しうるので、`safe` な部分の実行・所有権情報も追跡する - 例えば、unsafe なポインタ演算の正しさが safe な整数演算に依存しうる - 所有権が正しくついている状況で safe な関数の呼び出しは絶対に失敗しない、ということは保証されている - RustBelt 同様の分離論理での Hoare triple として理解できる ## 2024/08/01 ### 考察 - 厳密な「検証」にするために - malloc が返す非決定的なアドレスに依存するのは割とまずい → symbolic なメモリブロック番号変数 X を生成することにする - 2つの異なるメモリブロック番号変数 X, Y について X ≠ Y までは保証 - アドレスは RustBelt と同じく `(メモリブロック番号, オフセット)` の組として持つ - 基本的に非決定性は認めない方針にするのが良さそう - (非決定性を持たない) 各関数が実行されるたびに、特定の入力についての安全性/所有権の正しさの Hoare triple が厳密に証明される - Hoare triple は分離論理におけるもの ### Gradual typing ミーティングでの報告 - Dyro: Dynamic Rust Ownership Verification というプロジェクトを始めた - HackMD: https://hackmd.io/BUXiiU2cR2OsfXJbzYSH2w GitHub: https://github.com/SoftwareFoundationGroupAtKyotoU/dyro 論文スケッチ: https://www.fos.kuis.kyoto-u.ac.jp/~ymat/papers/sketch-dyro.pdf - タイトルを上げただけで GitHub に外部から 4 stars 付いて嬉しい - 研究計画 - しばらく松下の取り組むメインのプロジェクトになる予定 - Choi さんの卒論研究で実装・実験をしてもらおうとしている - Rust Verification Workshop 2025 (ETAPS併設、5月) で一旦お披露目 - POPL 2026 (来年7月投稿) あたりを目指す？ - Gradual typing や Interoperability と広い意味で関係がありそう - 明日 14時〜 に関山先生・田辺先生とミーティングする - Rust の所有権について、動的だが厳密な**検証** - 特定の入力 (+ 乱数の選択) については所有権上の安全性を (分離論理的な枠組みで) 厳密に保証 - 特に、実行の任意の組み合わせについてメモリ・スレッド安全性を保証 - RustBelt がベースだが、動的検証のために色々改良 - グローバルなメモリ状況を持ち回らず、局所的な情報だけを検査 - Miri のような Reference counting 等をするものとは違う - Key idea: 各 Rust オブジェクトを所有権情報を含めた木構造としてモデル化 - このモデル化のもとで実行する操作的意味論を考える - Rust の所有権型はこの木構造に対する制約 - 木構造は借用の id などの幽霊状態を含む - 木構造にしているおかげで、部分オブジェクトを操作する (ムーブ、更新 etc.) ことが自由にできる - (共有参照を通した) 循環参照がありうるので一般には無限木がありうる → 実装上はグラフ表現 - 意義 - そもそも Dyro のモデル化によりプログラマーはよりよく Rust を理解できる - 特に借用やライフタイムが絡んできたときに難しい - 所有権関係のバグがあったときに、早い段階で & 原因がクリアな形で気づくことができる - 比較: Miri はアクセス競合の検査をするだけ → 具体的にアクセスが起こって初めて気づく & 本質的な原因である所有権の競合まで遡るのが容易でない - 将来的には、動的検証をベースラインとして、だんだん Symbolic execution や Abstract interpretation 等の parametric な方向に向かっていく - Core challenge: 借用の扱い - 可変参照 `&'a mut T` は以下に「権利」と「義務」からなる - ライフタイム `'a` まで型 `T` のオブジェクトが使える「権利」 - ライフタイム `'a` までに型 `T` のオブジェクトを返す「義務」 - 借用を細分化するときに全称量化の命題の検証が必要 - 例: ```rs fn index_mut<'a, T>(v : &'a mut Vec<T>, i : usize) -> &'a mut T { assert!(i < v.len()); unsafe { &mut *(v.as_mut_ptr().offset(i)) } } ``` 特に、「ライフタイム `'a` 終了後に `&'a mut T` から**どのような**型 `T` のオブジェクトが返ってきたとしても、`v : &'a mut Vec<T>` は `Vec<T>` を作る義務を果たすことができる」という全称量化の命題を検証しないといけない - 配列自体が具体的に与えられていても、**将来** `&'a mut T` から返ってくるオブジェクトの具体的な内容はわからない - 要するに時間を超えたグローバルな所有権のやり取りを考えないといけない点が借用の難しさ - RustHorn 方式の預言が生きるのもそういう理由 ## 2024/07/26 ミーティング Miro ボード: https://miro.com/app/board/uXjVKvN4LMM=/ 実装 GitHub Repo - https://github.com/SoftwareFoundationGroupAtKyotoU/dyro 論文スケッチ - https://www.fos.kuis.kyoto-u.ac.jp/~ymat/papers/sketch-dyro.pdf ## 2024/07/25 やはり RustBelt を出発点として Dynamic Rust Verification を目指したい 松下: その方向で色々形式化してみます ### 関連しそうな論文 - C. von Praun and T.R. Gross. OOPSLA'01. "Object Race Detection". https://dl.acm.org/doi/pdf/10.1145/504282.504288 - R. O'Callahan and J.D. Choi. PPoPP'03. "Hybrid Dynamic Data Race Detection". https://dl.acm.org/doi/pdf/10.1145/781498.781528 ## 2024/07/23 ### 既存研究 RustBelt: めっちゃ手動の検証、表現力は相当高い、自動化が難しい Stacked Borrows: アノテーションが一切不要な動的検査、保証はかなり "浅い" (所有権をきちんと検査しているわけではない) ### 動的検査 Vec については len/cap の分だけ所有権があることを見る 注意点: Vec 等の invariant は関数の途中では一旦崩れる 例: RawVec の shrink は ptr を先に設定する ### Stacked Borrows で検出されない例 これはまずい ```rs unsafe fn evil<'a, T>(mv : &'a mut Vec<T>) -> (&'a mut Vec<T>, &'a mut T) { let rv = mv.as_mut_ptr(); (mv, &mut *rv) } ``` 配列と要素への可変参照が共存している Stacked Borrows はこれの呼び出しのエラーを検出できない Aliasing XOR Mutability に違反する Vec でなく slice だったらできる ### 懸念点 既存のライブラリで evil みたいな状況を引き起こしているものはないか？ おそらくない (実際に確かめたい!) ### やること * とりあえず Vec etc. 限定で動的検査器を作ってみる * 方向性: Miri 自体の拡張 * 関数の *入出力時* の Vec の所有権チェックが必要 * 動的検査のもとで "functional" な仕様が正しく動くことを証明する * Vec なら len だけでなく cap や ptr を含めたモデル、"深い Stacked Borrows" だと要素までも見られる ### 参考になる文献 * Stacked Borrows https://plv.mpi-sws.org/rustbelt/stacked-borrows/paper.pdf * ## 2024/06/25 Dynamic borrow checker * Minimal example for which Miri cannot catch the error ```rs unsafe { let mut v = vec![0, 1, 2, 3]; let mv = &mut v; let rv = mv.as_mut_ptr(); mv[0] += 5; *rv *= 10; mv[0] += 7; println!("{:?}", v); } ``` * As a tool for validating * Other borrow checkers (NEW!) * Optimization * Functional conversion * Unsafe programs (same as Miri) Comparison between other languages and Rust (why it is easier to implement it in Rust, or is there no difference (memory model)) Start with a simple subset e.g. safe Rust + Vec with index-level borrowing (<- already an extension to the borrow checker) Or use a higher-level language (depends on which is easier) Formalizing a simple system is generally enough + proving property (functional verification) Think about how to handle the tagging of allocated but not yet used memory in the vector (c.f. LLVM poison value) https://lab8.slack.com/archives/C06UJ94N2MA/p1719298006136179 (Will copy to this document later)