Development of Certified Program Translators to

Development of
Certified Program Translators to
Verify Low-Level Language
Programs
Toshihiro YOSHINO
(Yonezawa Lab, Univ. of Tokyo)
<[email protected]>
研究の動機

プログラム検証のための理論はあっても、実際に
検証器を作るのには手間がかかる
• 往々にしてad-hocに実装してしまうこともあり、コードの
再利用を妨げる

特に低級言語を相手にしようとする場合には顕著
• アーキテクチャ依存性が高く、システムの移植性が低下
⇒ 検証器を作るたびにモデル化の必要
• もともとの言語の意味論が(λ計算やMLなどの高級言語
に比べ)複雑
PPL2007 Poster
2
共通言語を使って解決

方針: 検証対象のプログラムを共通言語に変換
→ 変換されたプログラムに対して検査

利点
• システムの移植性が向上する
• 共通言語の意味論に対してのみ検証ロジックを設計すればよい
• 変換部分を取り替えることで複数の入力言語に対応可能

欠点
• 検証のためのロジックに加え、変換器の正しさを保証して
やる必要がある
PPL2007 Poster
3
共通言語を使って解決
変換器
共通言語に
変換された
プログラム
低級言語の
プログラム
検証結果
Success
/Fail
検証
ロジック
共通言語の意味論
PPL2007 Poster
検証器
4
変換器の「正しさ」とは

プログラム変換の前後での意味論に対応が
つかなくては、検証結果が信頼できない
⇒ 正しさの定義、またそれをどうやって保証
するか、がこの研究における一番の課題
• 対応がつけられれば、progress-preservationの
形をした検証ロジックは正しく動くことを(informal
に)証明 [Yoshino 2006]
PPL2007 Poster
5
変換器の「正しさ」とは

プログラム = 機械の状態集合上の関数
• 主なターゲットは低級言語なので手続き型として仮定

変換の正しさ =
入力・出力のプログラムに対して、変換前後2 つの言語
の間に、状態の「対応」が整合的に構成できる
状態
State State
変換元の
プログラム
変換後の
プログラム
状態’
PPL2007 Poster
State’ State’
6
Formal Definition
PPL2007 Poster
7
共通言語の設計

特定のアーキテクチャに依存しない
• 種々の低級言語を記述するための言語なので
• データの幅が 32bit とか 64bit であるとかいう制限は
できるだけ排除

低級言語に近いレベルの記述
• λ計算のように抽象度の高い記述は変換が手間
• レジスタ・メモリに対する操作を明示的に記述できる程度
を狙う

なるべくシンプルな言語構造
• 基本となる命令数が多いと意味論が複雑化
PPL2007 Poster
8
共通言語の設計

レジスタ・メモリなどを扱う手続き型言語
• 5 種類のコマンドの組合せで記述
• nop, error, 代入, goto, if-then-else
• アセンブリ言語よりも、C などに近い記法
• 中置演算子、カッコ付きの式
• if 文による自由な条件分岐
• 実行遷移をいじる命令は goto, if-then-else のみ

意味論は conservative に定義
• 実機との対応が自然につくように注意、だめならエラーに
• 「行儀の悪い」プログラムは記述できずともよい
• ポインタは加減算ができれば、配列や構造体を扱うには十分
PPL2007 Poster
9
共通言語: 構文定義
PPL2007 Poster
10
プログラム変換: 直観的には
data: ...
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;
命令単位
で変換
main:
movl
movl
x86
$data, %ebx
$0, %eax
lp:
addl
movl
cmpl
je
jmp
0(%ebx), %eax
4(%ebx), %ebx
$0, %ebx
end
lp
jmp
end
end:
PPL2007 Poster
11
プログラム変換のアルゴリズム

低級言語の命令はコンテクストを持たない
• レジスタの値、メモリの値以外によって挙動が
変わることはない
⇒ 命令ごとに対応するコマンド列へ変換して
やればよい
• 命令種別ごとに変換ルールを記述
• 変換の正しさについても、命令ごと(ルールごと)
に調べてやればよい
PPL2007 Poster
12
アーキテクチャ記述例 (IA-32、抜粋)
#operand {
eax = %eax;
ax = %eax[0,2];
al = %eax[0,1];
ah = %eax[1,1];
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 = 0
else
%_zf = junk;
...
ebx = %ebx;
...
}
mov(D, S) {
D = S;
}
...
}
PPL2007 Poster
13
実際のアーキテクチャとの対応付け

Conservative Simulation を満たす状態の対
応関係を(機械的に)構築できればよい
• 全数検査は現実的ではない
• ある程度の抽象化が必要
• 整数と整数のみならず、ポインタと整数値の対応
関係などを考える必要
• メモリブロックの検証のためにポインタをfat pointerに
しているが、実機上では整数と区別されていない
• ポインタとの対応関係の検証は毎回使いまわされると
予想
PPL2007 Poster
14
二段階アプローチ

値の種類を整数のみに制限した中間言語を用意
• 共通言語からは(一部捨てるだけで)簡単に変換可能
1.
2.
変換元言語と中間言語のsimulationを証明
中間言語と共通言語のsimulationを証明
共通言語
低級言語
(変換元)
中間言語
PPL2007 Poster
15
中間言語⇔共通言語

演算は下記のように定義されており、対応
関係を保存することは簡単に証明できる
加減算以外の演算子について:

基本的には conditional by kind のみが問題
• ポインタの比較を conservative にやるため
PPL2007 Poster
16
中間言語⇔共通言語 (続き)

アイデア: Symbolic Execution を行う
• ポインタあり側で junk になる場合はさておき、
そうならない場合に対応がつくことを証明
• Simplify (自動定理証明器)などをバックエンドと
して用いればできるのではと考えている

共通言語から中間言語への変換は、基本的に
conditional by kind を消して値を対応づけるだけで
よい
PPL2007 Poster
17
実機⇔中間言語

実機の意味論をなんらかの方法で記述し、
等価性を証明する
⇒ Coq などの証明支援系を使えないか？
• 現在はこちらをメインで着手している
• 中間言語の意味論を Coq のモジュールシステム
を用いて実装してみた
PPL2007 Poster
18
今回のデモ

中間言語との間の対応関係の証明
• 中間言語の意味論をライブラリとして用意
• Coqのモジュール機構を用いて実装してみた
• 簡単な仮想アーキテクチャを定義し、中間言語に変換後
の意味論との対応づけを証明
• 基礎の数論のところにいくつかAxiomが残っているが、上層は
とりあえず証明できた

変換アルゴリズムと、検証器フレームワークの実装
• L3Cover Framework:
http://www.yl.is.s.u-tokyo.ac.jp/~tossy-2/l3cover/
PPL2007 Poster
19
Future Work

数論の定理を充実させる必要
• 特にmod 2nの系での演算に関して

実際の命令には単純なコマンド列にならない
ものもある
• call命令は戻り先として次命令のアドレスを要求
• Delayed branchは変換途中で後続命令の変換
が必要
⇒ 他言語の助けを借りる等すれば実装できるが…
PPL2007 Poster
20

Download Report