Development of Certified Program Translators to Verify Low-Level Language Programs Toshihiro YOSHINO (Yonezawa Lab, Univ. of Tokyo) <tossy-2@yl.is.s.u-tokyo.ac.jp>

Presentation on theme: "Development of Certified Program Translators to Verify Low-Level Language Programs Toshihiro YOSHINO (Yonezawa Lab, Univ. of Tokyo) <tossy-2@yl.is.s.u-tokyo.ac.jp>"— Presentation transcript:

1 Development of Certified Program Translators to Verify Low-Level Language Programs
Toshihiro YOSHINO (Yonezawa Lab, Univ. of Tokyo)

2 研究の動機 プログラム検証のための理論はあっても、実際に 検証器を作るのには手間がかかる 特に低級言語を相手にしようとする場合には顕著
往々にしてad-hocに実装してしまうこともあり、コードの 再利用を妨げる 特に低級言語を相手にしようとする場合には顕著 アーキテクチャ依存性が高く、システムの移植性が低下 ⇒ 検証器を作るたびにモデル化の必要 もともとの言語の意味論が(λ計算やMLなどの高級言語に比べ)複雑 PPL2007 Poster

3 共通言語を使って解決 方針: 検証対象のプログラムを共通言語に変換 → 変換されたプログラムに対して検査 利点 欠点
方針: 検証対象のプログラムを共通言語に変換 → 変換されたプログラムに対して検査 利点 システムの移植性が向上する 共通言語の意味論に対してのみ検証ロジックを設計すればよい 変換部分を取り替えることで複数の入力言語に対応可能 欠点 検証のためのロジックに加え、変換器の正しさを保証してやる必要がある PPL2007 Poster

4 共通言語を使って解決 検証器 変換器 検証結果 検証 ロジック 共通言語の意味論 共通言語に 変換された プログラム 低級言語の プログラム
Success /Fail 検証 ロジック 共通言語の意味論 PPL2007 Poster

5 変換器の「正しさ」とは プログラム変換の前後での意味論に対応がつかなくては、検証結果が信頼できない
⇒ 正しさの定義、またそれをどうやって保証 するか、がこの研究における一番の課題 対応がつけられれば、progress-preservationの形をした検証ロジックは正しく動くことを(informalに)証明 [Yoshino 2006] PPL2007 Poster

6 変換器の「正しさ」とは 変換元の プログラム 変換後の プログラム プログラム = 機械の状態集合上の関数
主なターゲットは低級言語なので手続き型として仮定 変換の正しさ = 入力・出力のプログラムに対して、変換前後2 つの言語 の間に、状態の「対応」が整合的に構成できる 状態 State State 変換元の プログラム 変換後の プログラム 状態’ State’ State’ PPL2007 Poster

7 Formal Definition PPL2007 Poster

8 共通言語の設計 特定のアーキテクチャに依存しない 低級言語に近いレベルの記述 なるべくシンプルな言語構造
種々の低級言語を記述するための言語なので データの幅が 32bit とか 64bit であるとかいう制限は できるだけ排除 低級言語に近いレベルの記述 λ計算のように抽象度の高い記述は変換が手間 レジスタ・メモリに対する操作を明示的に記述できる程度を狙う なるべくシンプルな言語構造 基本となる命令数が多いと意味論が複雑化 PPL2007 Poster

9 共通言語の設計 レジスタ・メモリなどを扱う手続き型言語 意味論は conservative に定義 5 種類のコマンドの組合せで記述
nop, error, 代入, goto, if-then-else アセンブリ言語よりも、C などに近い記法 中置演算子、カッコ付きの式 if 文による自由な条件分岐 実行遷移をいじる命令は goto, if-then-else のみ 意味論は conservative に定義 実機との対応が自然につくように注意、だめならエラーに 「行儀の悪い」プログラムは記述できずともよい ポインタは加減算ができれば、配列や構造体を扱うには十分 PPL2007 Poster

10 共通言語: 構文定義 PPL2007 Poster

11 プログラム変換: 直観的には 共通言語 x86 命令単位で変換 data: ... main: %ebx = &data;
%eax = 0; goto &lp; lp: %eax = %eax + *[4](%ebx); %ebx = *[4](%ebx + 4); if %ebx == &null then goto &end else goto &lp; end: goto &end; 共通言語 data: ... main: movl $data, %ebx movl $0, %eax lp: addl 0(%ebx), %eax movl 4(%ebx), %ebx cmpl $0, %ebx je end jmp lp end: jmp end x86 ・出してみたら？ 命令単位で変換 PPL2007 Poster

12 プログラム変換のアルゴリズム 低級言語の命令はコンテクストを持たない ⇒ 命令ごとに対応するコマンド列へ変換して やればよい
レジスタの値、メモリの値以外によって挙動が 変わることはない ⇒ 命令ごとに対応するコマンド列へ変換して やればよい 命令種別ごとに変換ルールを記述 変換の正しさについても、命令ごと(ルールごと)に調べてやればよい PPL2007 Poster

13 アーキテクチャ記述例 (IA-32、抜粋) #operand { eax = %eax; ax = %eax[0,2];
al = %eax[0,1]; ah = %eax[1,1]; ebx = %ebx; ... } mov(D, S) { D = S; add(D, S) { // calculate the result first D = D + S; // ZF calculation if D : int then if D == 0 then %_zf = 1 else %_zf = 0 else if (D - &null) : int then if (D - &null) == 0 then %_zf = 1 else %_zf = junk; ... } この画面で実際にマッピングを黒板で説明したほうがいいと思う PPL2007 Poster

14 実際のアーキテクチャとの対応付け Conservative Simulation を満たす状態の対応関係を(機械的に)構築できればよい
全数検査は現実的ではない ある程度の抽象化が必要 整数と整数のみならず、ポインタと整数値の対応関係などを考える必要 メモリブロックの検証のためにポインタをfat pointerにしているが、実機上では整数と区別されていない ポインタとの対応関係の検証は毎回使いまわされると予想 PPL2007 Poster

15 二段階アプローチ 値の種類を整数のみに制限した中間言語を用意 変換元言語と中間言語のsimulationを証明
共通言語からは(一部捨てるだけで)簡単に変換可能 変換元言語と中間言語のsimulationを証明 中間言語と共通言語のsimulationを証明 低級言語 　　(変換元) 共通言語 中間言語 PPL2007 Poster

16 中間言語⇔共通言語 演算は下記のように定義されており、対応 関係を保存することは簡単に証明できる
基本的には conditional by kind のみが問題 ポインタの比較を conservative にやるため 加減算以外の演算子について: PPL2007 Poster

17 中間言語⇔共通言語 (続き) アイデア: Symbolic Execution を行う
ポインタあり側で junk になる場合はさておき、 そうならない場合に対応がつくことを証明 Simplify (自動定理証明器)などをバックエンドと して用いればできるのではと考えている 共通言語から中間言語への変換は、基本的に conditional by kind を消して値を対応づけるだけでよい PPL2007 Poster

18 実機⇔中間言語 実機の意味論をなんらかの方法で記述し、 等価性を証明する ⇒ Coq などの証明支援系を使えないか？
現在はこちらをメインで着手している 中間言語の意味論を Coq のモジュールシステムを用いて実装してみた PPL2007 Poster

19 今回のデモ 中間言語との間の対応関係の証明 変換アルゴリズムと、検証器フレームワークの実装 中間言語の意味論をライブラリとして用意
Coqのモジュール機構を用いて実装してみた 簡単な仮想アーキテクチャを定義し、中間言語に変換後の意味論との対応づけを証明 基礎の数論のところにいくつかAxiomが残っているが、上層は とりあえず証明できた 変換アルゴリズムと、検証器フレームワークの実装 L3Cover Framework: PPL2007 Poster

20 Future Work 数論の定理を充実させる必要 実際の命令には単純なコマンド列にならないものもある 特にmod 2nの系での演算に関して
call命令は戻り先として次命令のアドレスを要求 Delayed branchは変換途中で後続命令の変換が必要 ⇒ 他言語の助けを借りる等すれば実装できるが… PPL2007 Poster