BEACON[SP'22]

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

準備 #

区間抽象化による静的解析 #

以下を順番に見る:

  1. Data-Flow Value (DFV)
  2. DFV の更新方法
  3. DFV のマージ方法

Data-Flow Value (DFV) #

各変数の値を(a,b)のような形の区間で抽象化する

e.g.:

  • a : [20,∞)
  • b : [0,0]
  • c : (-∞,∞)

DFV の更新方法 #

更新方法は 2 つ:

  1. 代入命令
    • e.g. x = 10;x : $[10,10]$
  2. 条件分岐命令
    • e.g.
      1if (x>0)
      2  ...
      3else
      4  ...
      
      • Then 節 → x : $[0, \infty)$
      • Else 節 → x : $(-\infty,0]$

ただし:

  • 当該変数のみ更新
  • その他の変数は変更せずに伝播

DFV のマージ方法 #

マージ対象の区間全てを含む(最小の)区間を求める:

intro_interval

式で(ラフに)書くと:

  • 各変数に関して、$[a,b] \land [c,d] \rightarrow [\mathrm{mix}(a,c),\mathrm{max}(b,d)]$

精度が落ちる場合がある:

  • 上の 3. の場合: $[20,30]$ は精度低下の原因

具体例 #

例: (順方向)

1int a, b, c;
2a = input();
3if (a > 0) {
4  b = 10;
5} else {
6  b = 20;
7}
8c = b + 50;

各行直後でのプログラムの値

  • 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]$

定式化 #

DFVdict[変数, 区間]
解析の方向順方向・逆方向
伝達関数参照
境界条件全ての変数に関して $\phi$
パスの合流参照, 各変数に関して $[a,b] \land [c,d] \rightarrow [\mathrm{mix}(a,c),\mathrm{max}(b,d)]$
初期化全ての変数に関して $\phi$

以降、次を仮定する:

  • 解析の開始: Fuzzing における目的箇所
  • 解析の方向: 逆方向

区間抽象化における精度低下の原因 #

変数間の関係は追わないために精度が落ちる例 #

crash() に到達する条件は? (crash() から遡る)

1int x,y,z;
2
3if (z<50);
4  if (y==x-z)
5    if (y<100)
6      crash();

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$

この時点で 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() から遡る)

1int x,y;
2
3if (y>0)
4  x = x - 25;
5else
6  x = -x + 5;
7if (x > 0)
8  crash();

Motivating Example 2

  • 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 までの流れ:

  1. 区間抽象化による事前条件の計算 w/ 最適化
    • 計装 : 事前条件を満たさない場合、枝刈り
  2. CFG 上での Reachability 解析
    • 分岐箇所に計装
  3. 計装済みバイナリを用いて fuzzing (省略)

区間抽象化による静的解析での最適化を提案:

  • Relationship Preservation
  • Bounded Disjunction

最適化 1. Relationship Preservation #

変数間の関係式を追跡し精度向上

手順:

  1. 変数間の演算 (e.g. y==x-z) は別で記憶しておく
    • x→(-∞,∞), y→(a,b) と仮定
  2. (伝播させる)
  3. 演算結果の変数 (e.g. z) に対する制約が判明 → 式 (e.g. x-z) の制約にする
  4. 式の制約から、演算元の変数 (e.g. x) の制約を導出する

Motivating Example 1 を用いた具体例:

1int x,y,z;
2
3if (z<50);
4  if (y==x-z)
5    if (y<100)
6      crash();

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 #

複数の制約を持てるようにする、パス合流地点での精度低下を防ぐ

DFVdict[変数, 区間]list[dict[変数, 区間]] ただし数には上限あり
解析の方向逆方向
伝達関数参照
境界条件全ての変数に関して $\phi$
パスの合流下を参照
初期化全ての変数に関して $\phi$
  • 各ポイントで複数のパスの条件を別々で持つ
    • ただし、別々でもてる数には上限あり (ref. パス爆発)
  • そのために、以下を変更する必要がある
    • DFV
    • マージ方法
DFV に対する変更 #
  • DFV: list[dict[変数, 区間]]
    • → マージによる精度の損失を回避できる
    • ただし、数には上限を設ける
      • パスの数は指数的に増える → 制約数が爆発してしまう

具体例:

1int x,y;
2
3if (y>0)
4  x = x - 25;
5else
6  x = -x + 5;
7if (x > 0)
8  crash();

Motivating Example 2

  • 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$ の直感的な意味

interval_loss
  • 重なる領域がある → $L = 0$
  • 重なる領域がない → $L = $スキマの幅

具体例:

  • $\text{[B, C]}$ に対して $A$ を追加したい。
  • Q. $A$ は $B$ と $C$ のどちらにマージすべき?
    interval_meet

事前条件に基づく計装 #

計装方法:

  1. プログラムを SSA 形式に変換し、代入箇所に計装する。
    • 変数の代入箇所で事前条件のチェック ✅
  2. ある変数 $v_1$ が $v_2$ のみ依存している場合、$v_1$ には計装しない。
    • $v_2$ のチェックを行えば十分

具体例:

1int x,y,z;
2assert(x<150 && y<100 && z<50);
3if (z<50);
4  if (y==x-z)
5    if (y<100)
6      crash();
7...

解析結果:

  • 3 行目 → x : $(-\infty, 150)$, y : $(-\infty, 100)$, z : $(-\infty,50)$

→ 1 行目直後に計装

1int x,y;
2assert(w<5 || 25<w);
3if (y>0)
4  x = x + 25;
5else
6  x = -x + 5;
7if (x > 0)
8  crash();
9...

解析結果:

  • 2 行目 →
    [{x : $(25,\infty)$, y : $(0,\infty)$}, {x : $(-\infty, 5)$, y : $(-\infty, 0]$}]

→ 1 行目直後に計装

CFG 上での Reachability 解析 #

Fuzzing までの流れ:

  1. 区間抽象化による事前条件の計算 w/ 最適化
    • 計装 : 事前条件を満たさない場合、枝刈り
  2. CFG 上での Reachability 解析
    • 分岐箇所に計装
  3. 計装済みバイナリを用いて fuzzing (省略)

目的箇所に到達し得ないパスは早期に枝刈り:

1int x,y,z;
2assert(x < 150 && y < 100 && z << 50);
3if (z<50);
4  if (y==x-z)
5    if (y<100)
6      crash();
7assert(false);
8...
 1int x,y;
 2assert(w < 5 || 25 < w);
 3if (y>0)
 4  x = x + 25;
 5else
 6  x = -x + 5;
 7if (x > 0)
 8  crash();
 9assert(false);
10...

評価 #

  • 環境: 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] : 関数の呼び出し履歴を考慮した"距離"の導入。同上。
  • バグを含むリアル検体
    ProjectProgramVersionInput formatNum. CVEs
    Binutilscxxfilt2.26TXT2
    objdump2.28ELF7
    objcopy2.28ELF4
    Libjpegcjpeg2.04JPG1
    cjpeg1.98JPG1
    Mingswftophp0.4.7SWF7
    swftophp0.4.8SWF10
    Libxml2xmllint20902XML4
    Lrziplrzip0.631ZIP2
    Libpngpngimage1.6.35PNG1
    pdftoppm0.74PDF3
    Libpopplerpdftops0.74PDF1
    pdfdetach0.71PDF3
    Libavavaconv12.3AVI/AAC5
  • 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との比較表
ProgramCVE$T_{AFLGo}$$T_{sa}$$T_{f}$$T_{all}$$N$$F$
ming$_{\text{4.7}}$2016-98271.25h43s0.31h0.32h0.28M80.7%
2016-9829T.O.18s5.54h5.55h5.25M82.6%
2016-98312.52h16s0.62h0.62h0.47M84.3%
2017-75782.43h20s0.29h0.30h0.26M80.8%
2017-998837.99h20s1.45h1.46h1.26M72.3%
2017-11728T.O.27s11.14h11.15h23.70M84.6%
2017-117294.34h27s1.02h1.03h2.02M82.0%
ming$_{\text{4.8}}$2018-7868T.O.21s1.75h1.76 h3.91M85.8%
2018-880710.71h16s1.89h1.89h4.42M83.9%
2018-896235.39h20s1.92h1.93h5.96M88.8%
2018-1109560.29h20s3.13h3.14h6.07M84.9%
2018-1122534.23h17s2.84h2.84h4.33M91.7%
2018-1122637.59h18s3.98h3.99h5.25M89.0%
2018-20427T.O.21s3.14h3.15h7.81M86.2%
2019-9114T.O.22s3.53h3.54h7.08M84.0%
2019-12982T.O.20s2.47h2.48h4.12M82.3%
2020-6628T.O.24s3.91h3.92h8.76M84.3%
lrzip2017-88465.05h61s1.78h1.80h1.32M86.4%
2018-114963.01h68s1.17h1.19h0.89M92.4%
cxxfilt2016-44917.74h2,229s1.38h2.00h7.69M95.9%
2016-61315.88h2,258s0.84h1.47h3.76M94.9%
xmllint2017-59692.07h5,381s0.17h1.66h0.33M95.1%
2017-9047T.O.5,238s16.55h18.01h16.46M83.6%
2017-9048T.O.7,049s18.00h19.96h18.47M85.1%
2017-9049TO.5.672s31.56h33.14h40.15M95.2%
2017-8392T.O.2,654s8.42h9.16h1.97M79.3%
2017-8396T.O.2,909s39.03h39.84h95.85M91.2%
2017-8397T.O.3,067s83.46h84.31h261.2M96.1%
objdump2017-8398T.O.2,825s40.51h41.29h166.3M96.0%
2017-14940T.O.3,420s61.38h62.33h41.13M86.1%
2017-16828T.O.3,326s22.24h10.59h4.32M94.3%
2018-17360T.O.2,950s45.69h46.51h121.55M92.6%
2017-7303T.O.2,033s20.09h20.65h31.75M85.7%
objcopy2017-8393T.O.2,484s19.78h20.47h20.21M90.5%
2017-8394T.O.2,671s4.46h5.20h4.74M92.3%
2017-8395T.O.2,608s3.83h4.55h4.31M96.9%
cjpeg2018-1449849.78h93s11.46h11.46h20.12M91.2%
2020-137907.34h106s3.98h4.01h19.78M90.4%
pngimage2018-13785T.O.85s3.22h3.23h65.81M91.3%
pdftoppm2019-10872T.O.4,904s102.90h104.26h2.98M76.5%
2019-10873T.O.5,899s90.25h91.89h3.76M69.4%
2019-14494T.O.4,153s95.35h96.50h3.13M67.2%
pdftops2019-10871T.O.6,593s62.54h64.37h12.94M75.2%
2018-19058T.O.2,950s73.98h74.80h14.60M86.3%
pdfdetach2018-19059T.O.2,686s82.46h83.21h14.21M81.1%
2018-19060T.O.2,995s92.65h93.48h13.76M70.1%
2018-11102T.O.14,335s89.57h93.55h6.00M53.4%
2018-11224T.O.14,893s98.20h102.34h7.65M69.8%
avconv2018-18829T.O.14,623s47.97h52.03h3.44M56.7%
2019-14441T.O.16,600s52.86h57.47h6.89M51.3%
2019-14443T.O.14,239s95.81h99.77h13.49M52.6%
Avg.11.50x82.9%

  • バグ再現 (全 51 個)
    • AFLGo : 34
    • BEACON : 51
  • 高速化
    • 最低: 1.2x
    • 最高: 68.5x
    • 平均: 11.50x
  • 枝刈り
    • ほとんどの場合で
      80%以上枝刈り

実験 2: 事前条件による枝刈りと Reachability 解析による枝刈りの効果 #

BEACON では 2 つの枝刈りを行っている:

  • 各変数の事前条件のによる枝刈り
  • Reachability 解析による枝刈り (Path Slicing)

実験設定:

Path Slicing事前条件での枝刈りRelationship PreservationBounded Disjunction
BEACON
BEACON*--

結果:

fig10a
  • 見方
    • 横軸: 51 個 の CVE
    • 縦軸: バグの再現にかかった時間 (h)
  • BEACON* → 再現できないバグ有
    • Time Out (>120h)
  • BEACON の方が速く再現できる
    • 1.1x ~ 18.4x 速い
fig10a
  • 見方
    • 横軸: 51 個 の CVE
    • 縦軸: 枝刈りできたパスの割合
  • 事前条件による枝刈り
    • 平均で 29.1% 多く枝刈りできる
  • → 事前条件での枝刈りは fuzzing の効率化に貢献

実験 3: 抽象解釈における 2 つの最適化それぞれの効果 #

(事前条件を求めるための) 抽象解釈における最適化:

  • Relationship Preservation
  • Bounded Disjunction

実験設定:

Path Slicing事前条件での枝刈りRelationship PreservationBounded Disjunction
BEACON
BEACON*--
BEACON-$rp$
BEACON-$bd$

結果:

fig11
  • 読み方
    • 横軸: 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
Ming126K4.52m4.80m6.2%
Binutils2.38M2.48h2.51h1.2%
Libxml25K0.63h0.65h3.2%
Lrzip1.07M1.43h1.57h9.8%
Libjpeg2.97M0.59h0.61h3.4%
Libpng1.41M7.55h8.01h6.1%
Libpoppler1.21M23.73h25.27h6.5%
Libav7.62M23.87h26.13h9.5%
  • 最大 9.8%, 平均 5.7%のオーバーヘッド
  • 許容範囲内であるだろう

関連研究 #

入力効率的かオーバーヘッド効率化のための工夫
AFLGo[CCS'17]src+loc“距離” の導入
Hawkeye[CCS'18]src+loc“距離” の計算方法の改善
FuZZGuard[SEC'20]src+loc中(?)機械学習ベースの手法、“良い"入力を学習させる
Savior[SP'20]src1. 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. 入力形式が複雑な場合に、正しい入力の発見を効率化