Solver-validated llm guidance speeds hardware security proofs 600 fold
SLED-IFV: Solver-Validated LLM-Guided Decomposition for Scalable Hardware Information-Flow Verification
Cryptography and SecurityHardware ArchitectureLogic in Computer Science
Summary
Verifying that computer chips handle secret information safely can take a very long time due to complex logic and hard-to-prove relations. The authors created a new method that breaks down these tough proofs into smaller, easier parts using smart summaries and highlighting important relations. They use a combination of a large language model (LLM) and formal solvers to automate this breakdown and check the work. This approach made verifying real chip designs up to 600 times faster and completed proofs that previously timed out. Their system still relies on the formal verification tools to confirm correctness, ensuring strong guarantees.
What this means in practice
- •For hardware design teams: Speed up security verification of chip designs by automating proof decomposition and validation steps.
- •For formal verification engineers: Cut solver runtimes dramatically on complex information-flow proofs with an LLM-guided, solver-checked proof workflow.
Authors
Liangtao Dai, Yimin Gao, Melika Morsali, Mircea Stan
Abstract
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.