スライド 1

型付きアセンブリ言語の一般化
吉野 寿宏 (東京大学 米澤研究室)
<[email protected]>
背景

Mobile Code の隆盛
便利なことは多い
 スパイウェアやトロイの木馬などの脅威も


信用のおけないコードの取り扱い
実行しなければいい
→ すべて自分で手作りするわけにも…
 どうやったら配布されているコードを信用
できる/してもらえるか?

関連技術:
電子署名
コードの出自を保証
 悪意のあるコードを
含まないことは保証
できない



コードの正統性・
同一性を保証する
中身を保証する技術
ではない
ハッシュ値 h
公開鍵
暗号化
{h}Kpri
コード
{h}Kpri
D(Kpub, {h})
H(M)
ハッシュ値 h
ハッシュ値 h’
h=
h’ ?
関連技術:
[1]
Proof-Carrying Code

コードが安全である数学
的証明を添付



受け取った側は、ツー
ルで安全性を検証
検証に通ったコードは
信用できる
安全
証明
コード
このコード
は安全です
数学的理論に基づいた
中身の検証が可能
[1] G. Necula. Proof-Carrying Code. In POPL97
安全
ポリシー
関連技術:
Java VM

バイトコード検証機構
バイトコードの型検査
 コンパイル時の静的型が正しくない場合に有効

ライブラリのバージョンを途中で変えたり
 一部のファイルを再コンパイルしたり


しかし、Java であるがゆえに

デバイスドライバ等、システムの基幹部分に
応用が難しい
型付きアセンブリ言語(TAL)

アセンブリ言語に型を導入


[2]
レジスタの型・メモリの中身の型を静的に
検証
Java のバイトコード検証のアプローチを
実 CPU 向けのアセンブリ言語に適用

システムソフトウェアなどにも応用がきく
[2] G. Morrisett, et al. TALx86: A Realistic Typed Assembly Language. 1999
ACM SIGPLAN Workshop on Compiler Support for System Software
TAL による検証の流れ

アセンブリコードに
annotation を挿入



レジスタの型
スタックの型
各 annotation について
型を検証してゆく
mov eax,ecx
inc eax
mov ebx,0
jmp test
body: {eax: B4,
add ebx,eax
test: {eax: B4,
dec eax
cmp eax,0
jg body
; i = n
; ++i
; s = 0
ebx: B4}
; s += i
ebx: B4}
; --i;
; i > 0
EAX は 4-byte integer を持つ
EBX は 4-byte integer を持つ
応用例:
デバイスドライバ

デバイスドライバの安全性
WindowsXP: 署名がない場合に警告を表示
 オオカミ少年的状況


署名されていないドライバが数多い



私が知る限り、ちゃんと署名されていたドライバってあまり
見た記憶がない…
署名されていないからといって、ハードウェア用
ドライバのインストールを中断するか?
安全性を数学的に検証することによって、
動機付けを強くする
応用例:
BREW

携帯分野への応用


個人情報を取り扱う端末 = 頑健でなくてはならない
BREW アプリの登場



低レベルなコード(C++ などで記述)を実行させる技術
現在では認証を通った公式コンテンツプロバイダのみが
使用可能
TAL 検証系を利用すれば、サードパーティーの
コード安全性を検証可


認証を受けなくても BREW 使用可能に
開発者側の幅が広がるのでは
しかし…

現存する実装は一部 CPU に限られる
本家では x86 専用のツールを配布
→ http://www.cs.cornell.edu/talc/
 ほかにもアーキテクチャはたくさんある



PowerPC, Alpha, ARM, …
その他のアーキテクチャの取り扱いは?

システムを毎回独立に作成する必要


コスト高すぎませんか
書式が一定でないかもしれない
統一的な実装に向けて

CPU のできることは皆だいたい同じ

計算機の構成
レジスタがあって、
 メモリ(スタック、ヒープ、グローバル変数)があって


算術演算、メモリ操作、関数呼び出しなどの
命令
→ 共通化した型理論が構築できないか?
目指すべきもの

CPU 非依存な、アセンブリ言語レベルでの
型検査システム
IA-32
Alpha
SPARC
ARM
IA-32 定義
Alpha 定義
SPARC 定義
ARM 定義
共通型検査エンジン
複数のアーキテクチャを
統一的に扱えるようなシステム
CPU 非依存な型システム

Modular な型の処理・検証

CPU の実体とできるだけ癒着しないように
CPU 依存の部分を分離して記述するように
 あるいは、CPU 定義を読んで型処理コードを出力
するようなコードジェネレータを作成する


既存のアセンブラに組み込めることを想定

たとえば GNU as などに組み込めたら、利用
しやすいのでは
目指すべきもの
または、
 実 CPU の機械語にほぼ straightforward な変換
ができる型安全な中間言語
C/C++
コンパイラ
Objective
Caml
…
中間言語処理系(型検証エンジン)
IA-32
Alpha
SPARC
ARM
トランスレータ トランスレータ トランスレータ トランスレータ
IA-32
Alpha
SPARC
ARM
型安全な中間言語を定義する

実機の機械語とほぼ一対一対応する言語


簡単なトランスレータで各アーキテクチャに
対応
型の処理系は一つで済む

高級言語からのコンパイラが、その分必要に
なるが…
困難な点
ポインタの操作
 CPU specific な命令の処理

たとえば、IA-32 の LGDT 命令は他の CPU
ではどうなる?
 デバイスドライバなど、ハードウェアに近い
コードを検証する場合には必要


外部ライブラリとの連携
特定のレジスタによる値渡しなどの処理
 特に、中間言語のアプローチだとどうか?
