型付きアセンブリ言語を用いた安全なカーネル拡張

Presentation on theme: "型付きアセンブリ言語を用いた安全なカーネル拡張"— Presentation transcript:

1 型付きアセンブリ言語を用いた安全なカーネル拡張
前田俊行 米澤研究室

2 古典的なOSの問題点 システムコールが遅い 遅い! 割り込みやコンテキスト切替えのコストのため コンテキスト 切替え プログラム サービス
ユーザ空間 カーネル空間

3 システムコールの オーバーヘッドを解消するには?
プログラムをカーネル拡張としてカーネル内で実行すればよい システムコールは単なる関数呼び出しになる 速い! カーネル拡張 プログラム サービス システムコール カーネル空間

4 任意のプログラムを カーネル内で実行するのは危険
古典的なカーネル拡張の方法では、任意のメモリアクセスや任意のコード実行が可能なため 危ない! 悪い プログラム ディスクをフォーマットする 実行可能 他のプログラムを攻撃する カーネル空間

5 本研究の目的 安全! 安全なカーネルの拡張を実現する
「型」によって不正なメモリアクセスやコード実行を防ぐ この目的ために、型付きアセンブリ言語 TAL [Morrisett et al. 98]を用いる 安全! 悪い プログラム ディスクをフォーマットする 実行不可能 他のプログラムを攻撃する カーネル空間

6 関連研究 SPIN [Bershad et al. 95]
1つの高級言語(Modula-3)に依存 Software Fault Isolation [Wahbe et al. 93] 実行時のオーバーヘッドが大きい Proof-Carrying Code [Necula and Lee 96] 証明の生成が複雑で困難 ハードウェアの仮想記憶機構による保護機能を用いた手法 ページ単位でしか保護できない

7 TALとは何か? 型付けされたアセンブリ言語 型があること以外は普通のアセンブリ言語 レジスタ操作、メモリアクセス、分岐など
ただし、メモリ管理にはGCを利用する

8 TALを用いることの利点 型により次の2つの安全性を保証できる 機械語コードの安全性を型チェックによって検証できる メモリの安全性
不正なメモリをアクセスしないこと 制御フローの安全性 不正なコードを実行しないこと 機械語コードの安全性を型チェックによって検証できる TALのアセンブラが、機械語コードと共に型情報を生成するため

9 本研究のアプローチ カーネル拡張をTALを用いて作成する カーネル拡張をロードする前に型チェックで安全性を検証する カーネル空間
安全ならロードする TALで作られた カーネル拡張 型チェック

10 本研究のアプローチの特徴 カーネル拡張を安全に実行できる カーネル拡張の実行効率がよい メモリと制御フローの安全性が保証されるため
実行時の安全性チェックがほぼ不要なため 安全性はロード時に検証される ただし、配列の境界チェックは実行時に行われる

11 本研究の手法にもとづいた プロトタイプシステムの実装
x86のLinuxカーネル上で実装 カーネル拡張をカーネル内にロードする仕組み Linuxのカーネルモジュールロード機能を流用 カーネル拡張からシステムコールを呼ぶ仕組み システムコールによって、メモリや制御フロー以上の安全性を保証 ファイルのパーミッションなど GCは未実装

12 カーネル拡張から システムコールを呼ぶ仕組み
正しいアドレスに 跳ぶことを保証 システムコール sys_read シンボルを インポート TALカーネル拡張 … call sys_read … ret カーネルは呼ばせたいシステムコールをシンボルとして公開する TALカーネル拡張では外部シンボルを用いて呼び出すように書く 不正なアドレスへジャンプすることが防げる また、関数の型もインポートする 不正な引数や返り値を与えることを防げる 型をインポート sys_read = int (*)(int, char*, int) 外部シンボル 正しい引数、返り値で呼び出すことを保証

13 プロトタイプシステムを用いた 性能測定実験
目的 プログラムがカーネル空間で効率よく実行されることを確認する 方法 同一プログラムをカーネル空間、ユーザ空間で実行し、実行時間を比較 プログラムの作成にはTALを生成するCもどき言語 “Popcorn” [Morrisett et al. 99]を用いた 環境 マシン : Pentium III 350MHz 主記憶 : 384MB OS : Linux Kernel 2.4.5

14 実験対象プログラムその1 “getpid” システムコールgetpidを呼ぶだけのプログラム
システムコールのオーバーヘッドが最も大きくあらわれる getpidの行う処理が簡単なため Pentium IIから追加された、システムコールを高速に呼び出すための命令sysenter/sysexitとも比較した

15 getpidの実行結果 カーネル空間で実行することで、約19倍高速化された sysenter/sysexitと比べても約10倍高速
gpid * times [USER] real 0m0.992s user 0m0.430s sys 0m0.560s [KERNEL] real 0m0.061s user 0m0.000s sys 0m0.060s

16 実験対象プログラムその2 “find” ディレクトリツリーを探索するプログラム ディレクトリ情報がディスクキャッシュに存在している状態で実行
探索したディレクトリ数 : 1396 探索したファイル数 : 23690 C言語で作成したものとも比較 PopcornとCの性能差を見るため 利用したCコンパイラ : gcc –O2

17 findの実行結果 カーネル空間で実行することで、約1.4倍高速化された PopcornとCの性能差より高速化の度合いは大きい [USER]
real 0m0.148s user 0m0.050s sys 0m0.100s [KERNEL] real 0m0.103s user 0m0.000s

18 まとめ 型付きアセンブリ言語を用いた安全なカーネル拡張の手法を示した
本研究の手法でプログラムをカーネル内で実行することにより、実行効率が改善されることが確認できた

19 今後の仕事 Webサーバーなど、より現実的なプログラムもカーネル内で安全に実行できるようにする マルチスレッド環境における安全性を考慮