BEACON[SP'22] #
BEACON : Directed Gray-Box Fuzzing with Provable Path Pruning [SP'22]
事前知識 #
Fuzzing の分類 - 目的
- Directed ~ : プログラムの特定の箇所を集中的にテスト
- 用途に関しては AFLGo を参照
- Coverage-guided ~ : プログラム全体をテスト
Fuzzing の分類 - プログラムから得られる情報
- Black-box ~ : 無し (+ プログラムの出力)
- Gray-box ~ : 計装によるフィードバック
- White-box ~ : (動的)プログラム解析 (e.g. 記号実行) による情報
概要 #
目標 #
Directed Fuzzing において:
- なるべく早い段階での枝刈り
- なるべく多くのパスの枝刈り
- 低オーバーヘッド
以上を実現するために…
- 目的箇所から遡り、そこに到達するための**必要条件**を求める
- 各変数に関する条件を求める
- 必要条件を満たさないパスを枝刈り
課題 #
既存の Directed Fuzzer での課題:
- 無駄なパスを大量に実行している
- 無駄なパス:目的の箇所に到達しないパス
- 記号実行を使っている (Savior[SP'20])
- 記号実行はスケールしない
- 充足不能な条件に時間を浪費
- ヒューリスティックを使っている (AFLGo[CCS'17], Hawkeye[CCS'18])
- 目的の箇所に到達する保証が無い
提案手法 #
手法を一言で:目的箇所に到達するための事前条件を静的に求め、それを満たさないパスは早期に枝刈り
- 目的箇所から遡り、そこに到達するための**必要条件**を求める
- 各変数に関する条件を求める
- 必要条件を満たさないパスを枝刈り
→ 区間抽象化による静的解析での 2 つの最適化を提案:
- Relationship Preservation (後述)
- Bounded Disjunction (後述)
結果 #
- Directed gray-box fuzzer : ave. 11.50x faster
- Coverage-guided fuzzer : ~10.92x faster
- 10 new CVEs
準備 #
区間抽象化による静的解析 #
以下を順番に見る:
- Data-Flow Value (DFV)
- DFV の更新方法
- DFV のマージ方法
Data-Flow Value (DFV) #
各変数の値を(a,b)
のような形の区間で抽象化する
e.g.:
a
:[20,∞)
b
:[0,0]
c
:(-∞,∞)
DFV の更新方法 #
更新方法は 2 つ:
- 代入命令
- e.g.
x = 10;
→x
: $[10,10]$
- e.g.
- 条件分岐命令
- e.g.
- Then 節 →
x
: $[0, \infty)$ - Else 節 →
x
: $(-\infty,0]$
- Then 節 →
- e.g.
ただし:
- 当該変数のみ更新
- その他の変数は変更せずに伝播
DFV のマージ方法 #
マージ対象の区間全てを含む(最小の)区間を求める:
式で(ラフに)書くと:
- 各変数に関して、$[a,b] \land [c,d] \rightarrow [\mathrm{mix}(a,c),\mathrm{max}(b,d)]$
精度が落ちる場合がある:
- 上の 3. の場合: $[20,30]$ は精度低下の原因
具体例 #
例: (順方向)
各行直後でのプログラムの値
- 1 行目 →
a
: $\phi$,b
: $\phi$,c
: $\phi$ - 2 行目 →
a
: $\phi$,b
: $\phi$,c
: $\phi$ - 3 行目 →
a
: $\phi$,b
: $\phi$,c
: $\phi$ - 4 行目 →
a
: $\phi$,b
: $\phi$,c
: $\phi$ - 5 行目 →
a
: $\phi$,b
: $\phi$,c
: $\phi$ - 6 行目 →
a
: $\phi$,b
: $\phi$,c
: $\phi$ - 7 行目 →
a
: $\phi$,b
: $\phi$,c
: $\phi$ - 8 行目 →
a
: $\phi$,b
: $\phi$,c
: $\phi$
- 1 行目 →
a
: $\phi$,b
: $\phi$,c
: $\phi$ - 2 行目 →
a
: $(-\infty, \infty)$,b
: $\phi$,c
: $\phi$ - 3 行目 →
a
: $\phi$,b
: $\phi$,c
: $\phi$ - 4 行目 →
a
: $\phi$,b
: $\phi$,c
: $\phi$ - 5 行目 →
a
: $\phi$,b
: $\phi$,c
: $\phi$ - 6 行目 →
a
: $\phi$,b
: $\phi$,c
: $\phi$ - 7 行目 →
a
: $\phi$,b
: $\phi$,c
: $\phi$ - 8 行目 →
a
: $\phi$,b
: $\phi$,c
: $\phi$
- 1 行目 →
a
: $\phi$,b
: $\phi$,c
: $\phi$ - 2 行目 →
a
: $(-\infty, \infty)$,b
: $\phi$,c
: $\phi$ - 3 行目 →
a
: $(0, \infty)$,b
: $\phi$,c
: $\phi$ - 4 行目 →
a
: $\phi$,b
: $\phi$,c
: $\phi$ - 5 行目 →
a
: $\phi$,b
: $\phi$,c
: $\phi$ - 6 行目 →
a
: $\phi$,b
: $\phi$,c
: $\phi$ - 7 行目 →
a
: $\phi$,b
: $\phi$,c
: $\phi$ - 8 行目 →
a
: $\phi$,b
: $\phi$,c
: $\phi$
- 1 行目 →
a
: $\phi$,b
: $\phi$,c
: $\phi$ - 2 行目 →
a
: $(-\infty, \infty)$,b
: $\phi$,c
: $\phi$ - 3 行目 →
a
: $(0, \infty)$,b
: $\phi$,c
: $\phi$ - 4 行目 →
a
: $(0, \infty)$,b
: $[10,10]$,c
: $\phi$ - 5 行目 →
a
: $\phi$,b
: $\phi$,c
: $\phi$ - 6 行目 →
a
: $\phi$,b
: $\phi$,c
: $\phi$ - 7 行目 →
a
: $\phi$,b
: $\phi$,c
: $\phi$ - 8 行目 →
a
: $\phi$,b
: $\phi$,c
: $\phi$
- 1 行目 →
a
: $\phi$,b
: $\phi$,c
: $\phi$ - 2 行目 →
a
: $(-\infty, \infty)$,b
: $\phi$,c
: $\phi$ - 3 行目 →
a
: $\phi$,b
: $\phi$,c
: $\phi$ - 4 行目 →
a
: $\phi$,b
: $\phi$,c
: $\phi$ - 5 行目 →
a
: $(-\infty, 0]$,b
: $\phi$,c
: $\phi$ - 6 行目 →
a
: $\phi$,b
: $\phi$,c
: $\phi$ - 7 行目 →
a
: $\phi$,b
: $\phi$,c
: $\phi$ - 8 行目 →
a
: $\phi$,b
: $\phi$,c
: $\phi$
- 1 行目 →
a
: $\phi$,b
: $\phi$,c
: $\phi$ - 2 行目 →
a
: $(-\infty, \infty)$,b
: $\phi$,c
: $\phi$ - 3 行目 →
a
: $\phi$,b
: $\phi$,c
: $\phi$ - 4 行目 →
a
: $\phi$,b
: $\phi$,c
: $\phi$ - 5 行目 →
a
: $(-\infty, 0]$,b
: $\phi$,c
: $\phi$ - 6 行目 →
a
: $(-\infty, 0]$,b
: $[20,20]$,c
: $\phi$ - 7 行目 →
a
: $\phi$,b
: $\phi$,c
: $\phi$ - 8 行目 →
a
: $\phi$,b
: $\phi$,c
: $\phi$
- 1 行目 →
a
: $\phi$,b
: $\phi$,c
: $\phi$ - 2 行目 →
a
: $(-\infty, \infty)$,b
: $\phi$,c
: $\phi$ - 3 行目 →
a
: $(0, \infty)$,b
: $\phi$,c
: $\phi$ - 4 行目 →
a
: $(0, \infty)$,b
: $[10,10]$,c
: $\phi$ - 5 行目 →
a
: $(-\infty, 0]$,b
: $\phi$,c
: $\phi$ - 6 行目 →
a
: $(-\infty, 0]$,b
: $[20,20]$,c
: $\phi$ - 7 行目 →
a
: $(-\infty, \infty)$,b
: $[10,20]$,c
: $\phi$ - 8 行目 →
a
: $\phi$,b
: $\phi$,c
: $\phi$
パスの合流
- 1 行目 →
a
: $\phi$,b
: $\phi$,c
: $\phi$ - 2 行目 →
a
: $(-\infty, \infty)$,b
: $\phi$,c
: $\phi$ - 3 行目 →
a
: $[0, \infty)$,b
: $\phi$,c
: $\phi$ - 4 行目 →
a
: $[0, \infty)$,b
: $[10,10]$,c
: $\phi$ - 5 行目 →
a
: $(-\infty, 0]$,b
: $\phi$,c
: $\phi$ - 6 行目 →
a
: $(-\infty, 0]$,b
: $[20,20]$,c
: $\phi$ - 7 行目 →
a
: $(-\infty, \infty)$,b
: $[10,20]$,c
: $\phi$ - 8 行目 →
a
: $(-\infty, \infty)$,b
: $[10,20]$,c
: $[60,70]$
定式化 #
DFV | dict[変数, 区間] |
解析の方向 | 順方向・逆方向 |
伝達関数 | 参照 |
境界条件 | 全ての変数に関して $\phi$ |
パスの合流 | 参照, 各変数に関して $[a,b] \land [c,d] \rightarrow [\mathrm{mix}(a,c),\mathrm{max}(b,d)]$ |
初期化 | 全ての変数に関して $\phi$ |
以降、次を仮定する:
- 解析の開始: Fuzzing における目的箇所
- 解析の方向: 逆方向
区間抽象化における精度低下の原因 #
変数間の関係は追わないために精度が落ちる例 #
crash()
に到達する条件は? (crash()
から遡る)
- 3 行目 →
x
: $\phi$,y
: $\phi$,z
: $\phi$ - 4 行目 →
x
: $\phi$,y
: $\phi$,z
: $\phi$ - 5 行目 →
x
: $\phi$,y
: $\phi$,z
: $\phi$
- 3 行目 →
x
: $\phi$,y
: $\phi$,z
: $\phi$ - 4 行目 →
x
: $\phi$,y
: $\phi$,z
: $\phi$ - 5 行目 →
x
: $\phi$,y
: $(-\infty, 100)$,z
: $\phi$
- 3 行目 →
x
: $\phi$,y
: $\phi$,z
: $\phi$ - 4 行目 →
x
: $\phi$,y
: $(-\infty, 100)$,z
: $\phi$ - 5 行目 →
x
: $\phi$,y
: $(-\infty, 100)$,z
: $\phi$
この時点で x
, z
に関する情報はないため、y==x-z
の関係式は使えない
- 3 行目 →
x
: $\phi$,y
: $(-\infty, 100)$,z
: $(-\infty,50)$ - 4 行目 →
x
: $\phi$,y
: $(-\infty, 100)$,z
: $\phi$ - 5 行目 →
x
: $\phi$,y
: $(-\infty, 100)$,z
: $\phi$
Q. より正確な x
の事前条件は?
マージする時に精度が落ちる例 #
crash()
に到達する条件は? (crash()
から遡る)
- 2 行目 →
x
: $\phi$,y
: $\phi$ - 3 行目 →
x
: $\phi$,y
: $\phi$ - 4 行目 →
x
: $\phi$,y
: $\phi$ - 5 行目 →
x
: $\phi$,y
: $\phi$ - 6 行目 →
x
: $\phi$,y
: $\phi$ - 7 行目 →
x
: $\phi$,y
: $\phi$ - 8 行目 →
x
: $\phi$,y
: $\phi$
- 2 行目 →
x
: $\phi$,y
: $\phi$ - 3 行目 →
x
: $\phi$,y
: $\phi$ - 4 行目 →
x
: $\phi$,y
: $\phi$ - 5 行目 →
x
: $\phi$,y
: $\phi$ - 6 行目 →
x
: $\phi$,y
: $\phi$ - 7 行目 →
x
: $(0,\infty)$,y
: $\phi$ - 8 行目 →
x
: $\phi$,y
: $\phi$
- 2 行目 →
x
: $\phi$,y
: $\phi$ - 3 行目 →
x
: $\phi$,y
: $\phi$ - 4 行目 →
x
: $\phi$,y
: $\phi$ - 5 行目 →
x
: $\phi$,y
: $\phi$ - 6 行目 →
x
: $(-\infty, 5)$,y
: $\phi$ - 7 行目 →
x
: $(0,\infty)$,y
: $\phi$ - 8 行目 →
x
: $\phi$,y
: $\phi$
- 2 行目 →
x
: $\phi$,y
: $\phi$ - 3 行目 →
x
: $\phi$,y
: $\phi$ - 4 行目 →
x
: $\phi$,y
: $\phi$ - 5 行目 →
x
: $(-\infty, 5)$,y
: $(-\infty, 0]$ - 6 行目 →
x
: $(-\infty, 5)$,y
: $\phi$ - 7 行目 →
x
: $(0,\infty)$,y
: $\phi$ - 8 行目 →
x
: $\phi$,y
: $\phi$
- 2 行目 →
x
: $\phi$,y
: $\phi$ - 3 行目 →
x
: $\phi$,y
: $\phi$ - 4 行目 →
x
: $(25,\infty)$,y
: $\phi$ - 5 行目 →
x
: $\phi$,y
: $\phi$ - 6 行目 →
x
: $\phi$,y
: $\phi$ - 7 行目 →
x
: $(0,\infty)$,y
: $\phi$ - 8 行目 →
x
: $\phi$,y
: $\phi$
- 2 行目 →
x
: $\phi$,y
: $\phi$ - 3 行目 →
x
: $(25,\infty)$,y
: $(0,\infty)$ - 4 行目 →
x
: $(25,\infty)$,y
: $\phi$ - 5 行目 →
x
: $\phi$,y
: $\phi$ - 6 行目 →
x
: $\phi$,y
: $\phi$ - 7 行目 →
x
: $(0,\infty)$,y
: $\phi$ - 8 行目 →
x
: $\phi$,y
: $\phi$
- 2 行目 →
x
: $(-\infty,\infty)$,y
: $(-\infty,\infty)$ - 3 行目 →
x
: $(25,\infty)$,y
: $(0,\infty)$ - 4 行目 →
x
: $(25,\infty)$,y
: $\phi$ - 5 行目 →
x
: $\phi$,y
: $\phi$ - 6 行目 →
x
: $\phi$,y
: $\phi$ - 7 行目 →
x
: $(0,\infty)$,y
: $\phi$ - 8 行目 →
x
: $\phi$,y
: $\phi$
Q. より正確な x
の事前条件は?
BEACON の手法 #
事前条件の計算 #
Fuzzing までの流れ:
- 区間抽象化による事前条件の計算 w/ 最適化
- 計装 : 事前条件を満たさない場合、枝刈り
- CFG 上での Reachability 解析
- 分岐箇所に計装
- 計装済みバイナリを用いて fuzzing (省略)
区間抽象化による静的解析での最適化を提案:
- Relationship Preservation
- Bounded Disjunction
最適化 1. Relationship Preservation #
変数間の関係式を追跡し精度向上
手順:
- 変数間の演算 (e.g.
y==x-z
) は別で記憶しておく- x→
(-∞,∞)
, y→(a,b)
と仮定
- x→
- (伝播させる)
- 演算結果の変数 (e.g.
z
) に対する制約が判明 → 式 (e.g.x-z
) の制約にする - 式の制約から、演算元の変数 (e.g.
x
) の制約を導出する
Motivating Example 1 を用いた具体例:
- 3 行目 →
x
: $\phi$,y
: $\phi$,z
: $\phi$ - 4 行目 →
x
: $\phi$,y
: $\phi$,z
: $\phi$ - 5 行目 →
x
: $\phi$,y
: $\phi$,z
: $\phi$
- 3 行目 →
x
: $\phi$,y
: $\phi$,z
: $\phi$ - 4 行目 →
x
: $\phi$,y
: $\phi$,z
: $\phi$ - 5 行目 →
x
: $\phi$,y
: $(-\infty, 100)$,z
: $\phi$
- 3 行目 →
x
: $\phi$,y
: $\phi$,z
: $\phi$ - 4 行目 →
x
: $\phi$,y
: $(-\infty, 100)$,z
: $\phi$ - 5 行目 →
x
: $\phi$,y
: $(-\infty, 100)$,z
: $\phi$
追跡中の関係式:
y==x-z
- 3 行目 →
x
: $\phi$,y
: $(-\infty, 100)$,z
: $(-\infty,50)$ - 4 行目 →
x
: $\phi$,y
: $(-\infty, 100)$,z
: $\phi$ - 5 行目 →
x
: $\phi$,y
: $(-\infty, 100)$,z
: $\phi$
追跡中の関係式:
y==x-z
← これを用いてx
の制約を更新
- 3 行目 →
x
: $(-\infty, 150)$,y
: $(-\infty, 100)$,z
: $(-\infty,50)$ - 4 行目 →
x
: $\phi$,y
: $(-\infty, 100)$,z
: $\phi$ - 5 行目 →
x
: $\phi$,y
: $(-\infty, 100)$,z
: $\phi$
追跡中の関係式:
y==x-z
← これを用いてx
の制約を更新
最適化 2. Bounded Disjunction #
複数の制約を持てるようにする、パス合流地点での精度低下を防ぐ
DFV | dict[変数, 区間] list[dict[変数, 区間]] ただし数には上限あり |
解析の方向 | 逆方向 |
伝達関数 | 参照 |
境界条件 | 全ての変数に関して $\phi$ |
パスの合流 | 下を参照 |
初期化 | 全ての変数に関して $\phi$ |
- 各ポイントで複数のパスの条件を別々で持つ
- ただし、別々でもてる数には上限あり (ref. パス爆発)
- そのために、以下を変更する必要がある
- DFV
- マージ方法
DFV に対する変更 #
- DFV:
list[dict[変数, 区間]]
- → マージによる精度の損失を回避できる
- ただし、数には上限を設ける
- パスの数は指数的に増える → 制約数が爆発してしまう
具体例:
- 2 行目 → [{
x
: $\phi$,y
: $\phi$}] - 3 行目 → [{
x
: $\phi$,y
: $\phi$}] - 4 行目 → [{
x
: $\phi$,y
: $\phi$}] - 5 行目 → [{
x
: $\phi$,y
: $\phi$}] - 6 行目 → [{
x
: $\phi$,y
: $\phi$}] - 7 行目 → [{
x
: $\phi$,y
: $\phi$}] - 8 行目 → [{
x
: $\phi$,y
: $\phi$}]
- 2 行目 → [{
x
: $\phi$,y
: $\phi$}] - 3 行目 → [{
x
: $\phi$,y
: $\phi$}] - 4 行目 → [{
x
: $\phi$,y
: $\phi$}] - 5 行目 → [{
x
: $\phi$,y
: $\phi$}] - 6 行目 → [{
x
: $\phi$,y
: $\phi$}] - 7 行目 → [{
x
: $[0,\infty)$,y
: $\phi$}] - 8 行目 → [{
x
: $\phi$,y
: $\phi$}]
- 2 行目 → [{
x
: $\phi$,y
: $\phi$}] - 3 行目 → [{
x
: $\phi$,y
: $\phi$}] - 4 行目 → [{
x
: $\phi$,y
: $\phi$}] - 5 行目 → [{
x
: $\phi$,y
: $\phi$}] - 6 行目 → [{
x
: $(-\infty, 5)$,y
: $\phi$}] - 7 行目 → [{
x
: $(0,\infty)$,y
: $\phi$}] - 8 行目 → [{
x
: $\phi$,y
: $\phi$}]
- 2 行目 → [{
x
: $\phi$,y
: $\phi$}] - 3 行目 → [{
x
: $\phi$,y
: $\phi$}] - 4 行目 → [{
x
: $\phi$,y
: $\phi$}] - 5 行目 → [{
x
: $(-\infty, 5)$,y
: $(-\infty, 0]$}] - 6 行目 → [{
x
: $(-\infty, 5)$,y
: $\phi$}] - 7 行目 → [{
x
: $(0,\infty)$,y
: $\phi$}] - 8 行目 → [{
x
: $\phi$,y
: $\phi$}]
- 2 行目 → [{
x
: $\phi$,y
: $\phi$}] - 3 行目 → [{
x
: $\phi$,y
: $\phi$}] - 4 行目 → [{
x
: $(25,\infty)$,y
: $\phi$}] - 5 行目 → [{
x
: $\phi$,y
: $\phi$}] - 6 行目 → [{
x
: $\phi$,y
: $\phi$}] - 7 行目 → [{
x
: $[0,\infty)$,y
: $\phi$}] - 8 行目 → [{
x
: $\phi$,y
: $\phi$}]
- 2 行目 → [{
x
: $\phi$,y
: $\phi$}] - 3 行目 → [{
x
: $(25,\infty)$,y
: $(0,\infty)$}] - 4 行目 → [{
x
: $(25,\infty)$,y
: $\phi$}] - 5 行目 → [{
x
: $\phi$,y
: $\phi$}] - 6 行目 → [{
x
: $\phi$,y
: $\phi$}] - 7 行目 → [{
x
: $[0,\infty)$,y
: $\phi$}] - 8 行目 → [{
x
: $\phi$,y
: $\phi$}]
- 2 行目 →
[{x
: $(25,\infty)$,y
: $(0,\infty)$}, {x
: $(-\infty, 5)$,y
: $(-\infty, 0]$}] - 3 行目 → [{
x
: $(25,\infty)$,y
: $(0,\infty)$}] - 4 行目 → [{
x
: $(25,\infty)$,y
: $\phi$}] - 5 行目 → [{
x
: $\phi$,y
: $\phi$}] - 6 行目 → [{
x
: $\phi$,y
: $\phi$}] - 7 行目 → [{
x
: $[0,\infty)$,y
: $\phi$}] - 8 行目 → [{
x
: $\phi$,y
: $\phi$}]
マージ方法に対する変更 #
なるべく精度が落ちないようにマージする
マージ方法:
- リストの長さが上限に
- 達していない場合:
- リストに制約を追加
- 達している場合:
- 以下の $L$ が最小になるような制約 (
dict[変数, 区間]
) を見つけ、その制約にマージ - $L(\phi_1, \phi_2) = \sum_{v \in \phi_1 \cap \phi_2} \mathrm{min}(\mathrm{max}(0, l_2 - u_1), \mathrm{max}(0, l_1 - u_2))$
- $v_{\phi_1} = [l_1, u_1]$
- $v_{\phi_2} = [l_2, u_2]$
- 以下の $L$ が最小になるような制約 (
- 達していない場合:
$L$ の直感的な意味
- 重なる領域がある → $L = 0$
- 重なる領域がない → $L = $スキマの幅
具体例:
- $\text{[B, C]}$ に対して $A$ を追加したい。
- Q. $A$ は $B$ と $C$ のどちらにマージすべき?
事前条件に基づく計装 #
計装方法:
- プログラムを SSA 形式に変換し、代入箇所に計装する。
- 変数の代入箇所で事前条件のチェック ✅
- ある変数 $v_1$ が $v_2$ のみ依存している場合、$v_1$ には計装しない。
- $v_2$ のチェックを行えば十分
具体例:
解析結果:
- 3 行目 →
x
: $(-\infty, 150)$,y
: $(-\infty, 100)$,z
: $(-\infty,50)$
→ 1 行目直後に計装
解析結果:
- 2 行目 →
[{x
: $(25,\infty)$,y
: $(0,\infty)$}, {x
: $(-\infty, 5)$,y
: $(-\infty, 0]$}]
→ 1 行目直後に計装
CFG 上での Reachability 解析 #
Fuzzing までの流れ:
- 区間抽象化による事前条件の計算 w/ 最適化
- 計装 : 事前条件を満たさない場合、枝刈り
- CFG 上での Reachability 解析
- 分岐箇所に計装
- 計装済みバイナリを用いて fuzzing (省略)
目的箇所に到達し得ないパスは早期に枝刈り:
評価 #
- 環境: Intel Xeon E5-1620 v3 (3.50GHz, 4core), 64GB of RAM, ubuntu 16.04
- 実装: LLVM bitcode 上で静的解析 + 計装
- Fuzzing engine: AFLGo[CCS'17] (計装済みバイナリを AFLGo で fuzzing)
- 比較対象:
- Directed:
- AFLGo[CCS'17] : 入力と目的箇所との"距離"を導入。“距離"を基に入力を変化させる。
- Hawkeye[CCS'18] : 関数の呼び出し履歴を考慮した"距離"の導入。同上。
- Directed:
- バグを含むリアル検体
Project Program Version Input format Num. CVEs Binutils cxxfilt 2.26 TXT 2 objdump 2.28 ELF 7 objcopy 2.28 ELF 4 Libjpeg cjpeg 2.04 JPG 1 cjpeg 1.98 JPG 1 Ming swftophp 0.4.7 SWF 7 swftophp 0.4.8 SWF 10 Libxml2 xmllint 20902 XML 4 Lrzip lrzip 0.631 ZIP 2 Libpng pngimage 1.6.35 PNG 1 pdftoppm 0.74 PDF 3 Libpoppler pdftops 0.74 PDF 1 pdfdetach 0.71 PDF 3 Libav avaconv 12.3 AVI/AAC 5 - Bounded Disjunction : 5
実験 #
Research Questions:
- RQ1: 既存の fuzzing engine に比べて効率よくバグを再現できるか
- RQ2: 1. 事前条件による枝刈り と 2. Reachability 解析 それぞれの効果はどの程度か
- RQ3: 抽象解釈における 2 つの最適化それぞれの効果はどの程度か
- RQ4: Fuzzing 時のオーバーヘッドはどの程度か
実験 1: 既存の fuzzing engine とのバグ再現における比較 #
CVE が割り当てられたバグを fuzzing で再現できるか?
見方:
- $T_{AFLGo}$ : AFLGo[CCS'17] でバグを再現するまでの時間
- $T_{all} = T_{sa} + T_{f}$
- $T_{sa}$ : BEACON での静的解析にかかった時間
- $T_{f}$ : BEACON で計装したバイナリでバグを再現するまでの時間
- $N$ : 実行回数
- $F$ : 枝刈りしたパスの割合
- T.O. : Time Out (>120h)
結果:
AFLGoとの比較表
Program CVE $T_{AFLGo}$ $T_{sa}$ $T_{f}$ $T_{all}$ $N$ $F$ ming$_{\text{4.7}}$ 2016-9827 1.25h 43s 0.31h 0.32h 0.28M 80.7% 2016-9829 T.O. 18s 5.54h 5.55h 5.25M 82.6% 2016-9831 2.52h 16s 0.62h 0.62h 0.47M 84.3% 2017-7578 2.43h 20s 0.29h 0.30h 0.26M 80.8% 2017-9988 37.99h 20s 1.45h 1.46h 1.26M 72.3% 2017-11728 T.O. 27s 11.14h 11.15h 23.70M 84.6% 2017-11729 4.34h 27s 1.02h 1.03h 2.02M 82.0% ming$_{\text{4.8}}$ 2018-7868 T.O. 21s 1.75h 1.76 h 3.91M 85.8% 2018-8807 10.71h 16s 1.89h 1.89h 4.42M 83.9% 2018-8962 35.39h 20s 1.92h 1.93h 5.96M 88.8% 2018-11095 60.29h 20s 3.13h 3.14h 6.07M 84.9% 2018-11225 34.23h 17s 2.84h 2.84h 4.33M 91.7% 2018-11226 37.59h 18s 3.98h 3.99h 5.25M 89.0% 2018-20427 T.O. 21s 3.14h 3.15h 7.81M 86.2% 2019-9114 T.O. 22s 3.53h 3.54h 7.08M 84.0% 2019-12982 T.O. 20s 2.47h 2.48h 4.12M 82.3% 2020-6628 T.O. 24s 3.91h 3.92h 8.76M 84.3% lrzip 2017-8846 5.05h 61s 1.78h 1.80h 1.32M 86.4% 2018-11496 3.01h 68s 1.17h 1.19h 0.89M 92.4% cxxfilt 2016-4491 7.74h 2,229s 1.38h 2.00h 7.69M 95.9% 2016-6131 5.88h 2,258s 0.84h 1.47h 3.76M 94.9% xmllint 2017-5969 2.07h 5,381s 0.17h 1.66h 0.33M 95.1% 2017-9047 T.O. 5,238s 16.55h 18.01h 16.46M 83.6% 2017-9048 T.O. 7,049s 18.00h 19.96h 18.47M 85.1% 2017-9049 TO. 5.672s 31.56h 33.14h 40.15M 95.2% 2017-8392 T.O. 2,654s 8.42h 9.16h 1.97M 79.3% 2017-8396 T.O. 2,909s 39.03h 39.84h 95.85M 91.2% 2017-8397 T.O. 3,067s 83.46h 84.31h 261.2M 96.1% objdump 2017-8398 T.O. 2,825s 40.51h 41.29h 166.3M 96.0% 2017-14940 T.O. 3,420s 61.38h 62.33h 41.13M 86.1% 2017-16828 T.O. 3,326s 22.24h 10.59h 4.32M 94.3% 2018-17360 T.O. 2,950s 45.69h 46.51h 121.55M 92.6% 2017-7303 T.O. 2,033s 20.09h 20.65h 31.75M 85.7% objcopy 2017-8393 T.O. 2,484s 19.78h 20.47h 20.21M 90.5% 2017-8394 T.O. 2,671s 4.46h 5.20h 4.74M 92.3% 2017-8395 T.O. 2,608s 3.83h 4.55h 4.31M 96.9% cjpeg 2018-14498 49.78h 93s 11.46h 11.46h 20.12M 91.2% 2020-13790 7.34h 106s 3.98h 4.01h 19.78M 90.4% pngimage 2018-13785 T.O. 85s 3.22h 3.23h 65.81M 91.3% pdftoppm 2019-10872 T.O. 4,904s 102.90h 104.26h 2.98M 76.5% 2019-10873 T.O. 5,899s 90.25h 91.89h 3.76M 69.4% 2019-14494 T.O. 4,153s 95.35h 96.50h 3.13M 67.2% pdftops 2019-10871 T.O. 6,593s 62.54h 64.37h 12.94M 75.2% 2018-19058 T.O. 2,950s 73.98h 74.80h 14.60M 86.3% pdfdetach 2018-19059 T.O. 2,686s 82.46h 83.21h 14.21M 81.1% 2018-19060 T.O. 2,995s 92.65h 93.48h 13.76M 70.1% 2018-11102 T.O. 14,335s 89.57h 93.55h 6.00M 53.4% 2018-11224 T.O. 14,893s 98.20h 102.34h 7.65M 69.8% avconv 2018-18829 T.O. 14,623s 47.97h 52.03h 3.44M 56.7% 2019-14441 T.O. 16,600s 52.86h 57.47h 6.89M 51.3% 2019-14443 T.O. 14,239s 95.81h 99.77h 13.49M 52.6% Avg. 11.50x 82.9%
- バグ再現 (全 51 個)
- AFLGo : 34
- BEACON : 51
- 高速化
- 最低: 1.2x
- 最高: 68.5x
- 平均: 11.50x
- 枝刈り
- ほとんどの場合で
80%以上枝刈り
- ほとんどの場合で
実験 2: 事前条件による枝刈りと Reachability 解析による枝刈りの効果 #
BEACON では 2 つの枝刈りを行っている:
- 各変数の事前条件のによる枝刈り
- Reachability 解析による枝刈り (Path Slicing)
実験設定:
Path Slicing | 事前条件での枝刈り | Relationship Preservation | Bounded Disjunction | |
---|---|---|---|---|
BEACON | ✅ | ✅ | ✅ | ✅ |
BEACON* | ✅ | ❌ | - | - |
結果:
- 見方
- 横軸: 51 個 の CVE
- 縦軸: バグの再現にかかった時間 (h)
- BEACON* → 再現できないバグ有
- Time Out (>120h)
- BEACON の方が速く再現できる
- 1.1x ~ 18.4x 速い
- 見方
- 横軸: 51 個 の CVE
- 縦軸: 枝刈りできたパスの割合
- 事前条件による枝刈り
- 平均で 29.1% 多く枝刈りできる
- → 事前条件での枝刈りは fuzzing の効率化に貢献
実験 3: 抽象解釈における 2 つの最適化それぞれの効果 #
(事前条件を求めるための) 抽象解釈における最適化:
- Relationship Preservation
- Bounded Disjunction
実験設定:
Path Slicing | 事前条件での枝刈り | Relationship Preservation | Bounded Disjunction | |
---|---|---|---|---|
BEACON | ✅ | ✅ | ✅ | ✅ |
BEACON* | ✅ | ❌ | - | - |
BEACON-$rp$ | ✅ | ✅ | ✅ | ❌ |
BEACON-$bd$ | ✅ | ✅ | ❌ | ✅ |
結果:
- 読み方
- 横軸: 51 個 の CVE
- 縦軸: BEACON* に対するバグ再現までの時間の割合
- 観察
- BEACON-$rp$ → BEACON : 1.05x ~ 4.9x 速い
- BEACON-$bd$ → BEACON : 1.05x ~ 5.34x 速い
- 2 つの最適化が静的解析の精度向上に貢献している
- 枝刈りの精度向上 → fuzzing の効率化
実験 4: Fuzzing 時のオーバーヘッド #
- $N_exec$ : プログラムの実行回数
- $T_{orig}$ : 計装無しの実行時間
- $T_{Beacon}$ : 計装有りの実行時間 (比較のため、枝刈りはせず条件比較のみ)
Project | $N_{exec}$ | $T_{orig}$ | $T_{Beacon}$ | Overhead |
---|---|---|---|---|
Ming | 126K | 4.52m | 4.80m | 6.2% |
Binutils | 2.38M | 2.48h | 2.51h | 1.2% |
Libxml | 25K | 0.63h | 0.65h | 3.2% |
Lrzip | 1.07M | 1.43h | 1.57h | 9.8% |
Libjpeg | 2.97M | 0.59h | 0.61h | 3.4% |
Libpng | 1.41M | 7.55h | 8.01h | 6.1% |
Libpoppler | 1.21M | 23.73h | 25.27h | 6.5% |
Libav | 7.62M | 23.87h | 26.13h | 9.5% |
- 最大 9.8%, 平均 5.7%のオーバーヘッド
- 許容範囲内であるだろう
関連研究 #
入力 | 効率的か | オーバーヘッド | 効率化のための工夫 | |
---|---|---|---|---|
AFLGo[CCS'17] | src+loc | ❌ | 小 | “距離” の導入 |
Hawkeye[CCS'18] | src+loc | ❌ | 小 | “距離” の計算方法の改善 |
FuZZGuard[SEC'20] | src+loc | ❌ | 中(?) | 機械学習ベースの手法、“良い"入力を学習させる |
Savior[SP'20] | src | ❌ | 大 | 1. ConcEx 2. 怪しい箇所の自動特定 |
BEACON[SP'22] | src+loc | ✅ | 中 | 枝刈り |
- 略語
- src: ソースコード
- loc: プログラム中の目的箇所
- ConcEx: Concrete Execution
提案手法との関連 #
Transient Attack 関連の論文は以下に分類できる:
- 攻撃
- Gadget 探索
- CPU のテスト
- 防御
- Transient Instruction の無効化
- メモリ隔離 (memory isolation)
- アーキテクチャレベルの隔離 (architectural isolation)
- 安全な投機実行 (secure speculative execution)
- Covert Channel の無効化
- 時間的隔離 (time/temporal isolation)
- その他
- 検証系
- (学部) 提案手法: 動的テイント解析 + 動的キャッシュシミュレーター
- メモリアクセスに関する静的解析を行うことで、枝刈りを行える可能性
- その際の静的解析の参考になる
- Gadget 探索:
- 「静的解析で得られた情報を基に枝刈り」というアイデアは活かせそう
- Directed-fuzzer は網羅的な Gadget 探索には向かない
- が、fuzzing 効率化という面では役に立つ
- e.g. 入力形式が複雑な場合に、正しい入力の発見を効率化
- が、fuzzing 効率化という面では役に立つ