Safety Checking of Machine Code Zhichen Xu Barton P. Miller Thomas Reps Proceedings of the ACM SIGPLAN '00 Conference on Programming language design and implementation

Motivation 機械語コード上で検証ができたらいいな プログラマに言語選択の自由が生まれる 実行ホスト側で自由な検証ができる 利用例 ブラウザのプラグイン COM コンポーネント等

Safe Properties and Policies デフォルトの検査項目 配列境界, アラインメント, 未初期化変数 Null ポインタの参照, 危険なスタック操作 ホスト固有のアクセス制限ポリシー ホスト側のデータやメソッドのアクセス制限を規定できる 本当にどこまで実現可能なのか？

Limitations いくつかの性質を確認するだけであって、その他完全性などについては何も関知していない 検証にかかるコストは極めて大きい 検証プロセスも不完全である 配列の粒度の問題から、不正確な点がある 型の sub-typing を考慮していない 命令の特殊な用例をサポートできていない XOR を用いた非数の交換など

Related works Proof Carrying Code (PCC) Typed Assembly Language (TAL) 処理系: Touchstone Certifying Compiler Typed Assembly Language (TAL) 言語: Popcorn (C-like) 処理系: TALx86

Related works : 比較 (1/2) 共通 思想的相違 コンパイラ等の最終生成物だけを見ているので、ホスト側でもっと調べようと思えば不可能でない。 思想的相違 [PCC, TAL] ソースレベルで危険な操作を禁止している ポインタ演算, ポインタのキャスト, free() 等ができない [この研究] 危険なことをしなければ言語は何でもいい

Related works : 比較 (2/2) 検証方法の相違 ポインタの追跡 型だけでなく値の状態まで考慮しており、より細かな検証ができる ポインタの追跡 ポインタのコピーを追跡することで、より細かな検証ができる

Safety-Checking Analysis 定義: typestate 型, 値の状態, アクセス制限 入力 対象となる信用ならないコード ホストの typestate 定義 実行前のホスト側データの型および状態 ホスト側メソッドのパラメータや返り値に関する constraint ホスト側データやメソッドへのアクセス制限定義 対象コードへの初期引数の typestate

Safety-Checking Analysis: 入力例 1: mov %o0, %o2 2: clr %o0 3: cmp %o0, %o1 4: bge 12 5: clr %g3 6: sll %g3, 2, %g2 7: ld [%o2+%g2], %g2 8: inc %g3 9: cmp %g3, %o1 10: bl 6 11: add %o0, %g2, %o0 12: retl 13: nop Host Typestate e: <int, initialized, ro> arr: <int [n], {e}, rfo> Safety Policy V = {e, arr} [V : int : ro] [V : int [n] : rfo] Invocation %o0 ← arr %o1 ← n [Host Typestate] arr: サイズ n の int の配列, e: 抽象位置情報 arr の全要素を含んでいる [Safety Policy] arr と e は V リージョンに存在する, V の中の int はすべて読み出し可能で operable, V の中の int n 個の配列のベースポインタは読み出し可能 operable で followable [Invocation] arr と arr のサイズが %o0, %o1 を通じて渡される

Safety-Checking Analysis: Overview Phase 1: Preparation Phase 2: Typestate propagation Phase 3: Annotation Phase 4: Local verification Phase 5: Global verification

Safety-Checking Analysis: Phase1. Preparation Host Typestate, Safety Policy, Invocation から 初期 annotation を導く 初期 typestate 初期制約 左２行目：arr が %o0 で渡されている 右：サイズ n が %o1 で渡されている %o0, %o1 に r,w パーミッションが出ている。レジスタだからね。 でも配列 arr に書くことはできない。範囲 e に w がでてないからね。 Initial Annotation Initial Typestate e:<int, initialized, ro> %o0:<int [n], {e}, rwfo> %o1:<int, initialized, rwo> Initial Constraints n ≧ 1 かつ n = %o1

Safety-Checking Analysis: Phase2. Typestate propagation コード, 初期 annotation を受け取り、各命令の操作的意味を使って、各命令ポイントにおける typestate の変遷を追いかける 例の７行目で %o2 が配列のベースポインタになっていることなどを突き止める

Safety-Checking Analysis: Phase3. Annotation Phase 2 で得られた typestate とコードから Assertion Typestate からわかること Local Safety Precondition Typestate のみで検査可能な条件 Global Safety Precondition その他の手段を用いて検査すべき条件 からなる annotation を各命令ポイントで洗い出す

Safety-Checking Analysis: Phase3. Annotation Assertion %o2 は int 配列のアドレス, %o2 mod 4 = 0, %o2 ≠ NULL Local Safety Precondition e は読み出し可能, %g2 は書き込み可能, %o2 は参照可能 Global Safety Precondition 配列境界検査: %g2≧0 && %g2<4n && %g2mod4=0 NULL＆アラインメントチェック: %o2!=NULL && (%o2+%g2)mod4=0

Safety-Checking Analysis: Phase4. Local verification Phase 4 で得られた Local Safety Precondition を満たすかどうか検査する Typestate だけ見ればわかる条件なので自明

Safety-Checking Analysis: Phase5. Global verification プログラム検証の技術を使って Global Safety Precondition を満たすかどうか検査する ループが存在する時は induction-iteration 法を用いてループ不変量を特定したりする 例 (7行目) %g2 が配列境界を越えないのを示す過程で “n > %g3 かつ n ≧%o1” というループ不変量を特定したりする

実験: SPARC 向け実装 いくつかのサンプルプログラムでプロパティを満たさないものを検出させることに成功 制限: local 配列の境界検査ができない コンパイラの最適化との相性 よし: ループ不変量のコード移動, レジスタ割り当て あし: Strength Reduction, アドレス計算 Strength Reduction: ループの中でループ変数と定数の掛け算になっているものを扱っている時、それを加減算に置き換える Loop-invariant Code-Motion: ループが短くなるので induction-iteration がより効率的になる レジスタ割り当て: レジスタの中だけのやりくりでは正確に typestate が保存されるから あし: induction-iteration 法で使用する関係を隠してしまうから 関数のインライン展開も関数を長くしてしまって困る。関数の抽象化の恩恵。

Global Safety Conditions 実験: サンプルプログラム Sum Hash Btree Stack Smashing MD5 命令 13 25 41 309 883 分岐 2 4 11 89 ループ 1 7 5 呼び出し 6 Global Safety Conditions 14 162 135

実験: 検証時間計測 (Sun Ultra 10) 実装の制限：local の配列の bounds チェックができない