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.

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

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

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

実現方法 プログラムを書換える ヒープの二重化 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.

評価実験 実装: 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)

Automatic Generation of Load Tests 担当: 蜂巣@南山大学 P. Zhang, S. Elbaum, and M. B. Dwyer, “Automatic Generation of Load Tests”, ASE 2011, Lawrence, KS, USA.

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

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

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

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

Symbolic Search-Based Testing 担当: 吉田@南山大学 A. Baars, M. Harman and et al. , “Symbolic Search-Based Testing”, ASE 2011, Lawrence, KS, USA.

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

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 (ループの存在による記号実行の不正確さ)

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

評価実験 前提: 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% の評価回数を削減