Model checking of hyperproperties for high-level relational models

技術的概要：高レベル関係モデルに対するハイパープロパティのモデル検査

問題定義
多くの重要なシステム特性、特にセキュリティ（例：ノンインターフェアランス、一般化されたノンインターフェアランス）や並行性（例：リニアライザビリティ）に関する特性は、ハイパープロパティです。単一の実行について推論する従来のトレース特性とは異なり、ハイパープロパティは複数の実行トレース間の関係について推論する必要があります。ハイパーロジック（HyperLTL など）のモデルチェッカーを生成する最近の進展にもかかわらず、これらのツールは通常、低レベルで機械可読な形式（例：SMV フラグメント、オートマトン）で動作します。これにより、ソフトウェア工学の実務者にとって大きなギャップが生じています。すなわち、システム設計を自然にモデル化しつつ、ハイパープロパティの自動検証をサポートする高レベル仕様言語が不足しているという点です。既存のツールは、高レベルの概念を手動で低レベルの状態機械に変換するか、解釈が困難な形式（例：生の QBF 出力）で反例を提供することを要求することが多いです。

手法
著者は、関係モデル上のハイパープロパティの自動検証をサポートするために、Alloy 言語の時間論理バックエンドであるPardinusを拡張したモデル発見手続きHyperPardinusを提案します。このアプローチは、2 フェーズのパイプラインから構成されます。

1. 高レベルモデリングと変換（HyperPardinus）:

   • 著者は、Alloy 6言語への最小限の拡張を導入し、シグネチャに trace キーワードを追加しました。これにより、シグネチャは実行トレースを表すようになり、単一の仕様内で複数のトレースに対する量化が可能になります。
   • HyperPardinus は、ハイパー関係モデル発見問題を形式化します。高レベルの Alloy 仕様を受け取り、それを一連の低レベル SMV（Symbolic Model Verifier）状態機械と HyperLTL 式に変換します。
   • 変換アルゴリズムは、関係時間論理の制約を前束標準形に変換し、トレース量化子を非ハイパー部分から分離します。各量化されたトレースに対して SMV モデルを生成し、これらのモデル上でハイパープロパティを HyperLTL 式としてエンコードします。
   • 変換中には、量化子の合成（同じタイプの逐次量化子をマージしてトレース数を削減）、多重度制約の活用（ブール符号化の代わりに整数変数を使用し状態空間を削減）、対称性の破れなどの主要な最適化が適用されます。

2. 低レベル検証（HyperSMV）:

   • 生成された SMV モデルと HyperLTL 式は、高レベル Alloy 変換の固有の課題を処理するように設計された新しいモデルチェッカーHyperSMVによって処理されます。
   • HyperSMV は 2 つのバックエンドをサポートします。
     • 明示状態（Exp）: SMV モデルを明示状態システム（非決定性 Büchi オートマトン）に変換し、オートマトンベースのソルバー（例：AutoHyper, forklift, ROLL）を使用します。式の圧縮と双対性簡約のための最適化が含まれています。
     • 記号的（Sym）: アンローリング技術を用いてモデルと式を量化付きブール式（QBF）に変換し、市販の QBF ソルバー（例：Quabs, qute）を活用します。
   • HyperSMV の重要な機能は、証跡のバックトレース能力です。ソルバーの出力（通常は低レベルのトレースまたは QBF 割り当て）を、読みやすい SMV トレースに変換し、最終的に Alloy Analyzer によって可視化される高レベル関係インスタンスに変換します。

主要な貢献

• HyperPardinus: 一階ハイパーロジックのための最初のモデルチェッカーです。Alloy エコシステムを拡張し、柔軟なトレース量化子の交互を含むハイパープロパティの仕様と自動検証をサポートします。
• HyperSMV: 明示状態および記号的な最先端ソルバーの両方と統合される堅牢な SMV モデルチェッカーです。サポートされる SMV モデルの表現力（宣言的スタイルや整数変数の処理）と検証プロセスのスケーラビリティを大幅に向上させます。
• Alloy 拡張: Alloy 6 への最小限の、後方互換性のある拡張により、ユーザーは宣言的にハイパープロパティを指定し、高レベルの抽象度で反例を可視化できます。
• 評価: 会議管理システム（CMS）、ロボットの経路合成、変異テスト、並行データ構造（SNARK）のリニアライザビリティなど、多様なベンチマークを用いた包括的な評価。

結果
評価は、実現可能性、使いやすさ、最適化の有効性、およびパフォーマンスに関する 4 つの研究質問に答えています。

• 表現力と使いやすさ: このアプローチは、高レベルの Alloy で複雑なハイパープロパティ（例：リニアライザビリティ、ノンインターフェアランス）のモデリングに成功しました。著者は、Alloy モデルが、生成に広範なスクリプトを必要とすることが多い低レベルの SMV 対応物よりもはるかに読みやすく保守可能であることを実証しています。
• 反例の可視化: 生の QBF 出力や低レベルの SMV トレースを提供する既存のツールとは異なり、HyperPardinus は、Alloy Analyzer 内で可視化される最小限の高レベル関係反例を提供します。例えば、SNARK ベンチマークでは、このツールはバグを特定し、9 状態のグラフィカルなインスタンスを提供しましたが、最先端のツールは広範囲で読み取り不可能なトレースを生成しました。
• 最適化の影響: HyperPardinus の最適化（量化子の合成、対称性の破れ、多重度制約）は、明示状態バックエンドの実現可能性にとって決定的でした。これらなしでは、多くのモデル（例：CMS 変種、ロボット例）がタイムアウトするか、状態機械の生成に失敗しました。
• パフォーマンス:
  • 高レベルモデル: HyperSMV は、高レベル Alloy モデルにおいて最先端のツール（AutoHyper, HyperQB）を上回り、他がタイムアウトするケースでもしばしば数秒で解決しました。
  • 低レベルモデル: 標準的な SMV ベンチマーク（Alloy に変換し、再度変換したもの）に適用された場合、HyperSMV は競争力のあるパフォーマンスを示し、同等またはそれ以上の効率で期待される結果を再現しました。
  • 記号的 vs 明示的: 記号的バックエンド（Sym）はバグ発見（反例の発見）にはよく機能しましたが、有界モデル検査（BMC）セマンティクスに限界があるため、全称命題についてはしばしば決定的でない結果をもたらしました。明示的バックエンド（Exp）は、より小さなスコープの網羅的検証においてより効果的でした。

意義と主張
本論文は、HyperPardinus が高レベルソフトウェア設計とハイパープロパティ検証の間のギャップを埋めると主張しています。実務者が高レベル関係言語（Alloy）で直接ハイパープロパティを指定および検証できるようにすることで、このアプローチは低レベル形式への手動変換の必要性を排除します。著者は、これによりハイパープロパティ検証がより広範なソフトウェア工学コミュニティにアクセス可能になると述べています。

この研究はその範囲について控えめです。ハイパーロジックにおけるすべての決定可能性の問題を解決するものではなく、以前は既存のツールでは扱いが困難または使用不可能だった複雑な高レベルモデルを分析するための実用的なパイプラインを実証するものです。その意義は、使いやすさ（高レベル仕様と可視化）と、以前は低レベル、手動、または演繹的アプローチに限定されていた複雑なシナリオ（交互する量化子を持つリニアライザビリティなど）の検証の実現可能性にあります。著者は、このアプローチが標準形式に依存しており、将来の低レベルモデルチェッカーの改善の恩恵を受けることを保証していると指摘しています。