ハードウェアの情報流検証を分割して高速化する手法
SLED-IFV: Solver-Validated LLM-Guided Decomposition for Scalable Hardware Information-Flow Verification
この論文をやさしく読む
ひとことで言うと
秘密情報がハードウェアのタイミングや制御に漏れないかを証明する作業を、意味を保つ分割と形式検証で速める方法を示した。
何に役立つ？
大きなRTL回路で情報流検証が時間切れになる場合に、証明対象を単純化・強化する候補を探す参考になる。最終的な採否は形式検証器が判定する。
この研究の面白いところ
LLMは分割案を出す役割に限定し、証明の正しさはバックエンドが判断する。9件のベンチマークで最大603倍の高速化があり、12時間の時間切れ2件を完了させた。
どこまで分かった？
評価は実際のRTLから構成した9件のベンチマークで行われた。すべてのRTLや情報流の性質で同じ高速化が得られるかは、この要旨には示されていない。
v1のアブストラクトに基づくAI解説。日本語訳とは別に、用途の解釈を含みます。
アブストラクトの日本語訳
形式的なハードウェア情報流検証（IFV）は、秘密に依存するタイミングや制御動作がないことを強く保証できるが、現実的なRTLでは規模の面で行き詰まりやすい。本研究は、回路を二つ組み合わせた自己合成型のIFVで、繰り返し現れる二つの証明障壁を特定する。一つは、必要な性質には簡潔な境界の関係で十分なのに、証明しにくいデータ経路の実装が支配的になる実装の複雑さである。もう一つは、二つの回路の間で成り立つ公開制御の事実に証明が依存するのに、証明器がそれを効率よく推論できない、関係的な帰納の複雑さである。これに対し、二種類の意味に基づく証明分割を導入する。機能的な単純化では、証明困難なRTL領域を、検証済みで過大近似となる要約に置き換える。関係的な強化では、帰納に必要な二つの回路間の関係を明示して証明する。 さらに、ソルバーによる検証を伴うLLM誘導型の処理系SLED-IFVを提示し、分割方法と対象の選択を自動化する。自己合成した検証回路と、正解を含まない判断シートを入力とし、LLMが分割案を提案して、コントローラーの検査の下で証明用の成果物に具体化する。コントローラーは検査済みの成果物を証明すべき条件へ変換し、採否は形式検証のバックエンドだけが決める。実際のRTLから構成した9件の非自明なベンチマークで、ソルバー単独と比べて最大603倍の高速化を達成し、12時間で時間切れとなった2件を証明完了に変えた。閉ループの処理では、全ケースで検証器が受け入れる分割を生成した。
v1の要旨から自動生成。本文の精読・人による確認は未実施。
- 初稿
- 2026-09-22（UTC）
- 最新改訂
- 2026-09-22 · v1
- 査読・掲載
- 査読状況未確認
更新履歴
- v1 2026-09-22 この版を読む
取得できた版を表示。版の更新は査読済みを意味しません。過去版の本文差分は未解析です。
原文の要旨
Formal hardware information-flow verification (IFV) provides strong guarantees against secret-dependent timing and control behavior, but often scales poorly on realistic RTL. We identify two recurring proof barriers in self-composed IFV: implementation complexity, where proof-hard datapath logic dominates even though the property needs only a compact boundary relation, and relational inductive complexity, where the proof depends on cross-copy public-control facts that the backend prover does not infer efficiently. To address them, we introduce two semantic proof decomposition forms: functional simplification, which replaces a proof-hard RTL region with a validated over-approximate summary, and relational strengthening, which exposes and proves the cross-copy relations needed for induction. We further present SLED-IFV, a solver-validated LLM-guided flow that automates the selection of these forms and their concrete targets. Given a self-composed miter and an oracle-free decision sheet, the LLM proposes a decomposition, then materializes it into proof artifacts under controller checks. The controller compiles the checked artifacts into proof obligations, and the formal verification backend remains the sole authority for acceptance. Across nine nontrivial benchmarks constructed from real RTL, SLED-IFV achieves up to 603x solver-only speedup and converts two 12-hour timeouts into completed proofs. The closed-loop flow produces verifier-accepted decompositions for all cases.
著者のコメント
Accepted at the 32nd Asia and South Pacific Design Automation Conference (ASP-DAC 2027). 7 pages, 3 figures, and 5 tables
arXiv ID: 2609.25637 ／ 要約の誤りについて