\chapter{OS の信頼性の保障}
OS を要する機器に依存している現代では、OS のバグは日常に支障を来たすことに繋がる。
実際にパスワードなしで root にアクセスできるバグや、コンピュータの日付の設定を変更するとコンピュータ自体が壊れるバグが発生した。


 OS 自体に信頼性が求められるが、複雑な機能が多く、短期間のアップデートが必要な OS では、全てのコードに対して検証を行うのは困難である。
CPU やメモリなどの資源管理は基本的には OS が行なっているため、ユーザーが信頼性を保証こともできない。
これは資源管理が複雑な上、アクセスされたり書き換えられることを防ぐためだと考えられる。
OS による資源管理によってユーザーは資源を気にすることなくコンピュータを扱うことができる。


 このように OS には資源管理やシステムコールされた後の処理などユーザーが記述するプログラム以外の部分が存在する。
その処理をメタレベルの計算、ユーザーが記述する部分をノーマルレベルの計算と呼ぶ。


 本研究室ではノーマルレベルとメタレベルの記述を行える CbC というプログラミング言語を開発してきた。
CbC は Code Gear という基本的な処理の単位と Data Gear というデータの単位を用いる。
細かい処理に対してノーマルレベルとメタレベルの Code Gear を記述し、その間を関数型プログラミング言語のように goto によって継続する。そのため、状態遷移モデルに落とし込むことができる。
Code Gear に対して入力の Data Gear と出力の Data Gear が存在し、入力に対して期待される出力がされてるか検査することで信頼性を保証する。


モデル検査には定理証明支援系である Agda を用いる。
Agda は Haure Logic という検証手法を扱うことができる。
Haure Logic は事前条件を使ってある関数を実行して事後条件を満たすことを確認する検証手法であり、継続に事前条件と事後条件を持たせることのできる CbC と相性がいい。


 CbC を使って 信頼性の保証と拡張性を持たせる Gears OS の開発を行なっている。
本論文では、
% 資源管理を行える CbC で軽量なハードウェアでも動かせるように Arm のバイナリを出力する 
Xv6 という OS を参考にした Geas OS の書き換えの説明を行う。
OS の信頼性の基本であるメモリ管理部分を書き換えることで Page のバリデーションチェックによる不正なデータの変更やサンドボックスによるエクセプションをが可能となる。
また、Gears OS のメタレベルとノーマルレベルでは書き換えなどを防ぐために見えるデータに違いが生じ、Code Gear と Meta Code Gear の記述も煩雑になる。それを解消するために、インターフェースによるモジュール化を導入した。
% インターフェースは Agda に対応するようになっている。これにより Code Gear、Data Gearんの Agda による証明が可能になるように Geas OS の構築を行った。
インターフェースを使うことで機能の入れ替えによる拡張性や Agda による証明が可能となることを目的する。

% 既存の Gears OS でのメモリ管理では単に Page Table Entry をコピーする Fork を実装
% しているが、 さらに資源管理を行える CbC で軽量なハードウェアでも動かせるように Arm のバイナリを出力する Xv6 を参考に GearsOS にメモリ管理を行う API を考察する。


% Page をいじるのは メタレベル
% しかし、ユーザー空間で資源管理を行えるようにすることで、 
% Page のバリデーションをチェックしたり、サンドボックスによる信頼性の保証を行えるようになる。また、適切な記述をすれば最適な資源管理にも繋がる。