TAL : Typed Assembly Language について

TAL :
Typed Assembly Language
について
前田俊行
TALとは何か?
• Typed Assembly Language
• 型づけされたアセンブリ言語
– ベースとして、一般的な普通のアセンブリ言語
を想定している
– 既存の様々なCPU上で実現可能と思われる
• (例)TALx86 : TALをx86上で実現したもの
TALで何ができるか?
• 型チェックにより次の2つのことを防ぐこと
ができる
– 不正なメモリアクセスが行われること
– 不正なジャンプが行われること
TALの流れ
•
TALのアセンブラがソースファイルからオ
ブジェクトファイルを生成する
1. まずTALのソースを型チェックする
2. 型チェックをパスしたら、オブジェクトファイル
を生成する
•
生成されたオブジェクトファイルには型情報は一
切含まれない
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
コードでないアドレスに
ジャンプしている!!!
正しくないTALコードの例(6/6)
• 不正なジャンプ
l1:
∀[].{ r1 : int, r2 : < int >, r3 : ∀[].{ } }
mov r3, r1;
jmp l1
レジスタr3が飛ぼうとし
ているアドレスの条件を
満たしていない!!!
TALのプログラムモデル
• TALのプログラムは次の3つの要素からな
る
– レジスタファイル R
– ヒープ H
– 命令列 I
プログラムの要素(1/3)
レジスタファイル
• 各レジスタにはワード値を保存できる
– ワード値とは基本的には次の2種類である
• ラベル(ヒープの要素へのポインタ)
• 整数
レジスタファイルR ::= { r1
w1, …, rn
wn }
ワード値 w ::= l
(ラベル)
i
(整数)
?t | w[t] | pack [t, w] as t’ (その他)
プログラムの要素(2/3)
ヒープ(1/2)
• ヒープにはヒープ値を保存できる
– ヒープ値とは次の2種類である
• ワード値のタプル
• 命令列
ヒープ H ::= { l1
h1, …, ln
ヒープ値 h ::= < w1, …, wn >
code[α1, …, αn]Γ.I
hn }
(タプル)
(命令列)
プログラムの要素(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命令
• Existential Type をunpackする
– halt命令
• ある型の値を受けとってプログラムを終了する
TALの型(1/2)
値の型
• 型 t ::=
–α
: 型変数
– 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
< t1^φ1, …, ti^1, …, tn^φn > ≦
< t1^φ1, …, ti^0, …, tn^φn >
TALのsubtyping(2/2)
• レジスタファイル型のsubtyping
– 使わないレジスタの型を省略してもよい
Δ
Δ
ti (for 1 ≦ i ≦ m)
{ r1 : t1, ………….., rm : tm } ≦
{ r1 : t1, …, rn : tn }
m≧n
TALのstatic semantics(一部)
• プログラム(H, R, I)の妥当性の判定
– ヒープが妥当であるか、そして
– レジスタファイルが妥当であるか、さらに、
– 命令列が妥当であるか
H:Ψ
Ψ
R:Γ
( H, R, I )
Ψ; ; Γ
I
TALのstatic semantics(一部)
• ヒープの妥当性の判定
– ヒープの型が妥当であるか、そして
– ヒープの各要素を型づけできるか
Ψ
{ l1
Ψ
h1, …, ln
hi : ti hval
hn } : Ψ
Ψ(li) = ti
TALのstatic semantics(一部)
• レジスタファイルの妥当性の判定
– レジスタの各要素が型づけできるか
wi : ti wval (for 1 ≦ i ≦ m)
Ψ;
Ψ
{ r1
w1, …, rm
wm }
: { r1 : t1, …, rn : tn }
m≧n
TALのstatic semantics(一部)
• 命令列の妥当性の判定(一部)
– jmp命令
• vが命令列のラベルであるか
• レジスタファイルの型が、その命令列へジャンプで
きる条件を満たしているか
Ψ; Δ; Γ
v : ∀[].Γ’
Ψ; Δ; Γ
Δ
jmp v
Γ <= Γ’
TALのstatic semantics(一部)
• 命令列の妥当性の判定(一部)
– add命令
• rsとvが整数(int)であるか
• 残りの命令列が妥当であるか
Ψ; Δ; Γ
rs : int
Ψ; Δ; Γ
Ψ; Δ; Γ{ rd : int }
Ψ; Δ; Γ
v : int
I
add rd, rs, v ; I
TALのstatic semantics(一部)
• 命令列の妥当性の判定(一部)
– ld命令
• rsはiより大きいサイズのタプルであるか
• 読もうとしている領域は初期化済みか
Ψ; Δ; Γ
rs : < t0^φ0, …, tn-1^φn-1 >
Ψ; Δ; Γ{ rd : ti }
I
φi = 1, 0 ≦ i ＜ n
Ψ; Δ; Γ
ld rd, rs[i] ; I
TALのstatic semantics(一部)
• 命令列の妥当性の判定(一部)
– st命令
• rdはiより大きいサイズのタプルであるか
• rsは書きこもうとしている領域の型と同じ型か
Ψ; Δ; Γ
rd : < t0^φ0, …, tn-1^φn-1 >
Ψ; Δ; Γ
rs : ti
Ψ; Δ; Γ{ rd : < …, ti^1, … > }
I
Ψ; Δ; Γ
st rd[i], rs ; I
0≦i＜n
TALの型チェックの例……
の前に
• 以降の例では以下の仮定をおく
– ヒープHは空とする
– レジスタファイルRは以下の型Γを持つと分
かっているとする
– Γ = { r1 : int, r2 : < int^0 >, r3 : ∀[].{ } }
• 以上の仮定にもとづき、命令列の妥当性
のチェックのみを示す
正しいプログラムの型チェック
型チェックOK
!
Γ = { r1 : int, r2 : < int^0 >, r3 : ∀[].{ } }
Γ{ r2 : < int^1 > } ≦ { }
Γ
r3 : ∀[].{ }
Γ{ r2 : < int^1 > }
Γ
jmp r3
r2 : < int^0 > Γ
r1 : int
Γ
st r2[0], r1 ; jmp r3
正しくないプログラムの
型チェック
Γ = { r1 : int, r2 : < int^0 >, r3 : ∀[].{ } }
型チェックエラー
Γ
Γ
r2 : < int^0 >
ld r4, r2[0] ; jmp r3
ld命令のstatic
semanticsのうち
φi = 1
を満たさない
TALプロジェクトの現状(1/2)
• 拡張 : より現実に近づけるために
– スタックを扱えるようにしている
– 配列を扱えるようにしている
– など
• 実装 : 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. SpringerVerlag, 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 2535, May 1999.

Download Report