Formal Development of Operating Systems in Rust

Transcript

1. Formal Development of Operating Systems in Rust 第66回プログラミング・シンポジウム 尾田莉瑠(@ri5255) 1
2. 自己紹介 所属 早稲田大学基幹理工学部情報理工学科(B3) 興味 システムソフトウェア開発と形式検証 尾田莉瑠 (@ri5255) 2
3. 形式検証とは • 形式検証はプログラムが”正しい”(実装が仕様を満たす)ことを証明する手法 • 例) 配列をソートするプログラムをCreusot[1]で検証 事後条件 • 配列が昇順にソートされている • 配列が元の配列の並べ替えである ループ不変条件 • i番目のループにおいてi番目までが 昇順にソートされている • 配列が元の配列の並べ替えである 3
4. 形式検証とは • プログラムが”正しい”とは、実装が仕様を満たしていること • 仕様が間違っていれば証明できても”正しい”プログラムではない • 例) 事後条件が弱い場合 (これはソート関数ではないが証明は通る) 事後条件 • 配列が昇順にソートされている • 配列が元の配列の並べ替えである 4
5. 形式検証の利点 • 関数の動作が実装を見なくても分かる • コメントと違って機械検証可能(“正しくない”実装では証明が通らない) • コメントと違って曖昧性がない • 例) RustのBinaryHeap (同じ優先度の要素がどの順番で取り出されるかは不明) 5 • 信頼性が重要なOSカーネルに形式検証を適用するのは自然な発想
6. OSカーネルの形式検証とは • 基本的にやることは同じ • 関数の仕様を書き、実装がそれを満たすことを証明する 例) スケジュラーの仕様 (以下は[2]より引用) 事後条件 • キューの一番先頭のスレッドを返す • 返されるスレッドは実行可能である 6
7. 先行事例: seL4 • 形式検証によって”正しい”ことが保証された汎用マイクロカーネル • 以下のような性質をIsabelle/HOLで証明 • Functional Correctness (関数が仕様通りに実装されていること) • Security Properties • Integrity (許可なしに書き込みを行えないこと) • Confidentiality(許可なしに読み込みを行えないこと) • Availability(権限のないアプリケーションがDOS攻撃を行えないこと) • その他の性質 • システムコールの停止性 • NULLポインタアクセスが無いこと • ポインタが有効であること 7
8. seL4の問題点 • 証明が大変 • 下図は[3]より引用 • 同様の手法を他のOSカーネルの開発に取り入れるのは現実的に厳しい 8
9. 最近の研究動向 • Rustを用いたOSカーネルの開発と検証に関する提案[2, 4] • 現実的なコストでOSカーネルを検証可能なことが示されている(下図は[2]より引用) • seL4と同じようなことが現実的なコストで実現できる可能性がある 9
10. Rustとは • 性能と安全性を考えて設計されたシステムプログラミング言語 • Safe Rust(unsafeブロックを使わないRust)では未定義動作[5]が無いことが保証される • 例) data race, null pointer, dangling pointerへのアクセス • ただし以下は未定義動作ではない [6] • 整数オバーフロー • デッドロック • メモリリーク • ロジックエラー 例) use after freeを含むプログラム 10
11. Rustとは • コンパイラが未定義動作が起こらないことを保障できない部分にはunsafeブロックを使う • Unsafeブロックは”安全”に使うために満たすべき追加の制約があることを明示的にするためのもの • 例) Vec::get_unchecked関数 11
12. RustをOSカーネルの形式検証に使う利点 12 • RustコンパイラがCよりも強い性質を保障してくれるため、証明すべき性質が減る • seL4が証明しているいくつかの性質はRustを使うだけで保障される • 検証器がこの性質を利用できるため、効率的な検証が可能になる[1, 7] • Unsafeブロックにより追加で証明が必要な部分が明示的になる
13. 課題 • 検証器の機能不足 • 例) bit演算 • TCB(Trusted Computing Base)の大きさ • Rustコンパイラや標準ライブラリの”正しさ”は非自明 • 複雑性を抑えつつ、実用的なOSカーネルを作るには? • そもそもOSカーネルの”正しさ”とは? • 各関数が仕様通りに実装されていれば、”正しい”OSカーネルなのか? 13
14. 課題 • 検証器の機能不足 • 例) bit演算 • TCB(Trusted Computing Base)の大きさ • Rustコンパイラや標準ライブラリの”正しさ”は非自明 • 複雑性を抑えつつ、実用的なOSカーネルを作るには? • そもそもOSカーネルの”正しさ”とは? • 各関数が仕様通りに実装されていれば、”正しい”OSカーネルなのか? 14 本発表ではこれらの課題についてseL4を例に考えてみる
15. 例: seL4と割り込み • seL4は基本的に割り込み無効で動作する(Big Kernel Lock) • これにより並行性を気にしなくてよくなり、検証が簡単になる • しかし、割り込みを無効にするとレイテンシが大きくなる • そこでseL4は処理を切り替えても”安全”な箇所に「Preemption Point」を挿入している 15 例) cteRevoke関数 複雑性を抑えつつ、実用的なOSカーネルを作るには?
16. 例: seL4と割り込み • 処理を切り替えても”安全”な箇所とは不変条件が成り立つ箇所 • 例) 双方向連結リストの不変条件をVerus[7]で記述 16 head: null, tail: null prev: null, next: p1 prev: p0, next: null head: p0, tail: p1 複雑性を抑えつつ、実用的なOSカーネルを作るには?
17. 例: seL4と割り込み • ポイント: データ構造への変更は一時的に不変条件を破る • 例) 1つのエントリを持つ双方向連結リストから値を取り出す 17 head: null, tail: null prev: null, next: null head: p0, tail: p0 この間は不変条件が成り立たない 複雑性を抑えつつ、実用的なOSカーネルを作るには? 事前条件 • 不変条件が成り立つ • 長さが0より大きい 事後条件 • 不変条件が成り立つ • 先頭の値が取り出される
18. 例: seL4と割り込み • cteRevokeはリストから繰り返しエントリを削除する関数 • cteDelete関数の実行が終了するたびに不変条件が成り立つ • 故にpreemptionPointで処理を切り替えても”安全” • これはIncremental Consistencyと呼ばれる[8] 18 複雑性を抑えつつ、実用的なOSカーネルを作るには?
19. 例: seL4と動的メモリ割り当て • seL4はカーネル内で動的なメモリ割り当てを行わない • 空いている物理メモリ領域はUntypedオブジェクトとして管理される • カーネルオブジェクトを作る際はUntypedオブジェクトのRetypeメソッドを使う • 例) RetypeメソッドでTCB(Task Control Brock)オブジェクトを作成 19 Untyped Objectへのポインタ(Capability) TCBオブジェクトを作成することを表す OSカーネルの”正しさ”とは?
20. 例: seL4と動的メモリ割り当て • 動的なメモリ確保を避けるのはプロセスを”正しく”隔離するため • 動的なメモリ確保を行う場合、悪意あるプロセスが繰り返しシステムコールを呼ぶとメモ リが枯渇し、その結果他のプロセスが処理を続けられなくなる • これは本来隔離されているべきプロセスがメモリを共有していることが原因 • RetypeメソッドはUntypedオブジェクトへのポインタを要求する • Untypedオブジェクトを持っていないプロセスはカーネルオブジェクトを作ることができない • この仕組みによって各プロセスが使用できるメモリ量を制限できる 20 議論 • ”正しい”隔離とはなにか? それは形式化可能か? OSカーネルの”正しさ”とは?
21. まとめと展望 • Rustを使うことで現実的なコストでOSカーネルの検証ができる可能性がある • seL4(のサブセット)をRustで再実装して証明を付けたい(WIP) • どれだけ証明が簡単になるのかを調べたい • 新しいOSカーネルの形を模索したい • 同じ性質を保障できるなら手段はなんでもよい(ハードウェア/ソフトウェア) • Rustと形式検証を用いることで面白いOSカーネルが作れるかもしれない • 形式検証を広めていきたい • 「証明しないなんてありえない」をシステムソフトウェアの常識にしたい • 後でバグに苦しむより今証明に苦しむ方がいい 21
22. 参考 1. Xavier Denis, Jacques-Henri Jourdan, and Claude Marché. 2022. Creusot: A Foundry for the Deductive Verification of Rust Programs. In Formal Methods and Software Engineering, Adrian Riesco and Min Zhang (eds.). Springer International Publishing, Cham, 90–105. https://doi.org/10.1007/978-3-031-17244-1_6 2. Xiangdong Chen, Zhaofeng Li, Lukas Mesicek, Vikram Narayanan, and Anton Burtsev. 2023. Atmosphere: Towards Practical Verified Kernels in Rust. In Proceedings of the 1st Workshop on Kernel Isolation, Safety and Verification (KISV ’23), October 2023. Association for Computing Machinery, New York, NY, USA, 9–17. https://doi.org/10.1145/3625275.3625401 3. Gerwin Klein, June Andronick, Kevin Elphinstone, Toby Murray, Thomas Sewell, Rafal Kolanski, and Gernot Heiser. 2014. Comprehensive formal verification of an OS microkernel. ACM Trans. Comput. Syst. 32, 1 (February 2014), 1–70. https://doi.org/10.1145/2560537 4. Matthias Brun, Reto Achermann, Tej Chajed, Jon Howell, Gerd Zellweger, and Andrea Lattuada. 2023. Beyond isolation: OS verification as a foundation for correct applications. In Proceedings of the 19th Workshop on Hot Topics in Operating Systems (HOTOS ’23), June 2023. Association for Computing Machinery, New York, NY, USA, 158–165. https://doi.org/10.1145/3593856.3595899 5. The Rust Reference. https://doc.rust-lang.org/reference/behavior-considered-undefined.html 6. The Rust Reference. https://doc.rust-lang.org/reference/behavior-not-considered-unsafe.html 7. Andrea Lattuada, Travis Hance, Chanhee Cho, Matthias Brun, Isitha Subasinghe, Yi Zhou, Jon Howell, Bryan Parno, and Chris Hawblitzel. 2023. Verus: Verifying Rust Programs using Linear Ghost Types. Proc. ACM Program. Lang. 7, OOPSLA1 (April 2023), 286–315. https://doi.org/10.1145/3586037 8. Bernard Blackham, Yao Shi, and Gernot Heiser. 2012. Improving interrupt response time in a verifiable protected microkernel. In Proceedings of the 7th ACM european conference on Computer Systems, April 10, 2012. ACM, Bern Switzerland, 323–336. https://doi.org/10.1145/2168836.2168869 22