Mercurial > hg > Papers > 2020 > tobaru-master
view slide/CbCXv6.md @ 21:6d84ce92ff35
.
| author | tobaru |
|---|---|
| date | Sat, 08 Feb 2020 18:59:42 +0900 |
| parents | 98cee2f6c919 |
| children | 49d691a92b41 |
line wrap: on
line source
# CbCインターフェースによる CbCXv6 の書き換え - 並列信頼研 - 桃原 優 --- # 概要 - OS の信頼性を保証したい - メタレベルを記述できる CbC で OS の開発 - インターフェースの導入 - 煩雑な記述の解消 - Agdaによる証明のため --- # OS の信頼性の重要性 - OS のバグは日常生活に支障をきたす - パスワードなしで root にアクセスできるバグ - 日付設定でコンピュータが壊れる - -> OS自体に信頼性が求められる --- # OS の検証 - 全てのOSのコードに対して検証を行うのは困難 - 複雑な機能が多い - 短期間のアップデート - ユーザーが検証を行うこともできない - 資源管理はOSが行なってる - そもそも資源管理が複雑 - アクセスされたり書き換えられるリスク --- # メタレベルとノーマルレベル - ノーマルレベル - ユーザーがプログラミング言語によって記述する部分の処理 - メタレベル - ユーザーが記述しないOS 側の処理 - CPU - メモリ --- # Continuation based C - ノーマルレベルとメタレベルの処理を同じ言語で行えるようにした言語(以下CbC) - Code Gear - 基本的な処理の単位 - Data Gear - データの単位 --- # goto による継続 - Code Gear の処理の間を goto によって遷移していく  --- # Data Gear の継続 - goto の際に Data Gear も継続される  --- # Meta Code Gear - 実際にはノーマルレベルの間にメタレベルの処理がある - Meta Level では Data Gear の見え方は変わる(Meta Data Gear) - 書き換えやアクセスを防ぐため  --- # 状態遷移モデル - goto の遷移によって状態遷移モデルに落とし込める - Code Gear に対しての入力に対して期待される出力がされているかで検査して**信頼性を保証する** ---- # Agda による検証 - モデル検査 - 定理証明支援系である Agda を用いる。 - Agda - Hoare Logic という検証手法を扱える。 --- # Hoare Logic - 検証手法 - 事前条件を使ってある関数を実行して事後条件を満たすことを確認する - CbCと相性がいい - 継続に事前条件(Input Data Gear)と事後条件(Output Data Gear)を持たせることができる --- # Geas OS - CbC を使って信頼性の保証と拡張性を持たせる Gears OS の開発を行なっている - Xv6 という OS を参考に書き換えをしている --- # メモリ管理 - OS の信頼性の1つであるメモリ管理部分を CbC で書き換える - Page のバリデーションチェック - サンドボックスによるエクセプション --- # インターフェース - 書き換えを防ぐために見える Data Gear に違いが生じる - -> Gears OS のノーマルレベルからメタレベルの記述が記述が煩雑になるためインターフェースを導入 - インターフェースによる他のメリット - 煩雑な記述の解消 - 機能の入れ替え - Agda による証明 --- # CbC による Gears OS の開発 --- # Context - Meta Data Gear - Code Gear - Data Gear のリスト - Data Gear を確保するメモリ空間 - スレッドやプロセスに対応 - ノーマルレベルに必要な処理のみ Code Gear に渡す - Meta Code Gear は Perlスクリプトで自動生成 - 継続先を変えることで機能を置き換えることも可能 --- # Xv6 - MIT の講義用教材として作られたOS - 企画課される前のCで書かれたUNIX V6 を書き換えた - 1万行程の軽量なOS - Linuxだと数千万行 - Xv6 を参考に CbC で書き直すことで Gears OS を実装する --- # カーネル空間 - OS の中核となるプログラムで Meta Level に相当する - Xv6 ではカーネルとユーザープログラムは分離されている - ユーザープログラムはカーネルに直接アクセスできない。 - 書き換えやアクセスを防ぐため - 呼び出す場合は system call --- # カーネルが提供するもの - プロセス管理 - メモリ管理 - ファイル管理 - I/O, read, write --- # カーネルの保護機構 - CPUのハードウェア保護機構を持っている - ユーザー空間で実行されているプロセスが自身のメモリのみアクセスできるように保護 - system call - ハードウェアが一時的に特権レベルをあげ、カーネルのプログラムが実行される --- # system call - system call 呼び出し - トラップ の発生 - ユーザープログラムの中断 - 処理がカーネルに切り替わる --- # Xv6-rpi - Xv6 は Arm のバイナリを出力するので様々なハードウェアで動かすことができる - Raspberry Pi - 携帯電話 - 実際にRaspberry Pi で動かすために xv6-rpi を用意して動作しているか確認中 - CbCxv6 とは別のプロジェクト --- # CbCXv6 での Paging - OS の信頼性の1つであるメモリ管理部分の書き換えについて説明 --- # 実メモリの直接操作 - 実メモリを直接扱うと様々な問題が生じる - ユーザープログラムで空いているメモリ番地を探す必要 - フラグメンテーションが起こる - メモリ間に扱うには小さな隙間ができる --- # Paging - メモリ管理の手法 - Page と呼ばれる固定長のブロックに分割して、メモリとスワップ領域で Page を入れ替えて管理 - 仮想メモリとして扱うことでフラグメンテーションの解消と空き番地を探す必要がなくなる --- # Pagingの図 - 必要？  --- # メタレベルでの Paging の操作 - Page Table に相当するデータを Input Data Gear で受け取って変更した後、Context にある Meta Data Gear に goto で遷移してアクセス - メタレベルで処理することで本来カーネル側の処理である Page Table を操作できる --- # Paging の信頼性 - Input Data Gear に対しての Output Data Gear をバリデーションチェックすることで他のプロセスから書き換えられることを防ぐ - サンドボックス - 他のプロセスから書き換えられた時にエクセプションを飛ばす --- # Paging の書き換え - Xv6 では実メモリから仮想メモリの変換をvm.cで行なっている。 - 次の章で書き換えについて説明する --- # CbC インターフェースの導入 - 継続の記述が煩雑になる - Code Gear がどの Data Gear の番号に対応するか指定する必要がある - ノーマルレベルとメタレベルで Data Gear の見え方が異なるため調整する必要がある - ->インターフェースの導入 --- # CbC インターフェース - インターフェースは Data Gear に対しての操作を行う Code Gear - 実装は別で定義し、呼び出す - インターフェースによって機能を置き換えることができる --- # インターフェースの定義 - Data Gear と Data Gear に対して操作を行う Code Gear の集合を表現する **Meta Data Gear** --- # インターフェースのソースコード - vm.c をインターフェースで書き換えた vm.h のコードの説明をしていく --- # 実装名の定義 - typedef struct の直後に実装名(vm)を書く ``` c typedef struct vm<Type,Impl> { ``` --- # Code Gear の定義 - Code Gear は __Code CodeGear名(引数); で記述する - 第1引数の Impl* vm が Code Gear の型になる - 初期化された Data Gear が それぞれの Code Gear の引数として扱われる - 例)定義された uinit が kpt_freerange の Code Gear の第1引数と対応している ``` c typedef struct vm<Type,Impl> { __code init_vmm(Impl* vm, __code next(...)); __code kpt_freerange(Impl* vm, uint low, uint hi, __code next(...)); __code kpt_alloc(Impl* vm ,__code next(...)); __code switchuvm(Impl* vm ,struct proc* p, __code next(...)); __code init_inituvm(Impl* vm, pde_t* pgdir, char* init, uint sz, __code next(...)); __code loaduvm(Impl* vm,pde_t* pgdir, char* addr, struct inode* ip, uint offset, uint sz, __code next(...)); __code allocuvm(Impl* vm, pde_t* pgdir, uint oldsz, uint newsz, __code next(...)); ``` --- # next(...) - __code next(...) は条件分岐によって複数の継続先が設定される - それぞれの Code Gear の引数の1つに設定する ``` c __code kpt_freerange(Impl* vm, uint low, uint hi, __code next(...)); .... __code next(...); } vm; ``` --- # インターフェースの実装 - インターフェースの実装は別ファイルで定義する(vm_impl.cbc) - ヘッダーファイルの呼び出しは #include ではなく #interface で呼び出す ``` c #include "../../context.h" #interface "vm.h" ``` --- # create_impl - create_imple の関数内で vm の型を定義し、vm->CodeGear名 で対応させていく - 実装を Code Gear で記述していく。 ``` c vm* createvm_impl(struct Context* cbc_context) { struct vm* vm = new vm(); .... vm->void_ret = C_vm_void_ret; vm->init_vmm = C_init_vmmvm_impl; vm->kpt_freerange = C_kpt_freerangevm_impl; vm->kpt_alloc = C_kpt_allocvm_impl; ... __code init_vmmvm_impl(struct vm_impl* vm,__code next(...)) { initlock(&kpt_mem.lock, "vm"); kpt_mem.freelist = NULL; goto next(...); } ``` --- # private - CbC は信頼性を保証するためにそれぞれの Code Gear を細かくする必要があるので、for文やif文がある場合はさらに実装を分ける - Code Gear は基本的にインターフェースで指定された Code Gear 内からのみ継続さ れるため、Java の private メソッドのように扱われる。 - 実際に vm.c の loaduvm の実装を分けた記述を説明する ``` c int loaduvm (pde_t *pgdir, char *addr, struct inode *ip, uint offset, uint sz) { uint i, pa, n; pte_t *pte; if ((uint) addr % PTE_SZ != 0) { panic("loaduvm: addr must be page aligned"); } for (i = 0; i < sz; i += PTE_SZ) { if ((pte = walkpgdir(pgdir, addr + i, 0)) == 0) { panic("loaduvm: address should exist"); } pa = PTE_ADDR(*pte); if (sz - i < PTE_SZ) { n = sz - i; } else { n = PTE_SZ; } if (readi(ip, p2v(pa), offset + i, n) != n) { return -1; } } return 0; } ``` --- # goto private - vm と同じ create_impl 内で vm_impl を定義し、private で実装する Code Gear を定義する - loaduvmvm_impl で goto によって private に遷移する ``` c vm* createvm_impl(struct Context* cbc_context) { ... struct vm_impl* vm_impl = new vm_impl(); ... vm_impl->loaduvm_ptesize_check = C_loaduvm_ptesize_checkvm_impl; .... vm->loaduvm = C_loaduvmvm_impl; .... } __code loaduvmvm_impl(struct vm_impl* vm, pde_t* pgdir, char* addr, struct inode* ip, uint offset, uint sz, __code next(...)) { Gearef(cbc_context, vm_impl)->pgdir = pgdir; Gearef(cbc_context, vm_impl)->addr = addr; Gearef(cbc_context, vm_impl)->ip = ip; Gearef(cbc_context, vm_impl)->offset = offset; Gearef(cbc_context, vm_impl)->sz = sz; Gearef(cbc_context, vm_impl)->next = next; goto loaduvm_ptesize_checkvm_impl(vm, next(...)); } ``` --- # private のヘッダー - private 側のヘッダーファイルも vm_impl と同じように用意する ``` c typedef struct vm_impl<Impl, Isa> impl vm{ ... __code loaduvm_ptesize_check(Type* vm_impl, uint i, pte_t* pte, uint sz, __code next(int ret, ...)); ``` --- # private の記述 ``` c #interface "vm_impl.h" __code loaduvm_ptesize_checkvm_impl(struct vm_impl* vm_impl, __code next(int ret, ...)) { char* addr = vm_impl->addr; if ((uint) addr %PTE_SZ != 0) { // goto panic } goto loaduvm_loopvm_impl(vm_impl, next(ret, ...)); } ``` - vm.cではここから for だが CbC は if文の中と外にgoto を用意して実装する  ```c __code loaduvm_loopvm_impl(struct vm_impl* vm_impl, __code next(int ret, ...)) { uint i = vm_impl->i; uint sz = vm_impl->sz; if (i < sz) { goto loaduvm_check_pgdir(vm_impl, next(ret, ...)); } goto loaduvm_exit(vm_impl, next(ret, ...)); } __code loaduvm_check_pgdir(struct vm_impl* vm_impl, __code next(int ret, ...)) { pte_t* pte = vm_impl->pte; pde_t* pgdir = vm_impl->pgdir; uint i = vm_impl->i; char* addr = vm_impl->addr; uint pa = vm_impl->pa; if ((pte = walkpgdir(pgdir, addr + i, 0)) == 0) { // goto panic } pa = PTE_ADDR(*pte); vm_impl->pte = pte; vm_impl->pgdir = pgdir; vm_impl->addr = addr; vm_impl->pa = pa; goto loaduvm_check_PTE_SZ(vm_impl, next(ret, ...)); } __code loaduvm_check_PTE_SZ(struct vm_impl* vm_impl, __code next(int ret, ...)) { uint sz = vm_impl->sz; uint i = vm_impl->i; uint n = vm_impl->n; struct inode* ip = vm_impl->ip; uint pa = vm_impl->pa; uint offset = vm_impl->offset; if (sz - i < PTE_SZ) { n = sz - i; } else { n = PTE_SZ; } if (readi(ip, p2v(pa), offset + i, n) != n) { ret = -1; goto next(ret, ...); } vm_impl->n = n; goto loaduvm_loopvm_impl(vm_impl, next(ret, ...)); } __code loaduvm_exit(struct vm_impl* vm_impl, __code next(int ret, ...)) { ret = 0; goto next(ret, ...); } ``` ``` c int loaduvm (pde_t *pgdir, char *addr, struct inode *ip, uint offset, uint sz) { uint i, pa, n; pte_t *pte; if ((uint) addr % PTE_SZ != 0) { panic("loaduvm: addr must be page aligned"); } for (i = 0; i < sz; i += PTE_SZ) { if ((pte = walkpgdir(pgdir, addr + i, 0)) == 0) { panic("loaduvm: address should exist"); } pa = PTE_ADDR(*pte); if (sz - i < PTE_SZ) { n = sz - i; } else { n = PTE_SZ; } if (readi(ip, p2v(pa), offset + i, n) != n) { return -1; } } return 0; } ``` # インターフェースの呼び出し - 定義したインターフェースの呼び出しについて説明する - CbC の場合 goto による 遷移を行うので、関数呼び出しのように goto 以降のコードを実行できない - 例) goto すると戻ってこれないため それ以降が実行されなくなる。 ``` c void userinit(void) { struct proc* p; extern char _binary_initcode_start[], _binary_initcode_size[]; p = allocproc(); initContext(&p->cbc_context); initproc = p; if((p->pgdir = kpt_alloc()) == NULL) { panic("userinit: out of memory?"); } goto cbc_init_vmm_dummy(&p->cbc_context, p, p->pgdir, _binary_initcode_start, (int)_binary_initcode_size); p->sz = PTE_SZ; // craft the trapframe as if memset(p->tf, 0, sizeof(*p->tf)); ~ ``` # 呼び出しの解決 - 最初の命令は next で戻ってこれるので、dummy の関数を用意してそこで実行する ``` c void dummy(struct proc *p, char _binary_initcode_start[], char _binary_initcode_size[]) { // inituvm(p->pgdir, _binary_initcode_start, (int)_binary_initcode_size); goto cbc_init_vmm_dummy(&p->cbc_context, p, p->pgdir, _binary_initcode_start, (int)_binary_initcode_size); } __ncode cbc_init_vmm_dummy(struct Context* cbc_context, struct proc* p, pde_t* pgdir, char* init, uint sz){//:skip struct vm* vm = createvm_impl(cbc_context); // goto vm->init_vmm(vm, pgdir, init, sz , vm->void_ret); Gearef(cbc_context, vm)->vm = (union Data*) vm; Gearef(cbc_context, vm)->pgdir = pgdir; Gearef(cbc_context, vm)->init = init; Gearef(cbc_context, vm)->sz = sz ; Gearef(cbc_context, vm)->next = C_vm_void_ret ; goto meta(cbc_context, vm->init_inituvm); } void userinit(void) { struct proc* p; extern char _binary_initcode_start[], _binary_initcode_size[]; p = allocproc(); initContext(&p->cbc_context); initproc = p; if((p->pgdir = kpt_alloc()) == NULL) { panic("userinit: out of memory?"); } dummy(p, _binary_initcode_start, _binary_initcode_size); ```