POPLミーティング 5/11 型付きアセンブリ言語の 一般化実装に関する展望 米澤研 M2 吉野 寿宏 <tossy-2@yl.is.s.u-tokyo.ac.jp>

本日の Agenda 型付きアセンブリ言語 TALx86 TAL の一般化実装の可能性について 背景 概要・関連技術 概要 着想・要件

型付きアセンブリ言語

背景 ネットワーク越しのコード配布の隆盛 同時に不正なコードの脅威も蔓延 どうしたら、コードを信用できる/信用してもらえるか？ アプリケーションから、OS のパッチやドライバまで 同時に不正なコードの脅威も蔓延 どうしたら、コードを信用できる/信用してもらえるか？ ユーザとしては、実行しなければよいのだが、不便 ソフトウェア作成者としては、信用してもらうことでユーザの獲得につながる 全てのソフトウェアを自作することは現実的でない

悪意のあるコードを 含まないことは保証 できない 関連技術: 電子署名 コードの出自を保証 悪意のあるコードを 含まないことは保証 できない コードの正統性・ 同一性を保証するが 中身を保証する技術ではない 公開鍵暗号化 ハッシュ値 h {h}Kpri コード ハッシュ値 h H(M) D(Kpub, {h}) {h}Kpri ハッシュ値 h’ h = h’ ?

関連技術: Proof-Carrying Code[1] コードが安全である数学的証明を添付 受け取った側は、ツールで安全性を検証 検証に通ったコードは数学的に信用できる 数学的理論に基づいた、中身の検証が可能 安全証明 コード このコードは安全です 安全 ポリシー [1] G. Necula. Proof-Carrying Code. In POPL97

バイトコード検証機構 しかし、Java であるがゆえに 関連技術: Java VM バイトコードの型検査 そもそも型安全になるような設計 メソッドの型情報などをオブジェクトファイルに格納 コンパイル時の静的型が正しくない場合に有効 ライブラリのバージョンを途中で変えたり、一部のファイルを再コンパイルしたり しかし、Java であるがゆえに デバイスドライバ等、基幹部分への応用は難しい Java 以外の言語からのコンパイルは想定されない

型付きアセンブリ言語(TAL)[2] 実マシンのアセンブリ言語に型を導入 Java VM のバイトコード検証にヒント レジスタの型・メモリの中身の型などを静的に検証 型システムの完全性・健全性を証明することで、検証の妥当性をも含めて保証 [2] G. Morrisett, et al. From System F to Typed Assembly Language. In 1998 ACM SIGPLAN-SIGACT Symposium on Principles of Programming Language. [3] G. Morrisett, et al. TALx86: A Realistic Typed Assembly Language. 1999 ACM SIGPLAN Workshop on Compiler Support for System Software.

TAL の定式化 TAL の文法定義 操作的意味論の定義 型の導入 基本は、RISC マシンによくある命令セット ヒープの操作 3 operands 命令 ヒープの操作 malloc 解放は GC pack/unpack 操作 操作的意味論の定義 ほぼ直感的 型の導入

デバイスドライバ デバイスドライバの安全性 安全性を数学的に検証することによって、動機付けを強くする WindowsXP: 署名がない場合に警告を表示 オオカミ少年的状況になっているのでは？ 署名されていないドライバが数多い 私が知る限り、ちゃんと署名されていたドライバってあまり見た記憶がない… 署名されていないからといって、ハードウェア用 ドライバのインストールを中断するか？ 安全性を数学的に検証することによって、動機付けを強くする

BREW 携帯分野への応用 TAL 検証系を利用すれば、サードパーティーのコード安全性を検証可 個人情報を取り扱う端末 = 頑健でなくてはならない BREW アプリの登場 低レベルなコード(C++ などで記述)を実行させる技術 現在では認証を通った公式コンテンツプロバイダのみが 使用可能 TAL 検証系を利用すれば、サードパーティーのコード安全性を検証可 認証を受けなくても BREW 使用可能に 開発者側の幅が広がるのでは

TALx86

TALx86 Morrisett らは、Intel x86 向けの処理系を公開 実装に関する論文[3] OCaml で記述されており、ツール群全体で 約 7 万行 (!) (コンパイル全然通らないんですけど…) 実装に関する論文[3] 実装したツール群に関する紹介的な意味合い？ 詳しいところはあまりない([4] が少し詳しい) [3] G. Morrisett, et al. TALx86: A Realistic Typed Assembly Language. 1999 ACM SIGPLAN Workshop on Compiler Support for System Software. [4] http://www.cs.washington.edu/homes/djg/slides/talx86_wcsss_talk.pdf

TALx86 アセンブリ言語ツール Popcorn C 言語のサブセットから TAL へのコンパイラ talc 型検査ツール アセンブラ 機械語への変換 Link-verifier リンケージの安全性を検査 Popcorn C 言語のサブセットから TAL へのコンパイラ Scheme Popcorn で書かれた scheme インタプリタ

EAX は 4-byte integer を持つ EBX は 4-byte integer を持つ TAL による検証の流れ アセンブリコードに annotation を挿入 基本ブロックの入り口に 記述 レジスタの型・スタックの型 各 annotation について 型を検証 各命令の操作的意味論 ブロックに流入するところで 入り口条件を満足するか mov eax,ecx ; i = n inc eax ; ++i mov ebx,0 ; s = 0 jmp test body: {eax: B4, ebx: B4} add ebx,eax ; s += i test: {eax: B4, ebx: B4} dec eax ; --i; cmp eax,0 ; i > 0 jg body EAX は 4-byte integer を持つ EBX は 4-byte integer を持つ

TAL による検証の流れ 検証 エンジン アセンブラ ・リンカ TAL ソースコード 実行可能 コード talc TAL インターフェイス mov add jmp… 外部ライブラリ 010001011101010 0010 talc アセンブラ ・リンカ TAL ソースコード 実行可能 コード val f: int -> int … 検証 エンジン 検証結果 TAL インターフェイス 外部ライブラリ インターフェイス

TAL の一般化実装の 可能性について

CPU は一種類ではない プロセッサはいろいろな種類 各 CPU ごとに処理系を作成する必要 x86, PowerPC, SPARC, ARM, SuperH, … PC 用としては x86 (互換)が多いが 携帯デバイスだと ARM や SH が多い 各 CPU ごとに処理系を作成する必要 CPU が違えば命令セットも異なる

別のアーキテクチャに対応させる 最初から作るのは面倒であるし 現在ある TAL の実装を他のプロセッサ向けに書き換えると しかし、TALx86 は(コードをざっと見た感じ)実装のかなり中枢において x86 に依存している マシン状態、浮動小数点レジスタのスタック(というかリング)構造 命令セットを variant で列挙してるし (!) など どこまで作り直す必要があるか？

コンパイルの流れ 高級言語 中間言語 アセンブリ 機械語 mov add jmp… 0100101 1011101 0101011 00101… 機械語

コンパイルの流れ (複数アーキテクチャ) 機種ごとの TAL 処理系 高級言語 x86 Alpha PPC 中間言語 mov add jmp… アセンブリ 高級言語 0100101 1011101 0101011 00101… 機械語 Alpha 中間言語 mov add jmp… アセンブリ 0100101 1011101 0101011 00101… 機械語 PPC 中間言語 mov add jmp… アセンブリ 0100101 1011101 0101011 00101… 機械語

着想 アーキテクチャが変わっても、CPU の構成 自体はあまり変わらない → これらの共通項を、理論として定式化できない だろうか？ レジスタがいくつかあり、メモリ(スタック･ヒープ・ グローバル変数)があって その間で計算を行ったり、関数を呼び出したりする → これらの共通項を、理論として定式化できない だろうか？

着想 実装をいくつかの部分に分離して行う CPU の命令セットの操作的意味論 基本操作の定義 型検証エンジン 記述を簡単にするためのライブラリ的なもの 型検証エンジン レジスタの型・メモリの構造などを保持、検証を行う 中核部分 マイクロカーネルからの類推

共通項の抽出 x86 固有情報 Alpha 固有情報 SPARC 固有情報 (μOP 的なレイヤ) 抽象ハードウェア ←この記述を簡潔 　　にできるように 　　するには？ (μOP 的なレイヤ) ←この層に型を 　　導入できるか？ 抽象ハードウェア

関連研究: Foundational TAL TALx86 の妥当性はインフォーマルにしか 与えられていない 実装が正しいことをユーザは信用する必要 TCB (Trusted Computing Base) を小さく することが重要 実装を 2 つの段階に分けることを提案 まず一般的な型付きアセンブリ言語を開発し 実際のアーキテクチャからその言語へマッピング

関連研究: Foundational TAL TALT (TAL Two) 抽象機械 レジスタ N 個 (任意) 即値、レジスタ、メモリへの参照をオペランドとする RISC 系命令セット レジスタ間接やメモリ間接などのアドレッシングモードを 記述できる 算術演算と mov, cmp, 分岐命令, malloc を持つ Twelf (logical framework) で構築された LF の上に構築 Foundational PCC と同様

コンパイルの流れ (再掲) このへんをターゲットにした型検証系 高級言語 中間言語 アセンブリ 機械語 mov add jmp… 0100101 1011101 0101011 00101… このへんをターゲットにした型検証系 機械語

CPU 非依存な型システム Modular な型の処理・検証 既存のアセンブラに組み込めるとよい CPU の実体とできるだけ癒着しないように あるいは、コードジェネレータを作成する (yacc みたいに) もちろん拡張性も必要 既存のアセンブラに組み込めるとよい わざわざアセンブラから自作する必要はありや、なしや たとえば GNU as などに組み込めたら、利用しやすい？ 擬似命令はマクロなどで処理

型安全な中間言語を定義する 実機の機械語とほぼ一対一対応する言語 型の処理系は一つで済む 近いものとして、RTL (gcc の内部表現) 簡単なトランスレータで各アーキテクチャに対応 型の処理系は一つで済む 高級言語からのコンパイラが、その分必要に なるが… 近いものとして、RTL (gcc の内部表現) 現在詳細調査中

命令の分類 x86 算術命令、論理演算など 　　　固有命令 (特権命令など) ARM SPARC

命令の分類 余白はできてしまう だろう x86 x86 用定義・ライブラリ による拡張 型検証カーネル ARM SPARC 高級言語

静的型付けだけでうまくいかない部分 加減算は、数値にもアドレスにも用いることができる レジスタオフセット どちらとして用いている？ アドレス+数値、数値+数値 アドレス同士でオフセット計算もできそう 逆に、アドレス演算器で計算させるなんて芸当も lea eax, [eax+eax*4] ; eax = eax * 5 レジスタオフセット レジスタの値が静的に定まらない場合が難しい