形式手法特論：CEGAR を用いたモデル検査の状態空間削減 #kernelvm / Kernel VM Study Hokuriku Part 8

Kernel/VM 探検隊@北陸 Part 8 で使用したスライドです。

モデル検査は形式手法の一種であり、システムやプログラムを Kripke 構造と呼ばれるグラフに変換し、与えられた仕様に反した状態に到達しないことを網羅的・自動的に検査する技術です。全自動でシステマティックに検査が可能である点では有望ですが、同時に、現実的なプログラムをモデル検査にかけようとすると状態数の爆発が問題となり、産業界への普及の障害の一つとなっていました。

この問題に対して、Clarke らによって 2000 年に提案された手法が CEGAR（CounterExample-Guided Abstraction Refinement）です。

https://doi.org/10.1007/10722167_15

CEGAR ではまず、プログラムの動作を変えないように変数の振る舞いを抽象化（abstraction）することで、検査対象となるグラフを単純化し状態数を削減します。このとき、抽象化したグラフで反例が検出できなければ、元となるグラフにも反例は存在しません。しかし逆は成り立たず、元となるグラフに反例が存在しないにも関わらず、抽象化したことによって新たに反例が生じることがあります。このような反例を偽反例（spurious counterexample）と呼びます。

そこで CEGAR では次の段階として、詳細化（refinement）を行います。具体的には、抽象化された側で見つかった（偽反例の可能性がある）反例に対して、元の問題の側に引き戻して考え、もし元のグラフとは両立し得ない場合は偽反例と判断します。その場合、偽反例の元となっている過剰な抽象化を特定し、抽象化を緩め、この手続を繰り返すことで、元の構造をより正確に反映したグラフを得ることができます。

今回の講演では、シンプルなログイン処理を模した具体例を用いて、CAGAR の抽象化 - 詳細化の処理の流れを図を使って解説しています。

Transcript

1. 形式手法特論 CEGAR を用いた モデル検査の状態空間削減 #kernelvm チェシャ猫 (@y_taka_23) Kernel/VM 探検隊@北陸 Part 8 (6th Dec. 2025)
2. クリスマスといえば状態遷移図
3. 例：ログイン処理の状態遷移 • 4 個の Bool 変数フラグからなる系 ◦ loggedIn：ログインセッションが有効 ◦ trusted：デバイスが信頼済み ◦ redirect：ログイン画面へのリダイレクトフラグ ◦ locked：アカウントがロック状態 • 検査したい仕様「locked ならば必ず redirect」
5. 初期状態 ロックされていない場合 “*” は非決定選択 ログイン成功 ログイン失敗 アカウントロック発動 既にロックされている場合
6. FFTF スペースの節約のため、各変数の値を記号で略記
7. TTTT FTTT TTFT FTFT TFTT FFTT TFFT FFFT TTTF FTTF TTFF FTFF TFTF FFTF TFFF FFFF
8. TTTT FTTT TTFT FTFT TFTT FFTT TFFT FFFT TTTF FTTF TTFF FTFF TFTF FFTF TFFF FFFF 仕様 locked -> redirect に対する違反
9. TTTT FTTT TTFT FTFT TFTT FFTT TFFT FFFT TTTF FTTF TTFF FTFF TFTF FFTF TFFF FFFF
10. モデル検査と状態爆発 • モデル検査は一種のグラフ探索問題 ◦ プログラムやシステムを状態遷移で表現 ◦ 初期状態から違反状態へ至るパスの有無を探索 • 状態数の爆発が問題になる ◦ プログラムをそのまま検査するのは非現実的 ◦ どうにかして状態数を削減して最適化したい
11. CEGAR CounterExample-Guided Abstraction Refinement
12. 抽象化（Abstraction） • 状態遷移系を粗く近似 ◦ if 文や検査仕様に影響しない変数は一旦忘れる ◦ 状態が区別できず「潰れる」部分ができる ◦ 元のグラフより小さく単純なグラフができる • 単純化されたグラフに対し再度モデル検査 ◦ 仕様の反例（違反状態へのパス）の有無を確認
13. 抽象化の健全性 特定のタイプの仕様（今回は詳細略）については、 抽象化された状態遷移系において反例が検出できない場合、 元の状態遷移系でも反例は存在しない。 定理（Clarke et al. 2000） https://doi.org/10.1007/10722167_15
14. locked locked -> redirect TTTT T T TFTT T T FTTT T T FFTT T T TTFT T F TFFT T F FTFT T F FFFT T F locked locked -> redirect TTTF F T TFTF F T FTTF F T FFTF F T TTFF F T TFFF F T FTFF F T FFFF F T
15. locked locked -> redirect TTTT T T TFTT T T FTTT T T FFTT T T TTFT T F TFFT T F FTFT T F FFFT T F locked locked -> redirect TTTF F T TFTF F T FTTF F T FFTF F T TTFF F T TFFF F T FTFF F T FFFF F T
16. TTTT FTTT TTFT FTFT TFTT FFTT TFFT FFFT TTTF FTTF TTFF FTFF TFTF FFTF TFFF FFFF
17. **TT **FT **TF **FF
18. 16 状態から 4 状態に削減！
19. **TT **FT **TF **FF
20. （いや反例あるやんけ）
21. TTTT FTTT TTFT FTFT TFTT FFTT TFFT FFFT TTTF FTTF TTFF FTFF TFTF FFTF TFFF FFFF
22. 詳細化（Refinement） • 抽象化により偽の（spurious）反例が生じることがある ◦ つまり先ほどの定理の「逆」は成立しない ◦ 元のグラフ側で再現できない反例パスは偽反例 ◦ 状態を粗く潰しすぎてしまっている • 抽象化で消えた情報を部分的に復元し、偽反例を排除 ◦ 潰しすぎた状態を分離できるような変数を思い出す
23. **TT TTTT FTTT FFTT TFTT 初期状態 違反状態 抽象化のせいで本来は繋がっていないはずの 偽反例パスが繋がって見える
24. *FTT **TT TTTT FTTT FFTT TFTT *TTT TTTT FTTT FFTT TFTT 初期状態 違反状態 初期状態 違反状態 trusted（二つ目の変数）で詳細化しても 偽反例パスの原因となっている状態が分離できない
25. **TT TTTT FTTT FFTT TFTT 初期状態 違反状態 初期状態 違反状態 loggedIn（一つ目の変数）で詳細化すれば 偽反例パスの原因となっている状態が分離できる T*TT TTTT FTTT FFTT TFTT F*TT
26. **TT **FT **TF **FF
27. T*TT F*TT T*FT F*FT T*TF F*TF T*FF F*FF
28. 最終的に 8 状態のモデル検査に帰着 反例なしで確定！
29. まとめ：CEGAR による効率化 • モデル検査はグラフ上で違反状態を探索する問題 ◦ 状態数の爆発が問題になる • 一部の変数を忘れることで状態を潰して抽象化 ◦ 抽象化した状態で反例が見つからなければ OK • 偽反例が出た場合、それをヒントに状態を詳細化 ◦ 潰しすぎた状態を分離するような変数を思い出す
30. Harness Counterexamples to Counterpunch! Presented By チェシャ猫 (@y_taka_23)