Heap Cloning: Enabling Dynamic Symbolic Execution of Java Programs

Presentation on theme: "Heap Cloning: Enabling Dynamic Symbolic Execution of Java Programs"— Presentation transcript:

1 Heap Cloning: Enabling Dynamic Symbolic Execution of Java Programs
担当: S. Anand and M.J. Harrold, “Heap Cloning: Enabling Dynamic Symbolic Execution of Java Programs”, ASE 2011, Lawrence, KS, USA.

2 背景 Symbolic exection DSE: Dynamic symbolic execution プログラム解析の技術
記号を入力して解釈実行し path constraints を算出 実行できないプログラム native methods や library classes の存在 DSE: Dynamic symbolic execution Concolic exection 具体的な値を用いた実行と記号実行の併用 記号実行できない箇所を補う

3 DSEの問題 記号実行できないプログラム 記号実行系の実現の難しさ
native methods, standard library classes 副作用により具体的な実行結果と記号実行の結果に差異が生じる 手動で解析用モデルを補うことで対処 記号実行系の実現の難しさ 記号実行用インタプリタとJVMとの不親和 命令の置換え実行をするアプローチでもライブラリがうまく扱えず、精度が落ちる

4 Heap Cloning 目的: 提案: 解析用のモデルを追加する手間を減らしたい 既存の手法の限界を打ち破る ヒープの二重化
本来の具体的な計算に用いるヒープ 記号計算用のヒープ 副作用がある native methods を特定 native method を呼び出したあとにヒープ間に差異が生じたら副作用あり Standard library classes を使わない

5 実現方法 プログラムを書換える ヒープの二重化 Standard library classes を使わないようにする
直感的には、すべてのオブジェクトのラッパーを作る Standard library classes を使わないようにする S. Anand and M.J. Harrold, “Heap Cloning: Enabling Dynamic Symbolic Execution of Java Programs”, ASE 2011, Lawrence, KS, USA.

6 評価実験 実装: CINGER (Concolic INput GEneratoR) 実験:
対象: NanoXML, JLex, Sat4J(2 versions), BCEL, Lucene (約 12千〜57千行) テストケースを実行して path constraints を算出 ライブラリクラス内の実行で生じる制約を確認 BCEL の場合、約 90% 命令を置き換える方法で精度の向上に貢献できる モデル化すべき native method の特定 56 個中 1 個 (arraycopy in java.lang.system)

7 Automatic Generation of Load Tests
担当: P. Zhang, S. Elbaum, and M. B. Dwyer, “Automatic Generation of Load Tests”, ASE 2011, Lawrence, KS, USA.

8 背景 Load Test: 極端な負荷の下で，システムの性能が許容できるかどうか検証する 既存のLoad Test生成方法の限界
特定の値に依存 入力サイズを増やすとコスト増 入力サイズを増やしても同じ計算ばかり増える 応答時間やスループット以外の評価基準を扱えない メモリや消費電力

9 提案方法 単に入力サイズを増やすのではなく， 注意深くデータを選ぶ プログラムの振舞いの多様性(diversity)をカバー
複数の評価基準に対応 記号実行を用いてプログラムパスを探索してテスト生成

10 direct and incremental SE
テスタのすること 　(1) 記号として扱う変数を指定 　(2) 生成するテスト数を指定 　　　(testSuitSize) 　(3) 基準を選択(measure) 　　　応答時間，消費メモリ 　さらに，1フェイズの分岐の数を 　指定 (lookAhead) 共通のノードの距離が lookAhead/testSuitSize以上 testSuitSize=2, lookAhead=6

11 評価 応答時間 (左の図) JZlibを使って比較(ランダムデータ) 2倍の差 記号実行の最大分岐数を100に すれば100MBまで生成可能
2. 消費メモリ SAT4Jを使って比較(ベンチマーク) 　1.2倍から3.7倍の増加 3. 複数(応答時間と消費メモリ) (左の表) 　TinySQLを使って比較 応答時間も消費メモリも約2倍増加 　テストケースの多様性も十分

12 Symbolic Search-Based Testing
担当: A. Baars, M. Harman and et al. , “Symbolic Search-Based Testing”, ASE 2011, Lawrence, KS, USA.

13 背景と提案 Search Based Software Testing Symbolic Search-Based Testing
テストデータの自動生成 生成時の基準: Branch coverage テストデータの探索アルゴリズムは研究されているが、fitness function は古いまま Symbolic Search-Based Testing Fitness function の改善 Partial symbolic execution による静的解析 精度に関する尺度の導入

14 Symbolically Enhanced Fitness Function
目的の経路からそれた分岐で評価 従来: 2 つのパラメタの和 branch distance (分岐条件と距離) 例: x > 0 ⇒ |x – 0| + K (K is a failure constant. K=1) approach level (目標分岐条件までの距離) 提案: 目的の分岐までの各経路で2つのパラメタの和を求め、その最小値 path distance (branch distance の総和) approximation level (ループの存在による記号実行の不正確さ)

15 Approximation Level 分岐 2 から 8 まで ループの存在 s, i の値は正しく計算できない
Path condition: < n > 0 ∧ 0 < n ∧ a = n > approximation level: 3 1 ≧ n, s = 10, b = s

16 評価実験 前提: RQ1: branch coverage に負の影響がない？ RQ2: 効率が向上する？ 探索方法:
[local search] Alternating Variable Method (AVM) [global search] Generic Algorithm (GA) 対象: 複数のC言語のプログラム, 分岐数 338 RQ1: branch coverage に負の影響がない？ 結果: 同じか coverage を上げる 探索の成功率も高める傾向 ただし、オーバーフロー等の検査があると成功率が下がる RQ2: 効率が向上する？ AVM: 最大で約 90% の評価回数を削減 GA:最大で約 30% の評価回数を削減