A First Step Towards Automated Detection of Buffer

A First Step Towards Automated
Detection of Buffer Overrun
Vulnerabilities
情報理工学系研究科米澤研
M1 田渕直 ([email protected])
概要
• C言語で書かれたプログラムに存在する、
潜在的な Buffer Overrun バグをソースコー
ドのstaticな解析によって検出する方法を
提案する。
Cプログラムの問題点
•
C言語はいくつかの点で安全ではない
–
–
配列境界をチェックしない
配列境界に無頓着なライブラリ関数の存在
e.g. gets(), strcpy(), etc…
–
ライブラリ関数の仕様の不統一
e.g.
strncpy(d, s, sizeof d)
strncat(d, s, sizeof d)
○
×
解決策の提案
• 安全でない言語使用やライブラリの結果、
– 正しいプログラムを書くのは難しい。
– 危険なプログラムはすぐに書ける。
• しかし、現実にはLegacyなC言語に頼らざ
るを得ない場面も多い。
⇒ 人手によらず、危険な個所を自動検出で
きるツールがあれば嬉しい。
システムの特徴 (1/4)
• 静的解析: Cソースプログラムの静的な解
析に基づいて危険な個所を検出する。
• Scalability > Precision: 検出結果の過不足
には目をつぶって、現実のアプリケーショ
ンに適用できる程度の性能を目指す。
• 対象: 解析の対象は文字列(と文字列用ラ
イブラリ関数)に限定。
システムの特徴 (2/4)
• 静的解析
– Runtime testing では全ての条件とパスをテス
トできるとは限らない。
– 特に、セキュリティ上最も重要なコードは、通
常実行されることのないパスに潜んでいる。
e.g.
if (strlen(src) > sizeof (dst)) break;
strcpy(dst, src);
What if strlen(src) == sizeof (dst) ?
システムの特徴 (3/4)
• C文字列を抽象データ型として扱う
– ポインタは一般に静的解析と相性が悪い。
– ほとんどの buffer overrun は文字列バッファに
ついて起こる。
⇒ 文字列とライブラリ関数の動作を直接モデル化
することによって、ポインタの解析を回避する。
ポインタを直接操作するようなコードは、誤りを検
出できない。
システムの特徴 (4/4)
• 「バッファ」のモデル化
– 文字列バッファを「確保サイズ」・「文字列長」
の整数範囲のペアとしてモデル化
⇒ 文字列の内容を意識しない処理が可能。
⇒ 問題を integer range constraint として定式化でき
る。
システムの制限
•
Scalability > Precision の構図に基づき、
以下の制限を設けた実装とした。
1. 制御フローを無視。
2. ポインタの解析はしない。
3. 構造体は一括して扱う(次項)。
構造体の扱いについて
• Cの慣習として、構造体はポインタと組み
合わせて使われることが多い。
• 構造体を無視しては実世界のアプリケー
ションを検証することはできない。
⇒ 同じ型の構造体のインスタンスは制約シ
ステム中で全て一括して扱うという方針で、
妥協的に解決した。
アーキテクチャ
Source
Integer constraint
Constraint solver
generation
Syntax
Consttree
raints
C parser
Warnings
制約の表現 (1/4)
• Integer range:
integer range は Z∞ = Z ∪ {±∞} の部分集
合で、[m, n] = {m, …, n}
• Range closure:
S ⊆ Z∞ に対し、
range-closure(S) = [inf S, sup S]
制約の表現 (2/4)
• Operations on range closure:
S, T ⊆ Z∞ に対し、
S+T=
range-closure({ s+t | s ∈S, t ∈ T})
S – T, S * T も同様に定義される。
• {n} を n と略記する。
e.g. 2T = {2} * T = { 2t | t ∈ T}
制約の表現 (3/4)
• Integer range expression:
e ::= v | n | n * v | e + e | e – e
| max(e, …, e) | min(e, …, e)
where n ∈ Z, v は変数。
• Integer range constraint:
制約は e ⊆ v の形に表される。
制約の表現 (4/4)
• Assignment:
assignment α は、各変数 v に対し
α(v) ⊆ Z∞ (実際には range)を割当てる。
• 定義: αが制約システムを満たす
⇔ constraint 中の各変数 v をα(v) で置き
換えた時に、全ての constraint が成立。
• 定義: α ⊆ β ⇔ α(v) ⊆ β(v) for ∀v
制約の生成 (1/3)
• Cソースの構文木から、一連の constraint
を生成する。
– 整数変数 v に対し、変数 v を対応させる。
– 文字列変数 s に対し、確保長 alloc(s) と文字
列長 len(s) を対応させる(* len(s) は‘\0’を含
む)。
– 代入 v = e に対し、e ⊆ v を生成。
– 各文字列操作に対し、対応する制約を生成。
制約の生成 (2/3)
文字列操作に対応する制約の例。
Code
Interpretation
char s[n];
n ⊆ alloc(s)
strlen(s)
len(s) - 1
strcpy(d, s);
len(s) ⊆ len(d)
s = “foo”;
4 ⊆ len(s), 4 ⊆ alloc(s)
p = malloc(n)
n ⊆ alloc(p)
strcat(s, suf);
len(s)+len(suf)-1 ⊆ len(s)
制約の生成 (3/3)
• 関数 f(int p)の呼出し
b = f(a);
は p = a、b = f_return と解釈。
• ポインタ操作
q = p+j;
は alloc(p) – j ⊆ alloc(q)、
len(p) – j ⊆ len(q) と解釈(aliasing等を無
視)。
制約の解決
• 制約の解決は、全ての変数が取り得る値の
範囲をカバーする最小の bounding box を
求めることに相当。
• 求まった bounding box から各 len(s) と
alloc(s) の関係を見ることでoverrun を検出。
アルゴリズム (1/2)
• とりあえず f(vi) = avi + b⊆ vj の形の制約
のみで考える。
–
–
–
–
各vi に頂点 vi を割り当て
制約 f(vi) ⊆ vj に対し、枝 vi →f vj を割り当て。
各viに対し α(vi) = φ
制約 n ⊆ vi に対し、
α(vi) = range-closure(α(vi) ∪ {n})
アルゴリズム (2/2)
• 前項の初期化の後、グラフの枝に沿って
情報を伝播させる。
– f(α(vi)) ⊈ α(vj) であれば
α(vj) = range-closure(α(vj) ∪ f(α(vi)))
• グラフが閉路を含んでいれば、その部分に
関しては、別途直接計算で解を求める。
擬似コード (1/2)
Constraint-Solver:
Set α(vi) = φ for all i, done = false
For each constraint of the form n ⊆ w
Set α(w) = range-closure(α(w)∪{n})
While done = false call One-Iteration
One-Iteration:
Set C(vi) = white for all i, done = true
For each vi
if (C(vi) == white)
Set prev(vi) = null, call Visit(vi)
擬似コード (2/2)
Visit(v):
Set C(v) = gray
For each constraint of the form f(v) ⊆ w
if (f(α(v)) ⊈ α(w))
Set α(w) =
range-closure(f(α(v)) ∪ α(w))
Set done = false
if (C(w) == gray)
Call Handle-Cycle(v, w, prev)
if (C(w) == white)
Set prev(w) = v, call Visit(w)
Set C(v) = black
Overrun の検出
•
•
制約の解決後、各 alloc(s), len(s) の関係
から overrun を検出。
alloc(s) = [a, b], len(s) = [c, d] として…
1. b ≦ c ⇒ overrun は起こらない。
2. a > d ⇒ 常にoverrunが起こる。
3. Otherwise ⇒ overrun が起こる可能性有り。
性能評価
• いくつかの実際に使用されているパッケー
ジに対してツールを適用し、性能評価を試
みた。
• 人手でソースを解読して false alerm 率を
測定。
評価1. Linux net tools
• Linux net tools に関して、今まで報告され
ていない問題を検出できた。
– DNS・NISの応答を信頼している個所があり、
悪意のある応答に対して脆弱。
• 既知の問題をどの程度検出できたかにつ
いては言及がなかった。
評価2. Sendmail 8.9.3 (1/2)
• 既知の問題の多さ、プログラム規模等の
面で sendmail は良い題材である。
• セキュリティホールは検出されなかったが、
queue の扱いに関して小さな off-by-one バ
グを検出した。
• False alerm 率の高さのため、人手による
検証に多くの時間がかかった。
評価2. Sendmail 8.9.3 (2/2)
•
False alerm の例
1. if (sizeof dst < strlen(src)+1) break;
strcpy(dst, src);
→ 制御フローを無視することによるもの。
2. char* ptr;
if (A) ptr = “abc”;
else ptr = “defgh”;
→ bounding box 解析の原理上の制限。
評価3. Sendmail 8.7.5
• 公表されていない数多くのバグを検出した。
• chfn に関する既知の問題は検出できな
かったらしい。
パフォーマンス
• Sendmail の検証にかかった時間は
Pentium III で15分程度。
• 検証結果を人手で確認する手間の方が大
きいので、CPU時間はそれほど問題になら
ないのではないか。
問題点
• 現在のシステムの主な問題点は,
– False alerm の多さ
– 検出ミスの可能性
– 出力の情報量不足
False alerm の多さ (1/2)
• Precision を犠牲にした設計のため、実際
には問題のないコードが引っかかることが
多く、結局人手での検証に負担がかかる。
e.g.
Sendmail の検証では Probable とされた
44箇所のうち、40箇所が false alerm だった。
False alerm の多さ (2/2)
• 解析手法の強化でど
の程度精度が向上す
るかを見積もった。
–
–
–
–
制御フロー
ポインタ解析
文脈の情報
Linear invariants
手法
結果
フロー
19/40
フロー +
ポインタ
フロー +
文脈 + inv.
25/40
全部
38/40
28/40
⇒ もう少し精度を重視しても良かったかもしれない。
検出ミスの可能性
• 検出ミスの数を完全に見積もることは難し
い。
• Sendmail 8.7.5 の検証では…
chfn に関するバグは検出できなかった
(ポインタを直接操作していたため)。
その他の、未公表のまま修正されていた
問題は全て検出した。
出力の情報量不足
• ツールの報告は「どのバッファが溢れる
か」のみ。「どこで溢れるか」は示されない
(制約に基づくシステムの原理的な限界)。
⇒ 「バッファ溢れに関係する変数名を同時に
報告する」というヒューリスティクスを採用し
て、多少の改善を試みた。
結論
• Buffer overrun の静的解析技法として、2つのア
イデアを提案した。
– 文字列のモデル化
– 制約に基づく解析
• このアプローチは十分に有効で実用的。
• 精度を犠牲にして、大きなプログラムに適用でき
るだけのscalabilityを達成できた。
• 人手では発見できない小さなバグも発見できた。
• 精度に関しては改善の余地がある。

Download Report