充足可能性判定を利用した モデル検査 土屋達弘 (大阪大学)

モデル検査とは 形式的検証手法 入力: 設計 + 特性 (仕様) 出力: Yes or No 方法: 状態探索 モデル検査器 状態機械 設計 2007 Turing Award　(Clarke, Emerson, Sifakis)  入力: 設計 + 特性 (仕様) 出力: Yes or No 方法: 状態探索 モデル検査器 状態機械 設計 Yes No (＋反例) 特性 (仕様)

簡単な歴史 1980頃 1990年代 1998～ 2000年代中～後 最初の研究成果 Partial Order Reduction -> SPIN BDD (2分決定グラフ) -> SMV 1998～ SAT (充足可能性判定) 2000年代中～後 SMT 記号モデル検査 状態機械を記号的に表現・操作 今回のトピック

日本語でよめる記号モデル検査 関連の文献 米田，梶原，土屋，ディペンダブルシステム， 共立出版，2005. 電子情報通信学会ハンドブック／知識ベース， ７群１編「ソフトウェア基礎」 土屋，菊野，”モデル検査入門,” 計測と制御，2009. 土屋，菊野，”記号モデル検査の並行ソフトウェアシステムへの応用,”第17 回回路とシステム軽井沢ワークショップ，2004.

Part I 逐次プログラムのモデル検査

充足可能性判定問題 (拡張版) 入力：ブール値をもつ式 出力：Yes or No 条件：Yes の必要十分条件は， 式をTrueにする変数への値の割り当て (付値 valuation)が存在すること 例． 入力: x, y  Z, (x + y > 2)  ((x < 3)  (y < 2)) 出力: Yes (付値の例 x = 2, y = 1)

逐次プログラムの検証例 (1/2) assume(x0 + y0 > 2); assume(x + y > 2); if (b) x = x +1; else x = x + 2; y = y + x; x = y + 1; assert(x < 2); assume(x0 + y0 > 2); if (b0) x1 = x0 +1; else x2 = x1 + 2; y1 = y0 + x2; x3 = y1 + 1; assert(x3 < 2); 設計 特性 1変数は1度しか更新されないように変数の名前を付けかえる

逐次プログラムの検証例 (2/2)  y0 + x0 > 2   b0  x1 = x0 +1  b0  x1 = x0  y1 = y0 + x2  x3 = y1 + 1  (x3 < 2) assume(x0 + y0 > 2); if (b0) x1 = x0 +1; else x2 = x1 + 2; y1 = y0 + x2; x3 = y1 + 1; assert(x3 < 2); 充足可能　⇔ 言明を満たさない実行が存在

充足可能性判定の実行 SAT/SMT Solverを利用 一定の長さの実行を検査 有界(Bounded)モデル検査 % cat sample.txt (define b0::bool) (define x0::int) (define x1::int) (define x2::int) (define x3::int) (define y0::int) (define y1::int) (assert (and (> (+ y0 x0) 2) (or (and b0 (= x1 (+ x0 1))) (and (not b0) (= x1 x0)) ) (and (not b0) (= x2 (+ x1 2))) (and b0 (= x2 x1)) (= y1 (+ y0 x2)) (= x3 (+ y1 1)) (not (< x3 2)) (check) % yices –e sample.txt SAT/SMT Solverを利用 例．Yices @ SRI 一定の長さの実行を検査 有界(Bounded)モデル検査  y0 + x0 > 2   b0  x1 = x0 +1  b0  x1 = x0  b0  x2 = x1 + 2  b0  x2 = x1  y1 = y0 + x2  x3 = y1 + 1  (x3 < 2)

Presburger Arithmetic 式の表現力 計算量 NP完全 SAT solvers ブール式 Separation Formula O. Strichman et al., “Deciding Separation Formulas with SAT,” CAV 2002. 整数か実数（一方のみ），(x – y > c)の論理結合 ブール式 + 背景理論 SMT solvers 例．整数，実数，加減算大小比較 Presburger Arithmetic 計算量O(22^n) ツール例．Omega Library 整数，加減算，限量子(一階) ディオファントス方程式 決定不能

SAT Solver SMT (Satisfiability Modulo Theories) Solver 高速なヒューリステックアルゴリズム MiniSAT, Zchaff, Grasp, … ブール式以外の変数の表現 複数のブール変数からなるビットベクトル SMT Solver: 「ブール式＋背景理論」を扱う Yices, CVC3, Z3,… 種々の背景理論 （組み合わせても良い） 配列，Linear Arithmetic (整数and/or実数の加減算大小比較)，ビットベクトル

逐次プログラムのモデル検査 CBMCでの手順 CBMC: ANSI C Model Checker　(SATを利用) E. Clarke et al., “A tool for checking ANSI-C programs,” TACAS 2004. ネストしたループの解消 ループの削除 変数のRenaming 論理式への変換 他の方法も大体同じ A. Armando et al., “Bounded model checking of software using SMT solvers instead of SAT solvers,” J. Softw. Tools & Technol. Transfer, 2009. if, if-else のみに変換

1. ネストしたループの解消 ループの展開（手順2）でのプログラムのBlow upを避ける 仮想的なプログラムカウンタ (vpc) を導入 while (vpc <= 2) { switch (vpc) { case 1: if (B1) { S1; vpc = 2; } else vpc = 3; break; case 2: if (B2) S2 else vpc=1; } while (B1) { S1; while (B2) { S2; }

2. ループの削除 ループを展開 最大何回展開するかはユーザが入力 例．繰り返しが最大3回の場合 for, 後ろ向きのgoto,関数の再帰呼び出しも同様に変換 if (b) { S; assert(!b); } while (b) { S; } 最後はassert(!条件)に置き換える →　ループが指定回数以上実行される可能性を検出

変数のRenamingと論理式への変換 静的単一代入(SSA)とほぼ同じ x = x + y; if (x != 1) { x = 2; if (z) x++; } assert(x<=3); x1 = x0 + y0; if (x1 != 1) { x2 = 2; if (z0) x3 =x2 + 1; } assert(x3<=3); x1 = x0 + y0  x2 = ite(x1  1, 2, x1)  x3 = ite(x1  1  z0, x2 + 1, x2)  (x3  3)

論理式への変換 SATの場合 ー CNF (Conjunctive Normal Form)のブール式に変換 SMTの場合 変数: 複数のブール変数によるベクトル 演算(+,-,*,/など）: 演算回路 任意のブール式は，充足可能性を保存して線形の大きさのCNFに変換可能 SMTの場合 1プログラム変数を1変数で表現可能 背景理論：ビットベクトル 背景理論：Linear Arithmetic (上限のない整数,実数変数)

SAT vs. SMT SMTが優れる場合 背景理論によって式がコンパクトになる場合 例．配列を多用する場合 Primのアルゴリズム (最小スパニング木の計算, 4ノード) 時間(sec) 辺の数 A. Armando et al., “Bounded model checking of software using SMT solvers instead of SAT solvers,” J. Softw. Tools & Technol. Transfer, 2009.

適用事例 ANSI C の検証 PHPプログラムの脆弱性検出 CBMC @CMU @National Taiwan Univ. E. Clarke et al., “A tool for checking ANSI-C programs,” TACAS 2004. PHPプログラムの脆弱性検出 @National Taiwan Univ. Y.W. Huang et al., “Verifying web applications using bounded model checking,” DSN 2004.

Part II 並行システムのモデル検査

並行システム モデル検査の主たる対象 通常は停止しない (リアクティブシステム) 検証の関心 モデル検査問題の入力 アルゴリズム (cf. 実際のコード) 制御に関する正しさ (cf. データ) モデル検査問題の入力 設計：アルゴリズム 性質 (仕様)：時相論理 (ex. LTL, CTL) 有界モデル検査ではLTLを扱う

例．相互排除（２つの並行プロセス） 設計 状態：(pc0, pc1, t) 特性 (時相論理LTL, G：「常に」，F: 「いつか」) 0,0,0 0,1,0 1,1,0 2,0,0 2,1,0 1,0,0 0,1,1 0,2,1 1,1,1 1,2,1 0,0,1 1,0,1 P0:: 0: while True { 1: wait (t = 0) 2: t = 1;}　// CS P1:: 1: wait (t = 1) 2: t = 0;} // CS 特性 (時相論理LTL, G：「常に」，F: 「いつか」) 相互排除 G¬((pc0 = 2)(pc1 = 2)) スタベーションフリー(P0側) G(pc0 = 1→Fpc0 = 2) Yes No!

システムの記号表現 ー 記号モデル検査の基礎 状態：(pc0, pc1, t) システムの数学的表現 形式的な仕様記述にも有用 TLA, TLA+ (by Lamport) 状態とは？ グラフ表現:頂点 記号表現:変数への付値 例．pc0 = 0, pc1 = 2, t = 1 遷移とは？ グラフ表現:辺　 記号表現:変数とそのコピーへの付値 例．pc0 = 0, pc1 = 2, t = 1, pc‘0 = 1, pc‘1 = 2, t‘ = 1 0,0,0 0,1,0 1,1,0 2,0,0 2,1,0 1,0,0 0,1,1 0,2,1 1,1,1 1,2,1 0,0,1 1,0,1

記号表現：状態集合 状態集合S 例．初期状態集合 S = True  sS が付値 P0:: 0: while True { 1: wait (t = 0) 2: t = 1;}　// CS P1:: 1: wait (t = 1) 2: t = 0;} // CS 状態集合S S = True  sS が付値 状態集合とその記号表現を同一視 例．初期状態集合 I = {(pc0,pc1, t)=(0, 0, 0), (0, 0, 1)} 記号表現 I := pc0=0  pc1=0 0,0,0 0,1,0 1,1,0 2,0,0 2,1,0 1,0,0 0,1,1 0,2,1 1,1,1 1,2,1 0,0,1 1,0,1

記号表現：遷移関係 遷移関係T (遷移の集合) 例．P0の0行 遷移関係全体 変数とそれらのコピー上の論理式 0: while True { 1: wait (t = 0) 2: t = 1;}　// CS P1:: 1: wait (t = 1) 2: t = 0;} // CS 遷移関係T　(遷移の集合) 変数とそれらのコピー上の論理式 T = True  (s, s’)T が付値 例．P0の0行 G1 := pc0=0 T1 := G1 pc’0=1  pc’1=pc1 t’ =t 遷移関係全体 T :=T1T2… Tn  ¬(G1 … Gn )pc’0=pc0pc’1=pc1t’=t 0,0,0 0,1,0 1,1,0 2,0,0 2,1,0 1,0,0 0,1,1 0,2,1 1,1,1 1,2,1 0,0,1 1,0,1 実行できる命令がないなら「次状態 = 現状態」 記号表現は設計から直接得られる　(状態探索は不要) (むしろ設計そのもの)

記号表現: システム システム＝状態機械 3要素によりシステムの動作を完全に記述 記号表現のメリット ・・・ 記号モデル検査 変数の集合 (状態空間を規定) 初期状態集合I 遷移関係T 3要素によりシステムの動作を完全に記述 記号表現のメリット　・・・　記号モデル検査 BDDを用いたモデル検査 (1990年ころ) Burch et al., “Symbolic model checking: 1020 states and beyond,” LICS 1990. SATを用いたモデル検査 (1999年ころ) A. Biere et al., “Symbolic model checking without BDDs,” TACAS 1999.

有界モデル検査 (SATを利用) 初期状態からk回の状態遷移を検査 例：到達可能性の判定 I(0)  T(0,1)  …  T(k-1,k)  (P(0)…P(k)) が充足可能 ⇒ Pが成り立つ状態に到達 I(0): Iの各変数varをvar0に置き換え T(i, i+1):Tの各変数varをvariに, var’をvari+1に置き換え 検査する特性としては，任意のLTL式を扱える

例． I := x = 1 T := (x  3  x’ = x + 1)  (x > 3  x’ = x) I(0)  T(0,1)  …  T(k-1,k)  (P(0)…P(k)) =  x0 =1  (x0  3  x1 = x0 + 1)  (x0 >3  x1 = x0)  (x1  3  x2 = x1 + 1)  (x1 >3  x2 = x1) …  (xk-1  3  xk = xk-1 + 1)  (xk-1>3  xk = xk-1)  (P(x0) … P(xk)) 充足可能 ⇒ Pが成り立つ状態に到達

手法の完全性 充足不能の場合 「Pが成り立つ状態に到達しない」とは結論できない kを増やすと充足するかもしれない 直径を知るのに手間がかかる kが大きくなると時間が増加する for (k = 0, 1, 2, 3, …) { res <- Sat(I(0)  T(0,1)  …  T(k-1,k)  P(k)); if (res = True) return “reachable”; }

狭義の記号モデル検査 (BDD (2分決定グラフ)を利用) 高速な演算処理アルゴリズムが存在 ハードウェアの場合，システムの構造に規則性があることが多く，対応するBDDが非常に小さくなることが多い． 状態集合と遷移関係を表すBDDをつかって， 状態の幅優先探索が可能 検証の完全性 代表的なモデル検査ツール SMV　(@CMU) NuSMV SATを使う有界モデル検査も実装 f(x, y) = x ¬x y x 1 y 1 1

有界モデル検査の長短 長所 短所 初期状態に近い状態を効率良く検証 充足する場合は速い （Bug Huntingに効果的） 時間がかかる 完全な検証のためには大きなkが必要 式が大きくなり時間がかかるため検証が困難 十分なkを知るのが困難

Part III 有界から無界へ

無界モデル検査 Unbounded Model Checking 有界から無界へ 検査する範囲を状態空間全体に拡張 K-Induction L. de Moura et al., “Bounded Model Checking and Induction: From Refutation to Verification,” CAV 2003. Craig’s Interpolant ✔

K-Induction 目的: 性質Vが常に成立するか否かを判定 手法:以下の2条件を示す SALモデル検査器でサポート 初期状態からのk状態で性質Vが常になりたつ I(0) T(0,1) …T(k-2,k-1)  (V(0) … V(k-1)) が充足不能 連続するk状態で性質Vが成り立っているなら， k+1番目の状態でもVが成り立っている V(0) … V(k-1)  T(0,1)  … T(k-1,k)  V(k) が充足不能 1, 2 ⇒ Vが常になりたつ SALモデル検査器でサポート

適用事例：コンセンサスアルゴリズムのモデル検査 耐故障分散アルゴリズムの一種 Paxos (by Lamport) Chubby lock system @ Google Practical Byzantine Fault Tolerance (by Castro & Liskov) 全ノードを同じ決定にみちびく 各ノードが値を提案 全ノードが同じ提案値を選択・決定

コンセンサスアルゴリズムの特徴 全プロセスが決定するまで無期限にラウンドをくりかえす 検証では無限のラウンドを扱わなければならない メッセージの遅延，故障に耐えるため 検証では無限のラウンドを扱わなければならない 手法1: 有限状態への抽象化 (SRDS 2007) 手法2: K-Induction (DISC 2008) u1:= 1 v1,0 Ack v1 P1 e1:= v1 u1:= 0 v1 Ack v2,0 r1:= 1 P2 e2:= v2 e2:= v1 u2:= 0 v3,0 u2:= 1 v1 Ack r2:= 1 P3 e3:= v3 e3:= v1 u3:= 0 u3:= 1 r3:= 1

実験結果 (The LastVoting/Paxos Algorithm) 実行時間 (sec) SPIN ALV 手法１． 通常のモデル検査(NuSMV) + 有限状態への抽象化 手法2. SMT (Yices) + K-Induction ノード数

無界モデル検査 Unbounded Model Checking 有界から無界へ K-Induction Craig’s Interpolant K. McMillan, “Interpolation and SAT-Based Model Checking,” CAV 2003. ✔

Craig’s Interpolant F  Gが充足不能な場合， FとGのInterpolant IP が存在 例 F ⇒ IP IP  G は充足不能 IPの変数は FとGに共通 例 F := p  q, G := : q  r  s, Ip := q

Interpolantによる状態探索 (Pへの可到性) k = 0からスタート I(0)  T(0,1)  …  T(k-1,k)  P(k) 充足可能: 「Reachable」 充足不能: kステップ目の状態ではPは成り立たない F:= I(0)T(0,1), G:=T(1,2) …T(k-1,k)  P(k), IP := FとGのInterpolant 　IPはIから1ステップで行ける状態集合のOverapproximation F ⇒ IP IP  G は充足不能 IPの変数は FとGに共通 1ステップ後の状態 I

Interpolantによる状態探索 R <- I  IP R(0)  T(0,1)  …  T(k-1,k)  P(k) 充足不能: 手順4へ． F:= R(0)T(0,1), G:=T(1,2) …T(k-1,k)  P(k), IP := FとGのInterpolant R <- R  IP Rが変化しない: 「到達しない」 Rが増加：手順3へ． R Rから 1ステップ後の状態

適用例 電話通信サービスの競合問題検出 提案手法 従来法1 従来法2 電話通信サービス向きの記号表現 T. Matsuo et al., “Feature Interaction Verification Using Unbounded Model Checking with Interpolation,” IEICE Trans. Info & Syst, 2009. 提案手法 電話通信サービス向きの記号表現 Interpolant (ツールFOCI) 従来法1 Interpolant (ツールFOCI) + 通常の記号表現 従来法2 Spin (状態グラフを扱うモデル検査ツール)

実験結果 競合あり = 充足する場合: 提案手法は高速 充足しない場合: Spinの方が速い

Part IV まとめ

まとめ SAT/SMTソルバを利用したモデル検査 逐次プログラム 並行システム 非界モデル検査