M2 吉野 寿宏 <tossy-2@yl.is.s.u-tokyo.ac.jp> 全体ミーティング 12/13 修士研究進捗報告 M2　吉野 寿宏 <tossy-2@yl.is.s.u-tokyo.ac.jp>

Presentation on theme: "M2 吉野 寿宏 <tossy-2@yl.is.s.u-tokyo.ac.jp> 全体ミーティング 12/13 修士研究進捗報告 M2　吉野 寿宏 <tossy-2@yl.is.s.u-tokyo.ac.jp>"— Presentation transcript:

1 M2 吉野 寿宏 <tossy-2@yl.is.s.u-tokyo.ac.jp>
全体ミーティング 12/13 修士研究進捗報告 M2　吉野 寿宏

2 Agenda 研究内容 方針 概略 進捗報告 今後の予定

3 研究内容 「型付きアセンブリ言語の、複数アーキテクチャに 向けた実装」というタイトル In other words…
「型付きアセンブリ言語の、複数アーキテクチャに 　向けた実装」というタイトル In other words… アセンブリ言語のコード検証器を構築するための フレームワークを作成 特にプログラム変換の部分を扱う

4 背景 ネットワーク越しのコード配布の隆盛 どうしたらコードを信用できる/信用してもらえる？
ユーザーアプリケーション、OS のパッチ、ドライバ… 同時にセキュリティの脅威にもなっている トロイの木馬、アプリケーションの脆弱性への攻撃 スパイウェア どうしたらコードを信用できる/信用してもらえる？ 信用できないものは実行しなければよいのだが、不便 かといって、全てのソフトウェアを自作することは、 現実的でない まず背景説明

5 型付きアセンブリ言語 (TAL)[1] 実マシンのアセンブリ言語に型システムを導入 レジスタの型・メモリの中身の型などを静的に検証
メモリ安全性(範囲外のメモリをアクセスしないこと)などを保証 Code signing などよりも、中身に突っ込んだ検証を行う Java VM のバイトコード検証機構と類似 実マシンのアセンブリ言語(バイナリコードでもよい)を直接検証 できるため、OS パッチなどにも使用可 TALのプロジェクトはCornell Univ.でスタート。G. MorrisettもCornellの研究者(現在はHarvardにいるみたい。) この論文は、単純なRISC計算機上のアセンブリ言語に対して、System Fから型を維持したままコンパイルできるということを示している。 [1] G. Morrisett, et al. From System F to Typed Assembly Language. In 1998 ACM SIGPLAN-SIGACT Symposium on Principles of Programming Language.

6 TAL の問題点 アーキテクチャ(CPU)ごとに処理系を用意する必要 既存の処理系を他のアーキテクチャに移植するのが困難
命令の意味論はアーキテクチャごとに異なる 既存の処理系を他のアーキテクチャに移植するのが困難 既存の処理系は、CPU に特化した方向にしか進んでいない 命令セットのフルサポートを念頭においており、移植性に ついては二の次であることが多い そもそも書くべき量が多い モデル化が正しいかどうか？ しかしながら、TALにはこのような問題点が… 実際TALx86は総実装70,000行くらいある。 命令をvariantで全列挙していたり、アドレシングモードのスケーリングなどに対応するためにいろいろごちゃごちゃやっているので、どこを書き換えたものかかなり読み込まないと無理だと思う。

7 解決策 共通言語を一つ固定し、その上に検証器を構築 実際の(アセンブリ)言語からその言語に対して意味論のマッピングを構成
言語の semantics を固定 実際の(アセンブリ)言語からその言語に対して意味論のマッピングを構成 変換が「正しければ」(後ほど解説)、変換元のプログラムを検証しているのと等価 検証器の構成とは独立性が確保できるとよい 新しいアーキテクチャに対応する際に検証器を弄らない 検証器を取り替えるときにマッピングルールを弄らない

8 型によるコード検証 (Normal) Compilation
x86 x86 用 バイナリ 型 PPC 用 バイナリ 高級言語・ 中間言語 PPC 通常、型情報は失われる

9 型によるコード検証 Type-Preserving Compilation
x86 用 検証器 x86 x86 用 バイナリ 型 型 PPC 用 検証器 PPC 用 バイナリ 高級言語・ 中間言語 PPC

10 型によるコード検証 本研究のアプローチ 型 型 検証器 アリマス 型 コンパイル 逆コンパイル x86 高級言語 共通言語 PPC x86

11 研究方針 3 つのステップ 本研究は特に、このうち 1. と 2. に着目 共通言語を設計 実際のアーキテクチャから共通言語への変換器を作成
共通言語の semantics を用いて検証器を作成 本研究は特に、このうち 1. と 2. に着目 これまで 3. は数多く研究されてきているので、それらの成果を応用することができると考えられる しかし 2. についての記述性等を考慮している研究は(知る限り)ない 「変換の正しさ」の議論を含める

12 本研究の特徴 アセンブリ言語(≒機械語)のプログラムを検証 検証器を載せ替え可能にする 検証の理論は、多くがλ計算などの言語上に構築
その後機械語にコンパイルして実行 ⇒　コンパイラの正しさはどう保証するの？ 本研究は逆のアプローチ CPU エミュレータを記述する また、そのための記述性を考慮する 検証器を載せ替え可能にする プログラム検証に関する研究は数多い 様々な目的のための検証系が提案されている メモリ安全性、インターフェイスの整合性 (つまりは安全性) 情報流解析　　…

13 共通言語の設計 プログラムの変換対象となる言語 記述性の確保 変換元はアセンブリを念頭に置くので、アセンブリ言語の特徴を生かす
値は整数かポインタのみ (場合によっては整数だけでも可) 意味論は確定しておく 検証器を作成しやすいように インタプリタも作っておく (後で、変換の正しさの議論に用いる) 記述性の確保 書けるプログラムはなるべく広くとる ただし、行儀の悪いプログラムは必ずしも検証できずともよい

14 共通言語の設計 アイデア C などの手続き型言語ライクな構文を選択 実行フローに関わる命令は jump のみ
アセンブリ言語のプログラムは基本的に、破壊的代入により状態を書き換える 実行フローに関わる命令は jump のみ while ループ等はなくてもよい Primitive にループを行う命令はあるが、他の方法でも書ける ブロックの先頭へのみジャンプを許す 基本ブロック単位の構成を明確に意識 If-then-else による条件実行を導入 これと無条件分岐を組み合わせれば、条件分岐が書ける 複雑な条件による分岐も可能 条件代入なども記述が可能 → 検証の手間が減る(後述)

15 共通言語の設計 アイデア コードとデータを明確に分離 プログラムを構成するブロック同士は離れていると仮定 データの実行・コードの変更を禁止
コードを動的生成するプログラムは表現できなくなる 他の方法でも同じことが実現できるはず (Performance Degradation を気にしなければ) プログラムを構成するブロック同士は離れていると仮定 通常ならば、範囲を超えてアクセスすると隣にはみ出す しかしバッファオーバーフローなどで悪用されやすい はみ出「せ」ないような semantics 設計 コードブロックに関しては、末尾に暗黙の jump を入れることで fall-through を表現 コード・データとも範囲を超えたアクセスはエラーになる

16 共通言語の設計 機械の抽象モデル 取り扱う値 整数 ポインタ Junk 浮動小数点数も IEEE-754 などを用いてエンコードできる
検証をしやすくするため、内部的には fat pointer で扱う Junk 静的に定まらない値 例: ラベルに対する実際のポインタ値 ポインタも実際は、ラベル→整数 のマッピングが定められて、整数と同じように扱われる ただし、このマッピングはアセンブリ言語レベルで判明する話では なく、むしろリンカやローダなどが決定する

17 共通言語の設計 機械の抽象モデル 記憶領域 レジスタとメモリ 一時変数 エンコード、デコードのルールはアーキテクチャごとに 異なる
データをバイト列にエンコードして格納する 一時変数 こちらはエンコードをする必要は特にない エンコード、デコードのルールはアーキテクチャごとに 異なる Endianness など インターフェイス: Atom[] encode (Value value, int length); Value decode (Atom[] data);

18 共通言語の設計 レジスタとメモリ レジスタ メモリ データを入れる箱 名前で識別され、それぞれ固定長のデータを含む
ラベルで識別され、任意長のデータまたはコードを格納 コードは命令の列である データとコードは分離されている ⇒　命令をエンコード・デコードする必要はない 通常は、バイト列を命令として解釈する関数を定義したりするので、アーキテクチャ記述の煩雑化を招くおそれがある 本研究ではそこが必要なくなるので、シンプルになる

19 共通言語の設計 レジスタとメモリ レジスタ R、メモリ M それぞれバイト列(d)にエンコードされて格納
c* は命令(次で定義)列 それぞれバイト列(d)にエンコードされて格納 ルールはアーキテクチャ依存パラメータ m[n] は、アドレスの n バイト目をあらわす ポインタ長もアーキテクチャ依存パラメータ

20 共通言語の設計 計算言語

21 共通言語の設計 意味論 プログラムカウンタ = ラベル + 命令インデクス 詳細は省略 各命令に対して、副作用のある箇所は 1 箇所ずつ
代入または goto による無条件分岐 「1 命令実行する関数」step を考えると、インタプリタは step の不動点として定式化される step :: ExecContext → ExecContext=(Reg, Mem, PC) 詳細は省略 ほぼ、見て類推できるとおり 一部エラーになることがある 非ポインタを dereference しようとした場合 データブロックにジャンプしようとした場合　　　など

22 共通言語の設計 意味論 ポインタ演算を行うと一部 junk が出ることがある 変なデータをデコードすると junk になる
ポインタ同士の加算 ポインタ+整数は、オフセット部に整数が加算されるのみ ラベルの異なるポインタの減算 同一のラベルのポインタを減算するとオフセットの差になる それ以外の、ポインタが関与する演算は junk になる 乗除算、論理演算など 変なデータをデコードすると junk になる ポインタと整数が混じっている / ポインタの長さ不足 junk との演算は junk になる 結果を汚染する可能性がある が、「行儀のよい」プログラムなら大丈夫と考えている

23 プログラムの例 Linked List 内の値の和
struct list_t { 　 int value; struct list_t *next; } list; --- x86 Assembly start: mov ebx, list xor eax, eax loop: or ebx, ebx jz end_loop add eax, [ebx] mov ebx, [ebx+4] jmp loop end_loop: jmp end_loop start: %ebx = &list; %eax = 0; goto &loop; loop: if %ebx == &null then goto &end_loop else ε; %eax = %eax + *4(%ebx); %ebx = *4(%ebx + 4); end_loop: goto &end_loop; 勝手に次のブロックには行かない

24 プログラムの例 Junk になってしまう例 以下のような C のコード 通常のアセンブリ言語 この言語の意味論 p = &bar と同じ
char *p = &foo, *q = &bar; p += q - p; ... あまり行儀がよろしくない プログラム 通常のアセンブリ言語 p = &bar と同じ この言語の意味論 &bar - &foo ⇒ junk したがって、実行後にはp は junk になる メモリアクセス発生時にエラー

25 検証器 変換後の共通言語によるプログラムを検証 このシステムでは、検証器内部はブラックボックス化されている
「プログラムを受け取り検証結果を返すもの」とのみ定義 void verify(Program program) throws VerificationException; 検証が通ったらそのまま return 失敗したら VerificationException が throw される 中に原因の情報が格納されている

26 検証器 Pros and Cons of the Design
利点 システムが拡張可能になる 型理論やプログラム検証の、理論面における研究の進歩を反映できる プログラム変換と独立性を確保することにより、 検証器を取り替えたときに、変換ルールを弄らなくてよい 新しいアーキテクチャに対応するときに、変換ルールだけ書けば検証器はそのまま使える 欠点 このシステム単体では何も保証できない 検証の正しさを保証するのは検証器の製作者の責任

27 検証器 共通パターンの抽出 検証ロジックに共通のパターンが見出せそう 性質 性質 命令 状態 命令 状態 状態 状態 状態 状態
仮定している言語は手続き型言語 命令実行の傍系として、抽象化された状態による仮想 実行を行ってゆくパターンが多いのでは (と想像) 性質 性質 命令 状態 命令 状態 状態 状態 状態 状態 ： ：

28 検証器 共通パターンの抽出 とりあえずシンプルな検証器を設計してみた ある性質を持った値の集合を「型」として表す
“Typed” Assembly Language なので 型レベルのインタプリタを定義 意味論の定義は計算言語のインタプリタとほぼ同様 ブロックごとに前提条件(prerequisite)を記述し、実行遷移が流入するところで条件に合致しているかを検査 前提条件を満たしていると考えてブロックを型レベルで実行 goto 文がでてきたら検査 これをブロックごとに繰り返す

29 検証器 共通パターンの抽出 共通パターンが抽出できると… 基本的なロジックを共通パターンとして分離
ブロックごとに計算するループ precondition から postcondition を計算し、goto について検証するループ … 検証器を作成する側としては、型の計算ルールを命令に対して書き下すだけでよくなる 検証器を拡張する際に、必要なメソッドをオーバーライドするだけでよくなる OOP 的な考え方 そのため、実装は Java で行っている

30 プログラム変換 実際のアーキテクチャのアセンブリ言語を、先に 設計した共通言語に変換 命令 = コードのテンプレート + オペランド*
変換ルールの記述言語という仕事も考えられる 命令 = コードのテンプレート + オペランド* mov( D , S ) { D := S ; } テンプレートを、オペランドによってインスタンス化 オペランド = 即値 | レジスタ | メモリ 即値以外は代入が可能 (出力引数)

31 プログラム変換 設計 Reader, Writer を渡すと Reader から読んで 変換 必ずしも 1 命令が 1 文に対応しない
複数ブロックに跨る場合も起こりうる Reader は(命令+テンプレート引数 | データ | ラベル)のストリームとして考えられる ただし lookahead ができる (delayed branch で利用) Writer は、イベントハンドラのようなもの ブロック区切り コード・データ

32 Delayed Branch の変換方法 Delayed Branch : 分岐命令の発行から実際の分岐成立までに他の命令を実行すること
パイプラインのクリアによるペナルティを避ける 分岐命令の直後にある固定数の命令(delayed slot)は分岐成立如何に関わらず実行される SPARC では 1 つ Delayed slot にある命令が分岐命令のオペランドを書き換えるようだと… 一度分岐先をどこか(変数はこのためにある)に保存し delayed slot を実行して 保存した分岐先にジャンプ

33 Delayed Branch の変換方法 Unconditional Branch
SPARC で次のコードを 考える コード 1 ba label1 mov 0, %l0 コード 2 ret　(* ba %i7 *) restore 　(* 複雑なので詳細略 *) コード 1 は単純に順序を入れ替えればよい %l0 = 0; goto &label1; コード 2 は保存が必要 var jmp_target = %i7; (* ここで restore の処理 　%i7 も変更を受ける*) goto jmp_target; Fresh な変数を持ってくる

34 Delayed Branch の変換方法 Conditional Branch
同じく SPARC で ... bz l_zero sub %i0, 1, %i0 (* non-zero *) Delayed slot が分岐 命令のオペランドに影響 する場合も考慮 上のコードは定数なので 影響しませんが たとえば次のように変換 ... if ZF != 0 then var target = &l_zero else var target = &_thru; %i0 = %i0 – 1; (* delayed slot *) goto target; _thru:

35 プログラム変換の正しさ プログラム = 機械の状態集合上の関数
変換の正しさ = 実機械の状態と、共通言語の抽象機械の状態 の対応が任意のプログラムに関して保存 状態 State 実機械 プログラム 変換後の プログラム 状態’ State’

36 プログラム変換の正しさ 実機械の状態 = (レジスタ, メモリ) 抽象機械の状態 = (レジスタ, メモリ, 変数)
実機械の状態 = (レジスタ, メモリ) 抽象機械の状態 = (レジスタ, メモリ, 変数) 状態集合の間に全単射が定義できる 変数は、局所的(実機械の 1 命令に対応する範囲内)にのみ用いるのであれば、レジスタ・メモリの内容に従属 これを保証する機構はないのだが、変換ルール側で fresh な 変数を毎回作り、使いまわさないようにする ラベルはリンカ・ローダによって整数にマップされるので、抽象機械側では整数のみを考える ポインタはいらない 整数の演算で junk は生まれないので、junk も考えなくてよい

37 プログラム変換の正しさ 正しさを保証するには
実機械の状態集合は有限 したがって、全数検査すれば「理論的には」検証可能 しかし「現実的ではない」かもしれない 各命令の演算にかかわるオペランドのみを考慮すればよいので、各命令について 232 とか 264 とかの検査をすることに たいていの場合、境界例となる一部について検証 すれば十分なことが多い 計算結果が大きく変わる場所 オーバーフローしたり、キャリーが出たり

38 FAQ 問: 本研究で提案されるシステムは、いったい何を 保証してくれるの？ 答: 特に何も保証はしません たとえば安全性とか？
問: 本研究で提案されるシステムは、いったい何を 保証してくれるの？ たとえば安全性とか？ 答: 特に何も保証はしません 検証器がブラックボックス化されているので、中身の性質を外から知ることはできない プログラム変換によって意味論が保存されているならば、検証器が保証する何らかの性質が元のプログラムでも 保証できる (はず)

39 FAQ 問: いくつか制限事項があるようだが、それに よって検証対象を狭めているのでは？
問: いくつか制限事項があるようだが、それに よって検証対象を狭めているのでは？ 答: たしかに狭まるが、安全性に対する要求などを 考えればある程度は仕方ないと思う どちらかといえば、健全性が確保されていれば、完全性は必ずしも必要ではないというスタンス 少なくとも最低限必要なことはそろっているはず つまり他にも同じことをやる道があるはず

40 進捗状況 共通言語の設計、インタプリタの実装 プログラム変換器・検証器のインターフェイスを設計 簡単な検証器の設計 プログラム変換器を作成中
いずれも Java にて 簡単な検証器の設計 実装中 プログラム変換器を作成中 とりあえず手元にある x86, SPARC あたり優先で

41 今後の予定 モノ作り 論文書き 実装を完成させる QEmu を参考に、ARM, PPC なども記述してみる 変換の正しさに関する議論
x86 くらいは検証してみたい QEmu の CPU エミュレータ部分などを流用して検証用フレームワークを作る??? (おそらくはfuture work) 論文書き