← ENSOFT の研究
2013年11月12日

制御フローグラフに対する
縮約に基づく変換☆

Akshay Deepak∗

Ahmed Tamrawi

Suresh Kothari

Department of Electrical and Computer Engineering
Iowa State University, Ames, Iowa, USA

概要

ソフトウェアプログラムの制御フローグラフは、プログラムが実行しうる文のあらゆる系列を（グラフとして）表現する。制御フローグラフはソフトウェアプログラムの静的解析に広く用いられている。その用途の一つは、安全でないスレッド同期やメモリリークといったソフトウェアの脆弱性や、スマートフォン内の機密情報を悪意ある Web サイトへ漏洩させるといった悪意ある振る舞いの特定である。我々は、そのような脆弱性や悪意ある振る舞いの多くが、制御フローグラフのパス上に 2 種類のノードが特定の順序で現れることとしてモデル化できることを強調する。制御フローグラフのパスの数は指数的になりうることがよく知られており、そのため脆弱性や悪意ある振る舞いの解析は実用的でなくなりうる。これを動機として、我々は、脆弱性や悪意ある振る舞いの特定に必要な情報を保ったまま、制御フローグラフのサイズを大きく縮小できる変換を述べる。我々は、脆弱性と悪意ある振る舞いのこの特徴付けと、それに対応するグラフ変換が、他の実世界の問題にも適用できることを訴えたい。

キーワード: ソフトウェア工学, グラフアルゴリズム, グラフ変換, 静的解析, 制御フローグラフ

☆ 本資料は、契約番号 FA8750-12-2-0126 のもとで DARPA が支援した研究に基づく。米国政府は、著作権表示にかかわらず、政府の目的のために別刷りを複製し配布する権限を有する。

∗ 責任著者

電子メールアドレス: akshayd@iastate.edu (Akshay Deepak), atamrawi@iastate.edu (Ahmed Tamrawi), kothari@iastate.edu (Suresh Kothari)

Elsevier に投稿されたプレプリント

目次

1. はじめに

コンピュータプログラムの制御フローグラフ（CFG）[1] は、プログラムが実行中にたどりうるすべてのパスを表現するグラフである。CFG は、コンピュータプログラムにおける実行の流れとデータの関係のあらゆる静的解析の中心にある。ソフトウェアのコードにおける脆弱性や悪意ある振る舞いの検出に CFG を用いることは、その一例である [2, 3]。我々は、ソフトウェアプログラムの脆弱性や悪意ある振る舞いを特定するのに不可欠な情報を保ったまま CFG のサイズを縮小する、CFG 上のグラフ変換を述べる。この縮約により、人間の分析者がソフトウェアプログラムのそのような脆弱性や悪意ある振る舞いを特定する時間を大きく短縮できる。

ソフトウェアの脆弱性と悪意ある振る舞いは、特定の種類のイベントの実行系列として特徴付けることができる。例えば、スレッド同期では、並行に実行される任意の二つのスレッドが、プログラムの共通部分を同時に実行しないことが求められる。ロックの使用は、スレッド同期を保証するためによく用いられる仕組みである。実行の過程でプログラムの共通部分に入るスレッドは、その共通部分に対応付けられたミューテックスオブジェクトのロックを獲得しなければならない。ミューテックスオブジェクト m に対するロックのイベントを L(m) で表す。共通部分を実行した後、スレッドはロックオブジェクトを解放し、並行に実行される他のスレッドが同様に共通部分を実行できるようにしなければならない。ミューテックスオブジェクト m に対する解放のイベントを U(m)（U はアンロックを示す）で表す。スレッドの安全な同期を検証するには、ミューテックスオブジェクト m について L(m) を含むすべての実行パスで、L(m) の後に U(m) が続くことを確認すべきである。メモリリークの脆弱性についても同様の解析ができる。アドレス a に対するメモリの各割り当ての後には、a に対応する解放が続かなければならない。MITRE corporation による Common Weaknesses Enumeration（http://cwe.mitre.org/index.html）に挙げられた多くの脆弱性は、同様の 2 イベントの特徴付けによってモデル化できる。

2 イベントの手法は、悪意ある振る舞いを特徴付けることもできる。例えば、スマートフォンアプリケーションにおける一般的なマルウェアの活動は、機密情報を悪意ある Web サイトへ漏洩させることである [4]。この活動は、機密情報 i に対する読み取りイベント（イベント R(i) で表す）の後に、i を悪意ある Web サイトへ送信するイベント（イベント P(i) で表す）が続くこととしてモデル化できる。したがって、マルウェアを含まないスマートフォンアプリケーションは次を満たさなければならない。機密情報 i についてイベント R(i) を持つ CFG のすべてのパスで、R(i) の後に、悪意ある Web サイトに対応する P(i) が続いてはならない。

CFG の実行パスの数は、入れ子になっていない分岐ノードの数に対して指数的に大きくなりうるため [1, 5]、上述の 2 イベントの特徴付けを用いてソフトウェアの脆弱性と悪意ある振る舞いを検証することは、計算コストが高くなりうる。これを動機として、我々は、ソフトウェアの脆弱性を検証するのに十分な情報を保ったまま CFG のサイズを大きく縮小できる、CFG 上の変換を述べる。ソフトウェアの脆弱性と悪意ある振る舞い以外にも、上述の 2 イベントの特徴付けは他の実世界の問題のモデル化に役立ちうると我々は考える。例えば、広い地理的範囲を覆うコンピュータネットワークを考える。それはグラフで表現でき、各ノードは送信元または宛先のコンピュータ（あるいはルーター）に対応する。一部のノードは攻撃に対して脆弱でありうるため、脆弱なノードを通過したデータパケットを走査するツールを動かす「警察」ノードをネットワークに追加する必要がありうる。警察ノードが適切に配置されているかを検証するには、脆弱なノードを持つすべてのパスで、脆弱なノードの後に警察ノードがなければならない。静的なソフトウェア解析に限らない CFG のこのような一般的な適用可能性に訴えるため、我々はグラフ変換をフローグラフという汎用的な枠組みで述べる。フローグラフとは、次の性質を持つ有向グラフ G である。

  1. ⊤（⊥）は出ていく（入ってくる）エッジのみを持つ唯一のノードであり、入口（出口）ノードと呼ばれる。
  2. すべてのノードは ⊤ から到達可能であり、⊥ はすべてのノードから到達可能である。
  3. ℐ は「重要」なノードの部分集合である。{⊤, ⊥} ∈ ℐ は常に成り立つ。

重要なノードがそう呼ばれるのは、フローグラフに対する我々の解析が、フローグラフのパスにおける重要なノードの系列に焦点を当てるからである。例えば、スレッドの安全な同期の解析では、重要なノードはロックとアンロックのイベントに対応する。

フローグラフにおいて複数の出ていくエッジを持つノードの集合を分岐ノードと呼ぶ。フローグラフ G について、VG、EG、ℐG、⊤G、⊥G は、それぞれ G のノードの集合、エッジの集合、重要なノードの集合、入口ノード、出口ノードを表す。フローグラフ G を順序付き集合 {VG, EG, ℐG, ⊤G, ⊥G} で定義する。フローグラフ G が文脈から明らかなときは、添字を省略する。二つのフローグラフ A と B について、A − B は VA ∖ VB によって誘導される A の部分グラフを表す。以下の議論では、特に断らない限り、G はフローグラフを表す。

G において、u（始点ノード）から v（終点ノード）へのエッジを順序対 (u, v) で表す。G における自己ループとは、G のあるノード u についての (u, u) という型のエッジである。|G| = |E| + |V| は G のサイズを表す。二つのエッジが共通の始点ノードと共通の終点ノードを持つとき、それらは並行であるという。

G における端から端へのパスとは、⊤ から ⊥ へのパスである。G におけるトレースとは、G の端から端へのパスで出会う重要なノードの系列である。二つの端から端へのパス p1 と p2 は、同じトレースを持つとき等価であるといい、p1 ≡ p2 と表す。明らかに、≡ はフローグラフの端から端へのパスの集合上の同値関係である。G のトレース内容は ΔG で表し、G のすべてのトレースの集合である。P を、P 内の任意の p1 と p2 について p1 ≢ p2 となる、G の端から端へのパスの極大集合とする。すると、ΔG は P 内のすべての端から端へのパスのトレースの和集合であり、|ΔG| = |P| であることは容易にわかる。すなわち、|P| は、G のすべての異なるトレースを評価するために考慮しなければならない端から端へのパスの最小数を表す。

2. グラフ変換

有向グラフに対する五つの縮約。T1 はノード u の自己ループを取り除く。T2 は並行エッジ e2 を削除して e1 を残す。T3 はノード u を v に畳み込む。T4 は破線で囲まれた単一後続部分グラフ S を、その後続 m へのエッジで置き換える。T5 は破線で囲まれた強連結成分 C を中継ノード c で置き換える。
図 1: グラフ変換の例

トレース内容を保ったまま G のサイズを縮小できれば、フローグラフ G のトレース内容の計算を簡単にできる。これを動機として、我々は次のグラフ変換を述べる。

型 T1: G 上の変換 T1 は、重要でないノード上の自己ループを取り除く。

明らかに、T1 は G のトレース内容を変えない。図 1a は T1 の例である。

型 T2: e1 と e2 を二つの並行エッジとする。G 上の変換 T2 は e2 を削除する。

明らかに、T2 は G のトレース内容を変えない。図 1b は T2 の例である。

型 T3: G 上の変換 T3 は、出ていくエッジがすべて共通のノード v で終わる重要でないノード u に作用し、u の出ていくエッジをすべて削除して u を v に同一視する。具体的には、次を行う。

  1. すべてのエッジ e = (t, u) について、e を削除し、エッジ (t, v) を G に追加する。
  2. u を G から削除する。

明らかに、T3 は G のトレース内容を変えない。図 1c は T3 の例である。

変換 T3 は、重要でないノードによって誘導される G の部分グラフ S であって、S から G − S へのすべてのエッジが共通のノード m で終わるものへと一般化できる。すなわち、S 内のすべてのエッジ (u, v) について v が S 内にあるか v = m となるようなノード m ∈ {VG ∖ VS} が存在する。このような部分グラフを単一後続部分グラフと呼び、m をその後続ノードと呼ぶ。これが変換 T4 の動機となる。

型 T4: 変換 T4 は、後続ノード m を持つ単一後続部分グラフ S を取り除き、G − S から S へ入るすべてのエッジが m で終わるようにする。具体的には、次を行う。

  1. v が S 内にあり u がそうでない G 内のすべてのエッジ (u, v) について、エッジ (u, m) を G に追加する。
  2. S を G から削除する。

明らかに、T4 は G のトレース内容を変えない。図 1d は T4 の例である。T3 は、単一後続部分グラフが単一のノードからなる場合の T4 の特殊な場合であることに注意する。G のすべての単一後続部分グラフに T4 をどのように適用できるかの議論は、すべてのグラフ変換を定義し終えるまで延期する。

この変換の背後にある直観は、重要でないノードによって誘導される G の強連結部分グラフにも適用できる。重要でないノードによって誘導される G の強連結部分グラフ C を考える。C に入るパスは、C から出ていくどのエッジを通っても出られることに注目する。したがって、パス上の重要なノードの系列のみを考える場合、C は中継点として振る舞う。すなわち、C を対応する中継ノードに吸収しても、G のトレース内容は変わらない。これが変換 T5 の動機となる。

型 T5: 重要でないノードによって誘導される G の極大強連結部分グラフ C について、変換 T5 は C を新しいノード c で置き換え、G − C から C へ入るすべてのエッジが c で終わり、C から G − C へ出ていくすべてのエッジが c から始まるようにする。具体的には、次を行う。

  1. ノード c を G に追加する。
  2. v が C 内にあり u がそうでない G 内のすべてのエッジ (u, v) について、エッジ (u, c) を G に追加する。
  3. u が C 内にあり v がそうでない G 内のすべてのエッジ (u, v) について、エッジ (c, v) を G に追加する。
  4. C を G から削除する。

明らかに、T5 は G のトレース内容を変えない。求める強連結成分は O(|G|) 時間で特定できる [6, Section 22.5][7]。したがって、T5 は O(|G|) 時間で行える。図 1e は T5 の例である。

2.1. T4 の適用

G に閉路がなければ、T3 を適用できなくなるまで繰り返し適用することで、G のすべての単一後続部分グラフに O(|G|) 時間で T4 を適用できることは容易にわかる。G に閉路がある場合は、G のノード m が G の単一後続部分グラフ S の後続ノードであるかを調べる。そのような S が存在すれば、S に T4 を適用する。G のノード m について、これはアルゴリズム 1 に示すように行える。

アルゴリズム 1 ノード m について、m を後続とする単一後続部分グラフの特定。

  1. G′ を、G から m を取り除いた部分グラフとする。
  2. 𝒮 を特定する。これは、重要でないノードによって誘導される G′ のすべての極大強連結部分グラフの集合である。
  3. 𝒮 内のすべての C について、C に T5 を適用する。
  4. L をノードの空リストで初期化する。G′ に出ていくエッジを持たない重要でないノード u がある限り、u を L に追加し、u を G′ から取り除くことを繰り返す。
  5. L 内のノード u が、ステップ 2 の 𝒮 内の強連結成分 C に対応するならば、L 内の u を VC で置き換える。
  6. L が空でなければ、L 内のノードによって誘導される G の部分グラフは、m を後続ノードとする単一後続部分グラフに対応する。そうでなければ、m を後続ノードとする単一後続部分グラフは存在しない。

m を後続ノードとする任意の単一後続部分グラフ S について、アルゴリズム 1 はまず、S に T5 を極大に適用することで S を非巡回グラフに変換する。次に、S を逆トポロジカル順にたどる。このたどりは、出ていくエッジがすべて S 内にあるノードを訪問する。G − S へ出ていくエッジを持つノードは決して訪問されない。したがって、アルゴリズム 1 は S が存在すれば正しく特定する。アルゴリズム 1 のステップ 2 の集合 𝒮 は O(|G|) 時間で計算できる [6, Section 22.5][7]。したがって、G の各ノードについて、アルゴリズム 1 は O(|G|) 時間を要する。したがって、G のすべての単一後続部分グラフは O(|G|2) 時間で特定できる。

次に、G のすべての単一後続部分グラフに O(|G|) 時間で T4 を適用することを可能にする、G の性質を述べる。

定義 1. 重要でないノードによって誘導される G のすべての極大強連結部分グラフ C が次を満たすとき、G は性質 𝒫 を満たす。C が単一後続部分グラフ S ≠ C の部分グラフでないならば、C は、C′ が G の単一後続部分グラフであるような部分グラフ C′ ≠ C を持たない。

G が 𝒫 を満たすならば、アルゴリズム 2 を用いて、G のすべての単一後続部分グラフに O(|G|) 時間で T4 を適用できる。

アルゴリズム 2 G が性質 𝒫 を満たすときの、O(|G|) 時間での G 上の T4 のすべての適用。

  1. 適用できなくなるまで G に T3 を適用する。
  2. 𝒮 を特定する。これは、重要でないノードによって誘導される G のすべての極大強連結部分グラフの集合である。
  3. 𝒮 内のすべての C について、C が単一後続部分グラフならば、C に T4 を適用する。
  4. 適用できなくなるまで G に T3 を適用する。

アルゴリズム 2 のステップ 3 では、極大強連結部分グラフ C について、C が単一後続部分グラフであるかを O(|C|) 時間で簡単に調べられる。したがって、アルゴリズム 2 は O(|G|) 時間を要する。アルゴリズム 2 の実行後に G に単一後続部分グラフが存在しないことを背理法で証明する。アルゴリズム 2 の実行後に、S を後続ノード m を持つ G の単一後続部分グラフとする。S は連結であるとする（そうでなければ S の連結成分を選ぶ。それもまた単一後続部分グラフである）。一般性を失わずに S は極大であるとする。すなわち、S′ が連結で S が S′ の部分グラフであるような、G の単一後続部分グラフ S′ ≠ S は存在しない。次の二つの場合がありうる。

  1. S に閉路がない場合: このとき S はトポロジカルソートできる。したがって、S 内に出ていくエッジを持たないノード u が S に存在する。G では ⊥ は S のすべてのノードから到達可能であるので、エッジ (u, m) が G に存在する。したがって、G において u に T3 を適用できる。これは矛盾である。
  2. S に閉路がある場合: S′ を S の複製とする。S′ のすべての極大強連結部分グラフに T5 を適用する。すると S′ はトポロジカルソートできる。したがって、S′ 内に出ていくエッジを持たないノード u が S′ に存在する。u が S のノードに対応するならば、前の場合と同じ理由によりエッジ (u, m) が G に存在する。したがって、G において u に T3 を適用できる。これは矛盾である。u が S の極大強連結部分グラフ C に対応するならば、C は m を後続ノードとする単一後続部分グラフ C である。しかし、C は G の極大強連結部分グラフでもなければならない。そうでなければ、C′ が単一後続部分グラフの部分グラフではなく（S は極大であるから）、かつ C が単一後続部分グラフであるような部分グラフ C を C′ が持つような、G の極大強連結部分グラフ C′ が存在する。しかし、これは G の性質 𝒫 に矛盾する。したがって、C は G の極大強連結部分グラフである。しかし、C はアルゴリズム 2 のステップ 2 と 3 で特定されなかった。これは矛盾である。

したがって、いずれの場合も矛盾に至る。以上で証明された。

G が性質 𝒫 を満たさない場合でも、アルゴリズム 2 は役立ちうる。まず G にアルゴリズム 2 を実行する。結果のグラフに単一後続部分グラフ S があるならば、G は性質 𝒫 に違反しているので、S は G の極大強連結部分グラフ C ≠ S の部分グラフでなければならない。したがって、G の残りの単一後続部分グラフを特定するには、G のすべてのノードではなく、G の極大強連結部分グラフ内のノードについてのみアルゴリズム 1 を実行すればよい。

以上のグラフ変換を動機として、G のトレース縮約形（TRF）を、適用できなくなるまで G に T1 − T5 を繰り返し適用した後に得られるフローグラフ G′ と定義する。G の TRF が O(|G|2) 時間で得られることは容易にわかる。

2.2. 分岐ノードの保持

分岐ノードは、端から端へのパスのトレースに価値を加えうる。n > 1 本の出ていくエッジを持つ分岐ノード b を考える。P を b を通るすべての端から端へのパスの集合とする。P 内の任意のパス p は、b において n 本の出ていくエッジの一つを通る。これは、p が b において n 本の出ていくエッジの一つを選ぶ選択をしているとみなせる。P 内のパス p1 と p2 を考える。i1 と i2（i1 ≠ i2）を、それぞれ p1 と p2 において b を越えた後に最初に出会う重要なノードとする。このような場合、p1 と p2 をそれぞれ異なる重要なノードへ導いた、b での選択をトレースに含めることが重要になりうる。パスが条件ノードを通る際に行う選択というこの概念を捉えるため、分岐ノードの出ていくエッジにラベルを付ける。具体的には、分岐ノード b の n 本の出ていくエッジに、それぞれ b1, b2 . . . bn というラベルを付ける。端から端へのパス p の条件付きトレースとは、p における重要なノードとラベル付きエッジの系列である。

条件付きトレースにすべてのラベル付きエッジを保持しても、有益でないことがある。例えば、分岐ノード b が、m を後続ノードとする単一後続部分グラフ S に含まれる場合を考える。このとき、P 内のすべてのパスは b と m の間に重要なノードを持たない。したがって、P 内のパス p にとって、p が b の後に通る重要なノードを決める上で、b での選択は無関係である。直観的には、ノード b と i1 の間の P 内のパスによって誘導される部分グラフ S は、P 内の任意の二つのパスのトレースを区別する上で無関係である。すなわち、P 内の任意の二つのパス p1 と p2 について、b で p1 と p2 が行う異なる選択は、それがどのような選択であっても、p1 ≢ p2 であるかを判定する上で無関係である。したがって、S に T4 を適用して S を i に吸収することは理にかなっている。より一般的な状況として、b が、u1 . . . uk が単一後続部分グラフ S に含まれるような k < n 本の出ていくエッジ e1 = (b, u1) . . . ek = (b, uk) を持つならば、e1 . . . ek の中から選ぶことは、P 内の任意の二つのパスのトレースを区別する上で無関係である。すなわち、e1 . . . ek は同じ選択を表す。S に T4 を適用すると、b から m への k 本の並行エッジが生じる。次に、これらの並行エッジに T2 を k − 1 回適用すると、b から m へのエッジは 1 本だけになり、これは k − 1 個の冗長な選択を取り除くことに相当する。したがって、いずれの場合も、すなわち b の出ていくエッジのすべて、またはその真部分集合の終点ノードが単一後続部分グラフ内にある場合、T2 と T4 の変換を組み合わせて適用することで、求める縮約が達成される。

1 具体的には、S は次のように定義される。P 内のパス p について、Vp を b から i までの部分パス（b と i を含む）のノードとする。すると、S は ∪p∈PVp によって誘導される部分グラフである。

これを動機として、G の条件付きトレース縮約形（CTRF）を、適用できなくなるまで G に T1 − T4 を繰り返し適用した後に得られるフローグラフと定義する。G の条件付きトレース内容は ΔcG で表し、G の CTRF における条件付きトレースの集合である。G が O(|G|2) 時間でその CTRF に縮約できることは容易にわかる。

3. 結びに

フローグラフは、ソフトウェアのコードにおけるソフトウェアの脆弱性と悪意ある振る舞いを解析するための汎用的な枠組みを与える。フローグラフの重要なノードは、ミューテックスオブジェクトのロック/アンロックや、メモリ位置での割り当て/解放といった、関心のあるイベントに対応する。フローグラフに対する解析は、これらの重要なノードがフローグラフのパスにどのように現れるかに関わる。フローグラフにおける重要なノードのこの順序付けは、フローグラフのトレース内容によって捉えられる。述べた変換は、トレース内容を保ったまま、フローグラフのサイズを、したがって解析時間を大きく縮小できる。例えば、我々はこれらの変換を Linux カーネルのソース（v2.6.31）における安全な同期の性質の検証に適用した。何らかの同期機構を用いる最大の 10 個の関数において、対応する制御フローグラフのノード数、エッジ数、パス数がそれぞれ 89.77%、87.28%、99.98% 削減されることを観測した。我々の結果が、静的なソフトウェア解析だけでなく、他の実世界の問題にも役立つことを願う。

参考文献

  1. F. E. Allen, Control flow analysis, SIGPLAN Not. 5 (7) (1970) 1–19.
  2. D. Bruschi, L. Martignoni, M. Monga, Detecting Self-mutating Malware Using Control-Flow Graph Matching, in: R. Buschkes, P. Laskov (Eds.), Detection of Intrusions and Malware & Vulnerability Assessment, vol. 4064 of Lecture Notes in Computer Science, Springer Berlin Heidelberg, 129–143, 2006.
  3. C. Lattner, V. Adve, LLVM: A compilation framework for lifelong program analysis & transformation, in: Code Generation and Optimization, 2004. CGO 2004. International Symposium on, IEEE, 75–86, 2004.
  4. Y. Zhou, X. Jiang, Dissecting Android Malware: Characterization and Evolution, in: Security and Privacy (SP), 2012 IEEE Symposium on, 95–109, 2012.
  5. M. Das, S. Lerner, M. Seigle, ESP: path-sensitive program verification in polynomial time, SIGPLAN Not. 37 (5) (2002) 57–68.
  6. T. H. Cormen, C. E. Leiserson, R. L. Rivest, C. Stein, Introduction to Algorithms (The Third Edition), The MIT Press, 2009.
  7. R. Tarjan, Depth-first search and linear graph algorithms, SIAM journal on computing 1 (2) (1972) 146–160.