TAL : Typed Assembly Language について 前田俊行

TALとは何か? Typed Assembly Language 型づけされたアセンブリ言語 ベースとして、一般的な普通のアセンブリ言語を想定している 既存の様々なCPU上で実現可能と思われる (例)TALx86 : TALをx86上で実現したもの

TALで何ができるか? 型チェックにより次の2つのことを防ぐことができる 不正なメモリアクセスが行われること 不正なジャンプが行われること

TALの流れ TALのアセンブラがソースファイルからオブジェクトファイルを生成する まずTALのソースを型チェックする 型チェックをパスしたら、オブジェクトファイルを生成する 生成されたオブジェクトファイルには型情報は一切含まれない

TALのコード例…… の前に 以降の例ではレジスタに関して次の条件が満たされているとする 上の条件を以下のように書くことにする レジスタr1の中身は整数 レジスタr2の中身は1つのint要素を持つタプルのアドレス レジスタr3の中身は命令列のアドレス 上の条件を以下のように書くことにする ∀[].{ r1 : int, r2 : < int >, r3 : ∀[].{ } }

正しいTALコードの例 r1に与えられた整数を2倍し r2に与えられたアドレスに保存して r3に与えられたアドレスへジャンプする ∀[].{ r1 : int, r2 : < int >, r3 : ∀[].{ } } add r4, r1, r1; st r2[0], r4; jmp r3

正しくないTALコードの例(1/6) 不正なメモリアクセス ∀[].{ r1 : int, r2 : < int >, r3 : ∀[].{ } } ld r4, r1[0]; jmp r3 整数をポインタとして扱っている!!!

正しくないTALコードの例(2/6) 不正なメモリアクセス ∀[].{ r1 : int, r2 : < int >, r3 : ∀[].{ } } st r3[0], r2; jmp r3 コードを書き換えようとしている!!!

正しくないTALコードの例(3/6) 不正なメモリアクセス ∀[].{ r1 : int, r2 : < int >, r3 : ∀[].{ } } ld r1, r2[3] jmp r3 データ領域外から読もうとしている!!!

正しくないTALコードの例(4/6) 不正なジャンプ ∀[].{ r1 : int, r2 : < int >, r3 : ∀[].{ } } jmp r1 整数をアドレスとしてジャンプしている!!!

正しくないTALコードの例(5/6) 不正なジャンプ ∀[].{ r1 : int, r2 : < int >, r3 : ∀[].{ } } jmp r2 コードでないアドレスにジャンプしている!!!

レジスタr3が飛ぼうとしているアドレスの条件を満たしていない!!! 正しくないTALコードの例(6/6) 不正なジャンプ l1: ∀[].{ r1 : int, r2 : < int >, r3 : ∀[].{ } } mov r3, r1; jmp l1 レジスタr3が飛ぼうとしているアドレスの条件を満たしていない!!!

TALのプログラムモデル TALのプログラムは次の3つの要素からなる レジスタファイル R ヒープ H 命令列 I

プログラムの要素(1/3) レジスタファイル 各レジスタにはワード値を保存できる レジスタファイルR ::= { r1 w1, …, rn ワード値とは基本的には次の2種類である ラベル(ヒープの要素へのポインタ) 整数 レジスタファイルR ::= { r1 w1, …, rn wn } ワード値 w ::= l (ラベル) i (整数) ?t | w[t] | pack [t, w] as t’ (その他)

プログラムの要素(2/3) ヒープ(1/2) ヒープにはヒープ値を保存できる h1, …, ln hn } ヒープ H ::= { l1 ヒープ値とは次の2種類である ワード値のタプル 命令列 h1, …, ln hn } ヒープ H ::= { l1 ヒープ値 h ::= < w1, …, wn > (タプル) code[α1, …, αn]Γ.I (命令列)

プログラムの要素(2/3) ヒープ(2/2) 実行時にmalloc命令により新たに領域を確保できる 解放はGCによる

プログラムの要素(3/3) 命令列 命令列Iは次の3通りで構成される jmp v halt[t] (jmpとhalt以外の命令) ; I

命令の種類(1/2) 算術演算 ジャンプ命令 分岐命令 add rs, rd, v (vはレジスタや即値である) sub, mul (addと同様) ジャンプ命令 jmp v 分岐命令 bnz rs, v

命令の種類(2/3) メモリ(ヒープ)アクセス命令 ld rd, rs[i] st rd[i], rs

命令の種類(2/3) 特殊命令 malloc命令 unpack命令 halt命令 ヒープから新たにデータ領域を確保する Existential Type をunpackする halt命令 ある型の値を受けとってプログラムを終了する

TALの型(1/2) 値の型 型 t ::= 初期化フラグ φ ::= 0 (未初期化) 1 (初期化済み) α : 型変数 α : 型変数 int : 整数 ∀[ α1, …, αn ].Γ : 命令列 < t1^φ1, … tn^φn > : タプル ∃α.t : Existential Type 初期化フラグ φ ::= 0 (未初期化) 1 (初期化済み)

TALの型(2/2) プログラムの要素の型 ヒープの型 Ψ ::= { l1 : t1, …, ln : tn } レジスタファイルの型Ψ Γ ::= { r1 : t1, …, rn : tn } Type Context Δ ::= α1, …, αn

TALのsubtyping(1/2) タプル型のsubtyping Δ ti Δ 初期化済みの領域を未初期化とみなしてよい Δ ti Δ < t1^φ1, …, ti^1, …, tn^φn > ≦ < t1^φ1, …, ti^0, …, tn^φn >

TALのsubtyping(2/2) レジスタファイル型のsubtyping Δ ti (for 1 ≦ i ≦ m) m ≧ n Δ 使わないレジスタの型を省略してもよい Δ ti (for 1 ≦ i ≦ m) m ≧ n Δ { r1 : t1, ………….., rm : tm } ≦ { r1 : t1, …, rn : tn }

TALのstatic semantics(一部) プログラム(H, R, I)の妥当性の判定 ヒープが妥当であるか、そして レジスタファイルが妥当であるか、さらに、 命令列が妥当であるか H : Ψ ( H, R, I ) R : Γ Ψ Ψ; ; Γ I

TALのstatic semantics(一部) ヒープの妥当性の判定 ヒープの型が妥当であるか、そして ヒープの各要素を型づけできるか Ψ Ψ(li) = ti { l1 h1, …, ln hn } : hi : ti hval

TALのstatic semantics(一部) レジスタファイルの妥当性の判定 レジスタの各要素が型づけできるか Ψ { r1 w1, …, rm wm } : { r1 : t1, …, rn : tn } Ψ; wi : ti wval (for 1 ≦ i ≦ m) m ≧ n

TALのstatic semantics(一部) 命令列の妥当性の判定(一部) jmp命令 vが命令列のラベルであるか レジスタファイルの型が、その命令列へジャンプできる条件を満たしているか Ψ; Δ; Γ Δ Γ <= Γ’ v : ∀[].Γ’ jmp v

TALのstatic semantics(一部) 命令列の妥当性の判定(一部) add命令 rsとvが整数(int)であるか 残りの命令列が妥当であるか Ψ; Δ; Γ add rd, rs, v ; I rs : int v : int Ψ; Δ; Γ{ rd : int } I

TALのstatic semantics(一部) 命令列の妥当性の判定(一部) ld命令 rsはiより大きいサイズのタプルであるか 読もうとしている領域は初期化済みか Ψ; Δ; Γ ld rd, rs[i] ; I rs : < t0^φ0, …, tn-1^φn-1 > Ψ; Δ; Γ{ rd : ti } I φi = 1, 0 ≦ i ＜ n

TALのstatic semantics(一部) 命令列の妥当性の判定(一部) st命令 rdはiより大きいサイズのタプルであるか rsは書きこもうとしている領域の型と同じ型か Ψ; Δ; Γ st rd[i], rs ; I rd : < t0^φ0, …, tn-1^φn-1 > Ψ; Δ; Γ{ rd : < …, ti^1, … > } I 0 ≦ i ＜ n rs : ti

TALの型チェックの例…… の前に 以降の例では以下の仮定をおく 以上の仮定にもとづき、命令列の妥当性のチェックのみを示す ヒープHは空とする レジスタファイルRは以下の型Γを持つと分かっているとする Γ = { r1 : int, r2 : < int^0 >, r3 : ∀[].{ } } 以上の仮定にもとづき、命令列の妥当性のチェックのみを示す

正しいプログラムの型チェック 型チェックOK ! Γ = { r1 : int, r2 : < int^0 >, r3 : ∀[].{ } } Γ{ r2 : < int^1 > } ≦ { } r3 : ∀[].{ } Γ jmp r3 Γ{ r2 : < int^1 > } r2 : < int^0 > Γ r1 : int Γ st r2[0], r1 ; jmp r3 Γ

ld命令のstatic semanticsのうち 正しくないプログラムの 型チェック 型チェックエラー Γ = { r1 : int, r2 : < int^0 >, r3 : ∀[].{ } } ld命令のstatic semanticsのうち φi = 1 を満たさない r2 : < int^0 > Γ ld r4, r2[0] ; jmp r3 Γ

TALプロジェクトの現状(1/2) 拡張 : より現実に近づけるために 実装 : TALx86 スタックを扱えるようにしている 配列を扱えるようにしている など 実装 : TALx86 TALをx86上で実現したものである 型チェッカ兼アセンブラがある GCはBoehm-GCを利用している

TALプロジェクトの現状(2/2) 高級言語 : Popcorn Cの型安全な方言 PopcornコンパイラはTALのソースを生成する ちなみに、PopcornコンパイラはPopcornで書ける

TALで何ができないか? リソースを制御すること CPU時間やメモリ使用量を制限すること メモリを明示的に解放すること

TALのまとめ TALとは型づけされたアセンブリ言語である 型チェックにより、次のことを防げる ただし、次のことはできていない 不正なメモリアクセス 不正なジャンプ ただし、次のことはできていない リソース制御 明示的なメモリ解放

References(1/3) 以降の論文は以下のTALのページから入手可能ですhttp://www.cs.cornell.edu/talc/ Greg Morrisett, David Walker, Karl Crary, and Neal Glew. “From System F to Typed Assembly Language” In the 25th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, page 85-97, January 1998.

References(2/3) Greg Morrisett, Karl Crary, Neal Glew, and David Walker. “Stack-Based Typed Assembly Language” In the 1998 Workshop on Types in Compilation, March 1998. Published in LNCS, volume 1473, page 28-52. Springer-Verlag, 1998.

References(3/3) Greg Morrisett, Karl Crary, Neal Glew, Dan Grossman, Richard Samuels, Frederick Smith, David Walker, Stephanie Weirich, and Steve Zdancewic. “TALx86 : A Realistic Typed Assembly Language” In the 1999 ACM SIGPLAN Workshop on Compiler Support for System Software, pages 25-35, May 1999.