修士研究発表 A Framework Using a Common Language to Build Program Verifiers for Low-Level Languages 米澤研究室吉野寿宏 <[email protected]> 背景  ネットワーク越しのコード配布の隆盛   ユーザーアプリ、OS のパッチ、ドライバ… 同時にセキュリティの脅威にもなっている    トロイの木馬、アプリケーションの脆弱性への攻撃スパイウェアどうしたらコードを信用できる/信用してもらえる？   信用できないものは実行しなければよいが、不便全てのソフトウェアを自作することは、現実的でない背景  プログラム検証    プログラムの中身を静的に検査し、安全であることを数学的に保証する手法特にセキュリティの分野で研究が盛んである低級言語プログラムの検証は TCB を削減    高級言語はコンパイルしなければ実行できない ⇒ コンパイラも信頼しなければならないアセンブラなどはコンパイラよりも小さい型付きアセンブリ言語(TAL) などの既存研究 [1] 型付きアセンブリ言語 (TAL)  実マシンのアセンブリ言語に型システムを導入  レジスタの型・メモリの中身の型などを静的に検証メモリ安全性(範囲外のメモリをアクセスしないこと) などを保証  Java VM のバイトコード検証機構と類似   [1] 実マシンのアセンブリ言語(バイナリコードでもよい)を直接検証できるため、OS パッチなどにも使用可 G. Morrisett, et al. From System F to Typed Assembly Language. In 1998 ACM SIGPLAN-SIGACT Symposium on Principles of Programming Language. 低級言語向け検証器の問題点  アーキテクチャへの依存性が強い   種々のアーキテクチャそれぞれに派生言語検証器を作ろうとするたびにアーキテクチャをモデル化する必要   検証器の実装において、大きな負担実装の移植性が悪いことがしばしば解決策  共通言語を固定し、その上に検証器を構築   言語の semantics を確定させる実際の(低級)言語から共通言語に対して変換   変換が「正しければ」(後ほど解説)、変換元のプログラムを検証しているのと等価検証器のロジックとは独立性が確保できるとよい   新しいアーキテクチャに対応する際に検証器を弄らない検証器を取り替えるときにマッピングルールを弄らない検証器を分割実装する共通言語に変換されたプログラム変換器 (2) 低級言語のプログラム検証結果 Success /Fail 検証ロジック (3) (1) 共通言語の意味論検証器本研究のアプローチ  3 つのステップ 1. 2. 3. 共通言語を設計実際の低級言語から共通言語への変換器を作成共通言語の semantics を用いて検証ロジックを作成本研究のアプローチ  3 つのステップ 1. 2. 3.  共通言語を設計実際の低級言語から共通言語への変換器を作成共通言語の semantics を用いて検証ロジックを作成本研究は特に、このうち 1. と 2. に着目  これまで 3. は数多く研究されてきているので、それらの成果を応用することができると考えられる共通言語  プログラムの変換対象となる言語   フレームワークの中核変換元は低級言語 ⇒ 特徴を生かす   意味論は確定させる   取り扱う値は整数とポインタのみインタプリタも作っておく (変換の正しさの議論に用いる) 完全性より健全性を重視   行儀の悪いプログラムは記述できずともよい意味論などは conservative に定義共通言語概要  レジスタ・メモリなどを持つ抽象機械を定義    レジスタ・メモリは多くのアーキテクチャにて採用されている通り一時的な結果を保持できる変数を導入抽象機械の状態を変更する手続き型言語  アセンブリ言語等よりも、C などに近い記法を採用    中置演算子 if 文制御構造としては、goto のみ共通言語言語構文共通言語制限事項  コードとデータを明確に分離    データの実行・コードの変更を禁止命令デコードなどのフェーズを定式化する必要がなくなり、意味論はシンプルにコードを動的生成するプログラムは表現できなくなる  他の方法でも同じことが実現できるはず (Performance Degradation を気にしなければ) 共通言語制限事項  メモリブロック同士は離れていると仮定  通常は、範囲を超えてアクセスすると隣にはみ出す   はみ出「せ」ないような semantics 設計    バッファオーバーフローなどで悪用されやすい範囲を超えたアクセスはエラーコードブロックに関しては、末尾に暗黙の jump を入れることで fall-through を表現メモリレイアウトについて何も仮定しない  Conservative な意味論定義プログラム変換器  実際の低級言語を、設計した共通言語に変換    変換元としてはアセンブリ言語などを仮定命令単位の変換アルゴリズム変換後のプログラムは元のプログラムと同じ動作をしなければならない   そうでなければ検証結果が信用できないフレームワークの中でもっとも重要な位置を占めるプログラム変換器変換アルゴリズム   アセンブリ言語の命令 = 命令種別 + 0 個以上のオペランド命令種別 ⇔ テンプレート、オペランド ⇔ パラメータ  mov( D , S ) { D := S ; } のようなルールによる対応の記述    穴の開いた箇所にオペランドを与えることによってテンプレートをインスタンス化すべての可能性を列挙する手間が省けるオペランド = 即値 | レジスタ | メモリ  即値以外は代入が可能 (出力引数) プログラム変換器変換アルゴリズム  プログラムをストリームとして扱う   命令、データ、ラベル(ブロック区切り) Reader, Writer を渡すと Reader から読んで変換   必ずしも 1 命令が 1 文に対応しない複数ブロックに跨る場合も起こりうるプログラム変換の正しさ   プログラム = 機械の状態集合上の関数変換の正しさ = 実機械状態と共通言語の抽象機械の状態の対応が任意のプログラムに関して保存状態 State 変換元のプログラム変換後のプログラム状態’ State’ プログラム変換の正しさ    実機械の状態抽象機械の状態実機械の状態集合が抽象機械の状態集合に埋め込まれる    = (レジスタ, メモリ) = (レジスタ, メモリ, 変数) 抽象機械の状態の集合から実機械の状態の集合へ total な surjection が定義できること実機械では値として整数値しか用いないことを考えれば直観的に明らか状態の対応関係を定義プログラム変換の正しさ正しさを保証するには  実機械の状態集合は有限   したがって、全数検査すれば「理論的には」検証可能しかし「現実的ではない」かもしれない   各命令の演算にかかわるオペランドのみを考慮すればよいので、各命令について 232 とか 264 とかの検査をすることにたいていの場合、境界例となる一部について検証すれば十分なことが多い  計算結果が大きく変わる場所  オーバーフローしたり、キャリーが出たりフレームワークの実装  共通言語のインタプリタを定義   変換器を定義    変換の正しさを議論するため Intel x86, SPARC の一部命令を定義変換ルール→変換器へのコンパイラを実装検証ロジックのインターフェイスを定義フレームワークの実装  Java を使用   クラス継承を用いることで拡張性を確保バイトコードの移植性が高い   Java VM さえあればどこでも動く実行するのと同じアーキテクチャ上で検証したい  ライブラリが豊富  10K LoC 程度結論  低級言語用のコード検証器のためのフレームワークを構築した  共通言語を設計したプログラム変換器について議論した  Java による実装を行った 