\chapter*{要旨}
OS 自体に信頼性が求められるが、OS の全てのコードに対して検証を行うのは困難である。

本研究室で信頼性を保障するのに適したプログラミング言語 CbC を開発してきた。
CbC を使って OS の開発をすることにより、
CbC の軽量継続によりOSの動作を
状態遷移を基本としたモデルに落とし込むことができる。
これにより状態遷移機械の検証手法をOSに対して適用し信頼性を高めることができるようになると考えられる。
本研究では小型のOSであるxv6 をCbCで書き換えること
の一部を行う。具体的にはOSのメモリ管理を担当するvm.cをCbCに変換する。

CbCではインターフェースを用いたモジュール化を行う。
vm.cbcはメモリ管理(特にpaging)を行うインターフェース
と、その実装として記述される。インターフェース内部での
 CbCの接続はメタレベルの記述になる。OSで使われる
すべてのコードとデータはcontextと呼ばれるメタデータ
に記述される。contextのデータを書き換えることにより
、x.v6で仮想OSやコンテナを定義できるようになると
考えられる。

本論文では
OSの信頼性の基本であるメモリ管理部分のインターフェースと実装の記述の考察を行う。

% 既存の Gears OS でのメモリ管理では単に Page Table Entry をコピーする Fork を実装しているが、

\chapter*{Abstract}
Reliability of Operating Systems are important,
but it is difficult to verify the source code of
the Operating System.

Programming language CbC is developed in our laboratory,
which is designed to support reliability.
Operating System Project has
automaton like descriptions if it is written in CbC.
Using automaton based verification technologies,
the Operating System becomes more dependable.
In this research, we will rewrite x.v6 kernel which
is a small operating system written in C. Actually,
we will rewrite the memory management part vm.c of it using CbC.

CbC has module system called interfaces. vm.cbc is
implemented as an interface and the implementations.
In the interfaces, all connections and data structures
are written a meta data, which is called Context.
Virtual OS or so called Container can be realized as
a modification of the Context.

In this paper, we describes rewriting details of
memory management interface.