修論進捗状況報告 型付きアセンブリ言語のマルチアーキテクチャ化実装に向けて 吉野 寿宏 <tossy-2@yl.is.s.u-tokyo.ac.jp>

本日の Agenda 修論テーマについて説明 現在までの進捗状況 今後の予定 型付きアセンブリ言語(TAL)とは 着想・要件 現在までの進捗状況 定式化について説明 今後の予定

修論テーマについて

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

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

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

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 を持つ

しかし… プロセッサはいろいろな種類がある 各 CPU ごとに処理系を作成する必要 x86, PowerPC, SPARC, ARM, SH… PC 用としては x86 (互換)が多いが、携帯 デバイスには ARM や SH が多い 各 CPU ごとに処理系を作成する必要 CPU が違えば命令セットも異なる アセンブリの書式も異なるかもしれない オペランドの順序など

マルチアーキテクチャ対応 アプリケーションのコンパイル 機種ごとの TAL 処理系 が必要！ x86 中間言語 mov add jmp… アセンブリ 高級言語 0100101 1011101 0101011 00101… 機械語 Alpha 中間言語 mov add jmp… アセンブリ 0100101 1011101 0101011 00101… 機械語 PPC 中間言語 mov add jmp… アセンブリ 0100101 1011101 0101011 00101… 機械語

いろいろなアーキテクチャ x86 ARM Power PC ワード長 (ビット) 32 32/64 命令長 (バイト) 可変 2/4 4 SPARC Power PC ワード長 (ビット) 32 32/64 命令長 (バイト) 可変 2/4 4 エンディアン リトル 両用 ビッグ オペランド 2 入出力･入力 3 その他 アドレシングモードが 複雑 条件実行・ シフトなどが 簡単 レジスタ ウィンドウの機構

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

マルチアーキテクチャ化構想 CPU のできることは皆だいたい同じ → 共通化した実装が構築できないか？ 計算機の構成とは レジスタがあって メモリ(スタック、ヒープ、グローバル変数)があって 算術演算、メモリ操作、関数呼び出し などの命令がそれらの状態を変更する → 共通化した実装が構築できないか？

マルチアーキテクチャ化構想 x86 固有情報 Alpha 固有情報 SPARC 固有情報 (μOP 的なレイヤ) 抽象ハードウェア ←この記述を簡潔 　　にできるように 　　するには？ (μOP 的なレイヤ) ←この層に型を 　　導入できるか？ 抽象ハードウェア

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

TALT (TAL Two) 抽象機械 Twelf (logical framework) の上に構築された型システム 関連研究 Foundational TAL TALT (TAL Two) 抽象機械 レジスタ N 個 (任意) 即値、レジスタ、メモリへの参照をオペランドとする RISC 系命令セット 算術演算と mov, cmp, 分岐命令, malloc Twelf (logical framework) の上に構築された型システム Foundational PCC のアプローチ わざわざ verifier を実装しなおさなくてもよいように

しかし… TALT はまだ理論段階 後段の、アーキテクチャとのマッピングについては future work が多い 関連研究 Foundational TAL しかし… TALT はまだ理論段階 抽象機械と、その上の基本的な操作に ついて述べられているのみ 後段の、アーキテクチャとのマッピングについては future work が多い たとえば分岐遅延スロットの扱いとか TALx86 同様、GC の存在に依存している ので、free() が言語上ない、とか

進捗状況について

実装方針 目指す システム 型システム x86 アーキテクチャ PowerPC アーキテクチャ アーキテクチャ記述言語 (ADL) 抽象機械

システムの全体像 内部的 表現 パターン定義 計算の抽象的記述 適用された抽象機械 プログラム (ソース/ オブジェクトファイル) 変換 プログラム (ソース/ オブジェクトファイル) 適用 計算の抽象的記述 操作 適用された抽象機械 生成 アーキテクチャ 記述

システムの全体像 抽象機械の定式化 抽象機械の動作記述言語の定式化 動作記述言語に型システムを導入 実アーキテクチャからのマッピング データ構造の定義 抽象機械の動作記述言語の定式化 命令を分割記述 変数を導入 動作記述言語に型システムを導入 実アーキテクチャからのマッピング → 実際に記述を試みる

最終的にめざすもの (こんなことができるといいな) %register<4> eax, ebx, ecx, edx %register<4> esi, edi %register<4> ebp, esp %register<4> eflags function add(x:int, y:int) = x + y function add(x:int, <l+n>:addr) = <l+(x+n)> function add(x:addr, y:addr) = add y x ... mov(D, S) : { D := S; } inc(DS) : { DS := add DS 1; } add(DS, S2) : { DS := add DS S2; } ...

抽象機械を定義する 抽象機械 = 状態を保持する部分 実アーキテクチャを包含できるような 一般性が必要 可変個のレジスタ 抽象化するアーキテクチャと対応させる コードとデータは分離されていると仮定 つまり、コードをデータとしては扱わない 仮想機械側はデータ部分のみを抽象化

データはすべてバイト単位に分割して そのタプルで記述 抽象機械を定義する データ定義 データはすべてバイト単位に分割して そのタプルで記述

メモリアドレスは 内部的に fat pointer で扱う 抽象機械を定義する データ定義 データはすべてバイト単位に分割して そのタプルで記述 メモリアドレスは 内部的に fat pointer で扱う

データはすべてバイト単位に分割して そのタプルで記述 抽象機械を定義する データ定義 データはすべてバイト単位に分割して そのタプルで記述 アドレス値の n バイト目 未定義値

抽象機械を定義する 値とエンコードされたデータ 抽象機械のデータと、それがあらわす値 (下記定義はリトルエンディアンの場合) バイト列 → 整数、アドレス列 → アドレス A はアーキテクチャのアドレス長 junk などがまじっていると ⊥ (無意味な値)

抽象機械を定義する 値とエンコードされたデータ 値と、その抽象機械上での表現 (同様にリトルエンディアン) s はエンコード後のサイズ 数学記号で表すと繁雑だが、プログラム上は シンプル、なはず…

メモリへはラベル(とオフセット)でアクセス 抽象機械を定義する 抽象機械の持つ状態 レジスタは名前で識別 レジスタ r1 の幅を w1, … とする メモリへはラベル(とオフセット)でアクセス ラベルの異なるメモリ領域同士は「独立」 境界チェックができる

抽象機械上のプログラム言語 抽象機械の状態(レジスタ・メモリ)を操作 関数定義ができ、オーバーロードがあるとよい 整数とアドレスを扱える言語 レジスタ・メモリとのアクセス時に、データの エンコード・デコードが必要 関数定義ができ、オーバーロードがあるとよい addr+int = addr, int+int = int などの規則を まとめて書きたい add は一命令でアドレス/数値計算両方可 または(ML ライクな)マッチング機構でもよい 型をまたがったマッチングになるが… とりあえずこちらで定式化を進めてみた

抽象機械上のプログラム言語 参照 計算用の世界 代入 レジスタ 整数 アドレス メモリ 抽象機械 decode encode r1 = <…>, r2 = <…>, … 参照 decode メモリ 代入 l1 = <…>, l2 = <…>, … encode 抽象機械

そもそも計算はどういう進み方をするか オペランドの値を読み出す 値をごちゃごちゃ計算する 結果をどこかに代入する 抽象機械上のプログラム言語 言語の設計 そもそも計算はどういう進み方をするか オペランドの値を読み出す レジスタ、メモリ 値をごちゃごちゃ計算する 四則演算、ビット演算 関数型言語で(きれいに)記述できる範囲 結果をどこかに代入する ここもレジスタ、メモリ 破壊的代入、しかも型を上書きできる ref では扱いきれない

値をもらって計算する部分と、値の読み込み・代入の部分に分離 抽象機械上のプログラム言語 言語の設計 値をもらって計算する部分と、値の読み込み・代入の部分に分離 計算部分には副作用がないようにする 特定のレジスタやメモリに依存すること なく、単純にパラメータのみから結果を 生成するような記述 代入で型が変わりうるので、暗黙のうちに パラメータ化が必要になる

抽象機械上のプログラム言語 言語の定義: 計算記述

抽象機械上のプログラム言語 言語の定義: データ入出力 代入ベースな記述の部分 計算記述部で書いた関数を呼び出せる レジスタ・メモリへの参照が可能

抽象機械上のプログラム言語 言語定義: 操作的意味論 長いので、添付の別紙を参照 計算記述部 → 図 5, 6 型を跨ったマッチング機構がある Functor が、ここでは単純な値型のみマッチできればいい データ入出力部 → 図 7 エンコード・デコードが自動的に行われる r := r のような記述の場合は、単なるコピー でもいいかもしれない decode が ⊥ 以外になれば、encode はもとの値と同じものを返すはずである (サイズが一致していれば、の話だが)

抽象機械上のプログラム言語 Alternative Approach 整数・アドレスに変換するより、抽象機械のデータをそのまま扱うこともできる 表現のドメインとしては 整数∪アドレス ⊂ 抽象機械データ <m[0], m[1], junk, junk> みたいなデータも扱える 演算を定義すれば、抽象データのまま でも困らない プリミティブ側に押し込めるだけ どちらにも、長所があり短所があり (次で述べる)

抽象機械上のプログラム言語 Alternative Approach レジスタ プリミティブ Add (+) encode decode ユーザ 関数 r1 = <…>, r2 = <…>, … 操作 利用 メモリ Sub (-) encode decode エンコード・ デコードが分散 l1 = <…>, l2 = <…>, … … ユーザは中身を意識 する必要がない 抽象機械

Pros and Cons of These Two Approaches データのエンコード・デコード 計算するときは結局エンコード・デコードが必要 出入り口で変換してしまえば、変換はここだけ エンディアンの解釈の問題はここのフィルタを 取り替えるだけ デコードせずに計算する場合、計算ルーチンにエンコード・デコードがあちこちに分散 エンコーダ・デコーダ関数によって、プリミティブがパラメトライズされる 毎回複数用意する必要がでてくるのでは？ →記述性を下げてしまうのでは

Pros and Cons of These Two Approaches データ幅の取り扱い 一度整数(やアドレス)にしてしまうと、もともとの データ幅が曖昧になる 明示的に幅を指定するか 代入左辺の大きさに暗黙に coerce することもできるだろう 小さい幅に代入する場合はともかく 逆は符号拡張かゼロ拡張かが問題となる デコードしなければこの問題はない すべてのデータ型に幅が付随している 幅の一致しない代入はエラー、などより厳密なチェックができる

Pros and Cons of These Two Approaches リテラルの取り扱い 整数・アドレスの世界で演算するなら、 そのまま見ればよいので自明 抽象機械データの世界で演算する場合、 一度エンコードする必要がある 1 は 1 でも、<1, 0, 0, 0> か <1> なのかに よって、違うものとして扱われる つまりデータ幅の推論の問題 エンコード幅は手動指定が必要と思われる 或いは、暗黙で広いデータ型への coercion を行うことも可能 しかし符号拡張・ゼロ拡張の問題浮上

抽象機械上の型システム 計算記述言語の型 抽象機械における型 現在目下こちらの定式化中 型を跨るマッチングがあるので、functor が必要 TALT[2] を参考にできそう

抽象機械上の型システム 計算記述言語の型 型の定義 型付け規則 現在まだ途中作成中ですが… 別添用紙参照

実アーキテクチャからの マッピング 実アーキテクチャの命令を、仮想機械で同じ操作をするプログラムコードに変換 単純にやると、異なるオペランドに対して 別の記述が必要になる コードテンプレートを記述し、unification による適用 命令はオペランドでパラメトライズする OCaml の match … with や、Prolog の マッチングを想像してください

実アーキテクチャからの マッピング 命令の入力部分インターフェイス 命令を読み込んで、アーキテクチャ記述と同様のデータを出力 入力はアセンブリであったりオブジェクト ファイルであったり コードのラベル付けなどはここで管理される

実アーキテクチャからのマッピング テンプレートの記述 inc r1 : { r1 := r1 + 1; } inc r2 : { r2 := r2 + 1; } inc r3 : { r3 := r3 + 1; } ... inc REG : { REG := REG + 1; } というテンプレートで一般化される mov R1, R2 : { R1 := R2 ; } add R1, R2 : { R1 := R1 + R2 ; }

実アーキテクチャからのマッピング テンプレートの適用 実際の命令 → テンプレートパラメータ部分との対応 mov R1, R2 : { R1 := R2 ; } 要するに unification mov r2, r5 R1 = r2, R2 = r5

実アーキテクチャからのマッピング 特殊化テンプレート 一部レジスタを特殊扱いする場合がある r0 がゼロレジスタで、書き込んでも何もおきない等 レジスタとメモリで挙動を変えたい場合 mov R0, R2 : { ; } mov reg(R1), R2 : { ...; }

まとめ 抽象機械の定式化 抽象機械上のプログラム言語 (AML) 型システム 実アーキテクチャからのマッピング機構 データの抽象化レイヤ 抽象機械上のプログラム言語 (AML) 操作の抽象化レイヤ 型システム 実アーキテクチャからのマッピング機構 リーダー: アセンブリ/機械語コード → 命令 マッパー: 命令 → 抽象機械の操作(列) ADL = テンプレートコード(in AML) + マッピングルールの記述

現状と今後の予定

現状までの部分 定式化 (というか仕様策定) いろいろなアーキテクチャについて調査継続中 抽象機械の定式化 抽象機械上のプログラム言語 データの抽象化レイヤ ほぼ固まってきた 抽象機械上のプログラム言語 操作の抽象化レイヤまで もう少しきれいな書き方がないものか模索中 いろいろなアーキテクチャについて調査継続中 この仕様でほんとに書き下せるか? 等

今後の予定 定式化 (というか仕様策定) 実装、実装、実装、… 型システムの導入と検証 実アーキテクチャからのマッピング機構 リーダー: アセンブリ/機械語コード → 命令 マッパー: 命令 → 抽象機械の操作(列) 実装、実装、実装、… まだ仕様がフラフラしてますが…