3/11

全体ミーティング (3/11)
野尻隆宏
1
紹介する論文
• Sufficient Preconditions for Modular Assertion
Checking
– Yannick Moy
– VMCAI 2008
2
扱いたい問題
• ソースコードの安全性の検証を行いたい
null ポインタの参照
配列境界外のアクセス
整数オーバーフロー
• Assertion Checking ができればよい
ptr != NULL
0 <= index < length(array)
min_integer <= i + j <= max_integer
3
Assertion Checking を行うために
• プログラムの一部分（関数など）だけをみて、
assertion が満たされることを証明したい
• しかし、どのような context で、その部分が
実行されるか分からない
• 通常は、証明するのに十分な事前条件を
ユーザが与える必要がある
• それらを自動的に計算して与えたい
4
Running Example
{requires n <= 0 || n <= s}
void foo(int s, int n) {
int i = 0;
while (1) {
if (i < n) {
assert(0 <= i && i < s);
}
i = i + 1;
}
}
5
これまでの手法 1
• Induction-Iteration
– Suzuki and Ishihara, POPL ’77
• 最弱事前条件を用いる
• ループに関する事前条件では、ループ変数を
全称量化する
• Quantifier Elimination の手続きを使って、
量化子を消す
6
Induction-Iteration:
Backwards from Assertion
void foo(int s, int n) {
int i = 0;
while (1) {
{W(0) ≡ i < n ==> (0 <= i && i < s)}
if (i < n) {
{0 <= i && i < s}
assert(0 <= i && i < s);
}
i = i + 1;
}
}
7
Induction-Iteration:
Backwards from Assertion
• W(0) が while ループについて不変であれば、
assertion の正当性をいえる
• そこで、次に W(0) が不変であるかどうかを
確かめる
– W(0) を仮定した下で、ループを一回実行したら、
実行後にも W(0) が成り立っているか？
8
Induction-Iteration:
Loop Invariant Generation
void foo(int s, int n) {
int i = 0;
while (1) {
{W(1) ≡ i+1 < n ==> (0 <= i+1 && i+1 < s)}
if (i < n) {
assert(0 <= i && i < s);
}
{i+1 < n ==> (0 <= i+1 && i+1 < s)}
i = i + 1;
{W(0)}
}
9
}
Induction-Iteration:
Loop Invariant Generation
• W(0) ==> W(1) が成り立つか？
• 成り立つ場合、W(0)がループ不変式と分かる
• 成り立たない場合、
– 式を一般化する： ∀i. W(0) ==> W(1)
– 量化子を消す
– これを新たな不変式の候補として、繰り返す
10
Induction-Iteration の問題点
• 今回の例の場合、 n <= s が得られる
n<=0 || n<=s と比べて、強い条件
• ループ不変式の計算の際に、ループの外の
情報を使わないので、条件が強くなった
– ループの外から得られる ”i >= 0” という情報を
考慮していなかったので、 n <= 0 が
得られなかった
11
これまでの手法 2
• Abstract Debugging
– Bourdoncle, ESEC ’93
• 抽象解釈(Abstract Interpretation)を用いる
– プログラムの各点で、各変数の取りうる値を
知りたいが、厳密な計算は難しい
– 区間 [l, h] で表して近似的に計算する、など
• 前進伝播、後進伝播の計算を行う
12
Abstract Debugging:
Initial Forward Propagation
void foo(int s, int n) {
int i = 0;
{i == 0}
while (1) {
if (i < n) {
{0 <= i && i < n}
assert(0 <= i && i < s);
}
i = i + 1;
}
}
13
Abstract Debugging:
Backward Propagation
void foo(int s, int n) {
{n<=0 || (0<n && 0<s)}
int i = 0;
{(i==0 && n<=0) || (i==0 && 0<n && 0<s)}
while (1) {
{(0<=i && n<=i) || (0<=i && i<n && i<s)}
if (i < n) {
{0<=i && i<n && i<s}
assert(0 <= i && i < s);
}
i = i + 1;
}
}
14
Abstract Debugging の問題点
• 事前条件として n <= 0 || (0 < n && 0 < s)
が得られる
– 必要だが、十分な条件ではない
• 抽象解釈での近似による限界
– 区間による近似では、分岐の合流を扱いにくい
– x != y などの表現は扱いにくい
15
提案する手法
• 抽象解釈と最弱事前条件を組み合わせる
– ループの外からの情報も使いながら、
最弱事前条件を計算する
16
1. 前方抽象解釈を行う
• 各点で変数の取りうる範囲を、
近似的に求める（各点での不変式になる）
void foo(int s, int n) {
int i = 0;
while (1) {
if (i < n) {
{0<=i && i<n}
assert(0 <= i && i < s);
}
i = i + 1;
}
}
17
2. assertion を不変式で弱める
void foo(int s, int n) {
int i = 0;
while (1) {
if (i < n) {
{(0<=i && i<n) ==> i<s }
assert(0 <= i && i < s);
}
i = i + 1;
}
}
18
3. 最弱事前条件を計算する
void foo(int s, int n) {
int i = 0;
while (1) {
{(0<=i && i<n) ==> i<s}
if (i < n) {
{(0<=i && i<n) ==> i<s}
assert(0 <= i && i < s);
}
i = i + 1;
}
}
19
4. ループ変数を全称量化する
void foo(int s, int n) {
int i = 0;
{∀i. (0<=i && i<n) ==> i<s}
while (1) {
{(0<=i && i<n) ==> i<s}
if (i < n) {
assert(0 <= i && i < s);
}
i = i + 1;
}
}
20
5. 量化された変数を削除する
{requires n<=0 || n<=s}
void foo(int s, int n) {
{n<=0 || n<=s}
int i = 0;
{n<=0 || n<=s}
while (1) {
if (i < n) {
assert(0 <= i && i < s);
}
i = i + 1;
}
}
21
得られた事前条件
• 十分条件 n <= 0 || n <= s が得られた
• Induction-Iteration より優れている点
– ループの外からの情報を使える
• Abstract Debugging より優れている点
– 最弱事前条件の計算により、
十分条件が得られる
22
ポインタが存在する場合
• エイリアシングを考慮する必要がある
void bar(int *p, int *n) {
int i = 0;
while (1) {
if (i < *n) {
n と p+i が同じ
*(p + i) = 0;
場所を指している
}
かもしれない
i = i + 1;
}
}
23
エイリアシングへの対処
• 実際に人がプログラムを記述する際には、
エイリアスしていないことを前提としている
部分も多い
• そこで、このような前提を仮定として用いる
• 前の例では、n と p+i はエイリアスしていない、
と仮定してしまう
24
エイリアシングへの対処
• 具体的には、プログラムは次の規則に
従うものとして扱う
ポインタ変数 x を通したメモリへの書き込みと
読み込みの間に、別のメモリへの書き込みが
ある場合、その書き込みは x とは別の場所を
指している
25
エイリアシングへの対処
*x = 0;
…
*y = 10;
…
t = *x;
x と y が同じ場所を
指していた場合、
初めの書き込みを無効化
してしまう
そこで、 x と y は
異なる場所を指していると
考える
• このような規則を満たすものは、前と同様の
手法を用いて事前条件を計算できることが
示せる
26
扱いやすくするために
• 実際には、この規則を満たしているかどうか
確かめるのは難しいので、さらに強めた
次の条件を用いる
• 書き込みが行われる領域は互いに重ならない
• 読み込みだけが行われる領域と、
書き込みが行われる領域は互いに重ならない
 separated(p, q) と書くことにする
27
扱いやすくするために
• 前の例 (関数 bar) では separated(p, n)
p
n
• これを仮定して関数 bar を解析する
• separated(p, n) を仮定して事前条件の計算を
したので、 bar の呼出時には、この制約も
確かめる必要がある
28
実験結果
• Minix 3 Operating System 上で実装された
C の標準 string 関数に対して実行
• 20 の関数について、メモリ安全性を示すのに
十分な事前条件を推論できた
• strcat での例：
separated(dest[…],src[…])
&& offset_min(dest) <= 0 <= strlen(dest) <= offset_max(dest)
&& offset_min(src) <= 0 <= strlen(src) <= offset_max(src)
&& strlen(dest) + strlen(src) <= offset_max(dest)
29
実験結果
• Verisec buffer overflow benchmark に適用
– 実際のアプリケーション (sendmail, wu-ftpd など)
に存在した脆弱性からとられたベンチマーク
– 多くのものに対して十分な事前条件を推論できた
• バイナリサーチにおいて、整数オーバー
フローを起こさないための十分な事前条件を
推論できた
30
関連研究 (1/2)
• 配列境界検査・ループ不変式推論
– Abstract Interpretation
[Cousot and Halbwachs, POPL ’78]
– Induction-Iteration [Suzuki and Ishihara, POPL ’77]
• Modular Program Verification and
Precondition Inference
– Abstract Debugging [Bourdoncle, ESEC ’93]
31
関連研究 (2/2)
• Memory Separation and
Precondition Inference
– Pointer Separation
[Aiken et al., PLDI ’03] [Koes et al., MSP ’04] など
• 抽象解釈と演繹的証明の組み合わせ
– 抽象解釈と定理証明器を組み合わせて
ループ不変式を作る
[Leino and Logozzo, APLAS ’05]
32
まとめ
• assertion が成り立つことを証明するために
十分な事前条件を推論する方法を提案した
• 従来の方法を組み合わせて構成した
– 抽象解釈
– 最弱事前条件
– 量化子の削除
• あるルールに従う、ポインタを含むプログラム
に適用できることを示した
33

Download Report