Observable modified Condition/Decision coverage

Presentation on theme: "Observable modified Condition/Decision coverage"— Presentation transcript:

1 Observable modified Condition/Decision coverage
Session:B1

2 概要 背景 問題点 解決策(OMC/DC) テストを評価する指標として有効なMC/DCというC2カバレッジがある
Session:B1

3 MC/DCの問題点 MC/DCを100%にするテストでも内部状態の変化が隠れてしまうとバグを発見できない e1 = i1 or i2
o1 = e1 and i3 100%MC/DCテスト test i1 i2 i3 o1 1 T F 2 3 4 以下の様に2つのinput, i1とi2が中間変数e1をへて外部に影響する場合を考えてみます。 左下に4つのテストケースがあり、これでMC/DCは100%になるんですが、例えばtest1とtest2をみてみると I1の変化がo1に伝わっていません。このように本来伝わるべきはずの変化が伝わらないので、全てのテストケースに 対して結果が同じになり、バグを発見できないことになります。 e1 = i1 and i2 o1’ = e1 and i3 ※MC/DCとは？ ある条件の変化が独立に出力に影響するかどうかの指標 Session:B1

4 OMC/DCによる改善 MC/DCにオブザーバビリティという指標を追加することで内部状態の変化を出力に伝える e1 = i1 or i2
o1 = e1 and i3 100%OMC/DCテスト test i1 i2 i3 o1 1 T F 2 3 4 この基準に基づいて筆者達はテスト生成も行っているが、詳細は論文を読んでください e1 = i1 and i2 o1’ = e1 and i3 ※オブザーバビリティとは？ ある条件の全ての変化が独立に出力に影響するかどうかの指標 Session:B1

5 評価 基準 設定 対象 方法 バグ検出率 構造に対する堅牢性 手法：MC/DC or OMC/DC
第三者が作成した大小さまざまなプログラム5つ 方法 250個のバグを埋め込んでテスト Session:B1

6 バグ発見率 全てにおいて改善 特にNon-Inlined+Output-Only Non-Inlined Inlined DWM1 DWM2
Latctl Vertmax Microwave Non-Inlined OMC/DC Output-Only 91% 96% 95% 98% 93% MC/DC Output-Only 3% 77% 55% 41% 59% OMC/DC Maximum 100% 99% MC/DC Maximum 86% 92% 89% Inlined 88% 97% 82% 80% 73% Session:B1

7 構造に対する堅牢性 プログラムの構造が変わってもバグの発見率が変わらない Case Example Oracle OMC/DC MC/DC
DWM1 Output-Only -3 79 Maximum 13 DMW2 1 18 6 Latctl 2 37 Vertmax -2 39 3 Microwave 14 4 一般性が高い Session:B1

8 Billions and Billions of Constraints: Whitebox Fuzz Testing in Production
Ella Bounimova, Patrice Godefroid, David Molnar 概要 超大規模にwhitebox fuzzingを適用した結果の報告 大規模に長期間のテストを行うと問題が発生 Windows 7のバグの1/3を発見 こんにちは。東京大学本位田研究室の鈴木です。 本日はBillions and Billions of Constraints: Whitebox Fuzz Testing in Productionという論文の内容を発表いたします。 この論文は、Whitebox fuzzingというテスト入力自動生成手法を超大規模に運用した結果の報告論文です。 大規模かつ長期間に亘ってテストを走らせると様々な問題が発生します。 そこで、人間がそれらの問題を解決できるよう、テスト環境の監視と制御を支援するシステムを開発しました。 その結果、マイクロソフト社内において、2007年から2013年までの総計500マシン年に亘って大規模に運用することができ、バグを大量に発見することができました。 人間による監視と制御を支援するシステムを開発 マイクロソフト社内で500マシン年の規模で運用できバグを大量に発見

9 背景知識｜Whitebox fuzzing
ランダムに生成した入力を利用して 記号的実行を行う 記号的実行で収集された条件の一部 を反転して制約を生成する 生成された制約をソルバに解かせる ソルバが求めた解を新たな入力とし て1.に戻る 入力： x = 0 , y = -1 , y = 4 if x = 0 if x = 0 x = 0 x != 0 if y > 3 if y > 3 y > 3 y <= 3 背景知識としてwhitebox fuzzingについて説明します。 これは記号的実行とfuzzingを組み合わせたテスト入力の自動生成手法です。 制御フローグラフを深さ優先探索するように新たな入力を生成していきます。 まず、ランダムに生成された入力に沿って記号的実行を行い、パスを記憶しておきます。 例えば、入力としてx = 0, y = -1を与えると、最初の条件文はtrueですから左へ行き、次の条件文はfalseですから右へ行きます。 このようにして記号的実行のパスが得られます。 次にこの条件の一部を反転してこのような制約を作り、このパスを通るような入力をソルバに求めさせます。 解としてたとえばx = 0, y = 4が得られますから、これを新たな入力として同様の手順を繰り返します。 これがwhitebox fuzzingです。 a = x + y a = x + y 制約： x = 0 , !(y > 3) , y > 3

10 提案システム SAGAN JobCenter 運用中に発生する問題を人間が解決する必要 ⇒ 大量のマシンの監視・制御を支援するシステムを開発
SAGEからのログを収集するシステム JobCenter SAGEを中央からコントロールするシステム このwhitebox fuzzingを大規模かつ長期間に亘って運用すると、当然のことながら様々な問題が発生します。 それらの問題を解決するために大量のマシンからなるテスト環境の監視と制御を支援するシステムが必要になります。 ここではwhitebox fuzzingツールSAGEからのログを収集するSAGANと、SAGEを中央からコントロールするJobCenterという二つのシステムを開発しました。 共著者らが提案したWhitebox fuzzingツール

11 提案システムによる運用 長期間の運用が可能に （台） （台） （台） （日） （日） （日）
その結果長期間の運用が可能になり、バグの発見に大きく寄与しました。 ここでは運用結果の一例としてSAGEの稼働台数に関する統計を紹介します。 このグラフは横軸が日数で、縦軸がSAGEの稼働台数です。 1番目のセットでは稼働期間が長くなるとエラーによりどんどんSAGEが落ちていきますが、 提案システムによって収集されたログの分析とチューニングを行うことで、 テ落ちるSAGEの割合が少なくなり、バグの発見に寄与しています。 その他にも収集されたログを分析することで記号的実行を補完したり制約を枝狩りしたりなどが可能になっています。 （日） （日） （日） 分析とチューニングを挟んで3セット実行した時の台数の遷移の比較（横軸：日数、縦軸：台数）