カーネルランド Rust 勉強会 #2; Rust の unsafe

5/28 に開催した「カーネルランド Rust 勉強会 #2」で使ったスライドに加筆したもの。Rust の unsafe の説明と、形式的検証の取組を紹介しました。

Transcript

1. カーネルランド Rust 勉強会 #2 古賀信哉 株式会社アットマークテクノ
2. 今日のネタ Rust の安全性と unsafe contract と仕様駆動開発 Rust と形式的検証 (formal verification)
3. Rust の安全性と unsafe カーネルランドでは避けられない unsafe Rust の安全性とは何か unsafe は、どのように安全じゃないのか Rust の言語仕様が提供する仕組み 静的型付けによる静的検査 メモリ操作の制約（GC 無しのメモリ管理）
4. Rust の安全性と unsafe メモリ操作の制約（GC 無しのメモリ管理） mutable な大域変数のアクセスを禁止 ポインタの間接参照（逆参照）を禁止 値（メモリ領域）の所有者とスコープ 値（メモリ領域）の参照とスコープ
5. Rust の安全性と unsafe メモリ操作の制約（GC 無しのメモリ管理） mutable な大域変数のアクセスを禁止 ポインタの間接参照（逆参照）を禁止 値（メモリ領域）の所有者とスコープ 値（メモリ領域）の参照とスコープ 複数スレッド間のデータアクセス 競合問題を排除
6. Rust の安全性と unsafe メモリ操作の制約（GC 無しのメモリ管理） mutable な大域変数のアクセスを禁止 ポインタの間接参照（逆参照）を禁止 値（メモリ領域）の所有者とスコープ 値（メモリ領域）の参照とスコープ ポインタ型の値を作ることはできる： ・値の参照からポインタ値を作る ・ポインタ変数に数値を代入する しかし、ポインタの逆参照は禁止。
7. Rust の安全性と unsafe 値（メモリ領域）のスコープと所有者 構文スコープによる値の生存スコープ 単一の所有者と、代入による所有先の移動 明示的な参照カウンタ型 基本型に対するコピーのセマンティクス Copy trait: コピーセマンティクスの宣言
8. Rust の安全性と unsafe 値（メモリ領域）の参照とスコープ 参照の生存期間と値の生存期間 共有参照と変更可能な参照 (shared, mutable) 参照の借用 (borrow) 関数の入出力引数 変更参照のエイリアスを禁止 ・同じ値に対する参照と変更可能な参照 ・同じ値に対する複数の変更参照
9. Rust の安全性と unsafe unsafe だと許されること ポインタの逆参照 mutable な大域変数のアクセス unsafe な関数の呼び出し unsafe な trait の実装 カーネルランドでは必須！ 標準ライブラリ内部でも必要
10. Rust の安全性と unsafe Rust の unsafe の考え方（C# と比較） C#（の現在の）仕様 ⚫ unsafe な executable は全て unsafe Rust の仕様 ⚫ unsafe を safe なコードが内包できる！ モジュールの public でない部分のみ unsafe に推奨される作法： ・contract の記述（事前条件、事後条件） C++ における例外仕様に通じる？ C# の新仕様でも
11. Rust の安全性と unsafe Rust に導入されつつある contract 関数の属性／アノテーションとして記述 requires, ensures, invariant ⚫ 関数の仕様記述としての contract contract の情報を利用して、呼出し側と 呼び出される側の正しさをそれぞれ検証 できればベスト。 標準ライブラリの実装に対する検証の活動（後述）
12. contract と仕様駆動開発 AI 支援 SDD のテクニカルペーパー https://arxiv.org/html/2602.00180v1#S6 仕様としての contract ⚫ API 仕様化ツール (OpenAPI) ⚫ BDD (Behavior Driven Dev.) のシナリオ ⚫ ユースケース記述（事前条件、事後条件） 曖昧さのない、必要最小限の仕様： 生成 AI に、明確な context で指示することにより、 出力されるコードの精度が上がる。 ←間違いを最大50%削減できるという研究結果あり。
13. Rust と形式的検証 Rust Foundation によるinitiative 標準ライブラリの検証 検証ツールの導入 ⚫ Kani ⚫ GOTO-Transcoder ⚫ ESBMC model checker ⚫ VeriFast ⚫ Flux
14. Rust と形式的検証 Rust Foundation によるinitiative 標準ライブラリの検証 検証ツールの導入 ⚫ Kani ⚫ GOTO-Transcoder ⚫ ESBMC model checker ⚫ VeriFast ⚫ Flux https://model-checking.github.io/verify- rust-std/intro.html https://github.com/model-checking/verify- rust-std unsafe なコードに対する 検証
15. Rust と形式的検証 Rust Foundation によるinitiative 標準ライブラリの検証 検証ツールの導入 ⚫ Kani ⚫ GOTO-Transcoder ⚫ ESBMC model checker ⚫ VeriFast ⚫ Flux https://github.com/model-checking/kani https://github.com/esbmc/goto- transcoder/blob/main/docs/Architecture.md https://github.com/esbmc/esbmc https://github.com/verifast/verifas https://flux-rs.github.io/flux/
16. Rust と形式的検証 その他の形式的検証ツール Creusot ⚫ Coma（中間検証言語） ⚫ Why3（演繹的な検証器） rocq-of-rust ⚫ Rocq（以前の Coq）を利用 ⚫ Rust の型付き中間言語から Rocq に変換 ⚫ その後は手作業を交えて（？）検証 https://github.com/creusot-rs/creusot https://coma.paulpatault.fr/ https://why3.org/ https://github.com/formal-land/rocq-of-rust