型付きアセンブリ言語の一般化吉野寿宏 (東京大学米澤研究室) <[email protected]> 背景  Mobile Code の隆盛便利なことは多い  スパイウェアやトロイの木馬などの脅威も   信用のおけないコードの取り扱い実行しなければいい → すべて自分で手作りするわけにも…  どうやったら配布されているコードを信用できる/してもらえるか？  関連技術: 電子署名コードの出自を保証  悪意のあるコードを含まないことは保証できない    コードの正統性・同一性を保証する中身を保証する技術ではないハッシュ値 h 公開鍵暗号化 {h}Kpri コード {h}Kpri D(Kpub, {h}) H(M) ハッシュ値 h ハッシュ値 h’ h= h’ ? 関連技術: [1] Proof-Carrying Code  コードが安全である数学的証明を添付    受け取った側は、ツールで安全性を検証検証に通ったコードは信用できる安全証明コードこのコードは安全です数学的理論に基づいた中身の検証が可能 [1] G. Necula. Proof-Carrying Code. In POPL97 安全ポリシー関連技術: Java VM  バイトコード検証機構バイトコードの型検査  コンパイル時の静的型が正しくない場合に有効  ライブラリのバージョンを途中で変えたり  一部のファイルを再コンパイルしたり   しかし、Java であるがゆえに  デバイスドライバ等、システムの基幹部分に応用が難しい型付きアセンブリ言語(TAL)  アセンブリ言語に型を導入   [2] レジスタの型・メモリの中身の型を静的に検証 Java のバイトコード検証のアプローチを実 CPU 向けのアセンブリ言語に適用  システムソフトウェアなどにも応用がきく [2] G. Morrisett, et al. TALx86: A Realistic Typed Assembly Language. 1999 ACM SIGPLAN Workshop on Compiler Support for System Software TAL による検証の流れ  アセンブリコードに annotation を挿入    レジスタの型スタックの型各 annotation について型を検証してゆく mov eax,ecx inc eax mov ebx,0 jmp test body: {eax: B4, add ebx,eax test: {eax: B4, dec eax cmp eax,0 jg body ; i = n ; ++i ; s = 0 ebx: B4} ; s += i ebx: B4} ; --i; ; i > 0 EAX は 4-byte integer を持つ EBX は 4-byte integer を持つ応用例: デバイスドライバ  デバイスドライバの安全性 WindowsXP: 署名がない場合に警告を表示  オオカミ少年的状況   署名されていないドライバが数多い    私が知る限り、ちゃんと署名されていたドライバってあまり見た記憶がない… 署名されていないからといって、ハードウェア用ドライバのインストールを中断するか？安全性を数学的に検証することによって、動機付けを強くする応用例: BREW  携帯分野への応用   個人情報を取り扱う端末 = 頑健でなくてはならない BREW アプリの登場    低レベルなコード(C++ などで記述)を実行させる技術現在では認証を通った公式コンテンツプロバイダのみが使用可能 TAL 検証系を利用すれば、サードパーティーのコード安全性を検証可   認証を受けなくても BREW 使用可能に開発者側の幅が広がるのではしかし…  現存する実装は一部 CPU に限られる本家では x86 専用のツールを配布 → http://www.cs.cornell.edu/talc/  ほかにもアーキテクチャはたくさんある    PowerPC, Alpha, ARM, … その他のアーキテクチャの取り扱いは？  システムを毎回独立に作成する必要   コスト高すぎませんか書式が一定でないかもしれない統一的な実装に向けて  CPU のできることは皆だいたい同じ  計算機の構成レジスタがあって、  メモリ(スタック、ヒープ、グローバル変数)があって   算術演算、メモリ操作、関数呼び出しなどの命令 → 共通化した型理論が構築できないか？目指すべきもの  CPU 非依存な、アセンブリ言語レベルでの型検査システム IA-32 Alpha SPARC ARM IA-32 定義 Alpha 定義 SPARC 定義 ARM 定義共通型検査エンジン複数のアーキテクチャを統一的に扱えるようなシステム CPU 非依存な型システム  Modular な型の処理・検証  CPU の実体とできるだけ癒着しないように CPU 依存の部分を分離して記述するように  あるいは、CPU 定義を読んで型処理コードを出力するようなコードジェネレータを作成する   既存のアセンブラに組み込めることを想定  たとえば GNU as などに組み込めたら、利用しやすいのでは目指すべきものまたは、  実 CPU の機械語にほぼ straightforward な変換ができる型安全な中間言語 C/C++ コンパイラ Objective Caml … 中間言語処理系(型検証エンジン) IA-32 Alpha SPARC ARM トランスレータトランスレータトランスレータトランスレータ IA-32 Alpha SPARC ARM 型安全な中間言語を定義する  実機の機械語とほぼ一対一対応する言語   簡単なトランスレータで各アーキテクチャに対応型の処理系は一つで済む  高級言語からのコンパイラが、その分必要になるが… 困難な点ポインタの操作  CPU specific な命令の処理  たとえば、IA-32 の LGDT 命令は他の CPU ではどうなる？  デバイスドライバなど、ハードウェアに近いコードを検証する場合には必要   外部ライブラリとの連携特定のレジスタによる値渡しなどの処理  特に、中間言語のアプローチだとどうか？ 