resume1

型付きアセンブリ言語を用いた
安全なカーネル拡張
前田俊行
米澤研究室
古典的なOSの問題点
• システムコールが遅い
– 割り込みやコンテキスト切替えのコストのため
遅い!
コンテキスト
切替え
プログラム
ユーザ空間
システムコール
割り込み
サービス
カーネル空間
システムコールの
オーバーヘッドを解消するには?
• プログラムをカーネル拡張としてカーネル
内で実行すればよい
– システムコールは単なる関数呼び出しになる
速い!
カーネル拡張
プログラム
システムコール
カーネル空間
サービス
任意のプログラムを
カーネル内で実行するのは危険
• 古典的なカーネル拡張の方法では、任意のメモ
リアクセスや任意のコード実行が可能なため
危ない!
悪い
プログラム
ディスクをフォーマットする
実行可能
他のプログラムを攻撃する
カーネル空間
本研究の目的
• 安全なカーネルの拡張を実現する
– 「型」によって不正なメモリアクセスやコード実行を防ぐ
• この目的ために、型付きアセンブリ言語 TAL
[Morrisett et al. 98]を用いる
安全!
悪い実行不可能
プログラム
カーネル空間
ディスクをフォーマットする
他のプログラムを攻撃する
関連研究
• SPIN [Bershad et al. 95]
– 1つの高級言語(Modula-3)に依存
• Software Fault Isolation [Wahbe et al. 93]
– 実行時のオーバーヘッドが大きい
• Proof-Carrying Code [Necula and Lee 96]
– 証明の生成が複雑で困難
• ハードウェアの仮想記憶機構による保護機能を
用いた手法
– ページ単位でしか保護できない
TALとは何か?
• 型付けされたアセンブリ言語
• 型があること以外は普通のアセンブリ言語
– レジスタ操作、メモリアクセス、分岐など
• ただし、メモリ管理にはGCを利用する
TALを用いることの利点
• 型により次の2つの安全性を保証できる
– メモリの安全性
• 不正なメモリをアクセスしないこと
– 制御フローの安全性
• 不正なコードを実行しないこと
• 機械語コードの安全性を型チェックによっ
て検証できる
– TALのアセンブラが、機械語コードと共に型情
報を生成するため
本研究のアプローチ
• カーネル拡張をTALを用いて作成する
• カーネル拡張をロードする前に型チェック
で安全性を検証する
カーネル空間
安全ならロードする
TALで作られた
カーネル拡張
型チェック
本研究のアプローチの特徴
• カーネル拡張を安全に実行できる
– メモリと制御フローの安全性が保証されるた
め
• カーネル拡張の実行効率がよい
– 実行時の安全性チェックがほぼ不要なため
• 安全性はロード時に検証される
• ただし、配列の境界チェックは実行時に行われる
本研究の手法にもとづいた
プロトタイプシステムの実装
• x86のLinuxカーネル上で実装
– カーネル拡張をカーネル内にロードする仕組み
• Linuxのカーネルモジュールロード機能を流用
– カーネル拡張からシステムコールを呼ぶ仕組み
• システムコールによって、メモリや制御フロー以上の
安全性を保証
– ファイルのパーミッションなど
• GCは未実装
カーネル拡張から
システムコールを呼ぶ仕組み
正しいアドレスに
跳ぶことを保証
TALカーネル拡張
…
call sys_read
…
シンボルを
インポート
システムコール
sys_read
…
…
ret
型をインポート
外部シンボル
sys_read =
正しい引数、返り値で int (*)(int, char*, int)
呼び出すことを保証
プロトタイプシステムを用いた
性能測定実験
• 目的
– プログラムがカーネル空間で効率よく実行されること
を確認する
• 方法
– 同一プログラムをカーネル空間、ユーザ空間で実行し、
実行時間を比較
• プログラムの作成にはTALを生成するCもどき言語
“Popcorn” [Morrisett et al. 99]を用いた
• 環境
– マシン : Pentium III 350MHz 主記憶 : 384MB
– OS
: Linux Kernel 2.4.5
実験対象プログラムその1
“getpid”
• システムコールgetpidを呼ぶだけのプログ
ラム
• システムコールのオーバーヘッドが最も大
きくあらわれる
– getpidの行う処理が簡単なため
• Pentium IIから追加された、システムコー
ルを高速に呼び出すための命令
sysenter/sysexitとも比較した
getpidの実行結果
• カーネル空間で実行することで、約19倍高速化
された
– sysenter/sysexitと比べても約10倍高速
実行時間(マイクロ秒)
getpidの実行時間の比較
1
0.985
ユーザ空間
sysenter
カーネル空間
0.54
0.5
0.052
0
実験対象プログラムその2
“find”
• ディレクトリツリーを探索するプログラム
• ディレクトリ情報がディスクキャッシュに存
在している状態で実行
– 探索したディレクトリ数 : 1396
– 探索したファイル数 : 23690
• C言語で作成したものとも比較
– PopcornとCの性能差を見るため
– 利用したCコンパイラ : gcc –O2
findの実行結果
• カーネル空間で実行することで、約1.4倍高速化
された
– PopcornとCの性能差より高速化の度合いは大きい
findの実行時間の比較
実行時間(秒)
0.15
0.148
0.142
0.103
0.1
0.05
0
ユーザ空間
(Popcorn)
ユーザ空間(C
言語)
カーネル空間
まとめ
• 型付きアセンブリ言語を用いた安全なカー
ネル拡張の手法を示した
• 本研究の手法でプログラムをカーネル内
で実行することにより、実行効率が改善さ
れることが確認できた
今後の仕事
• Webサーバーなど、より現実的なプログラ
ムもカーネル内で安全に実行できるように
する
– マルチスレッド環境における安全性を考慮

Download Report