一句话：提出 Spoq2，首个高度自动化验证未修改系统软件安全属性的框架，通过降低验证复杂度使 SMT 求解可行。
系统软件复杂且常隐藏可被利用的安全漏洞，形式化验证虽能保证无缺陷，但证明成本高昂，难以应用于真实系统代码。Spoq2 基于一个观察：非干涉性等许多安全属性可归约为对建模系统软件的迁移系统中单个迁移建立归纳不变式，然而直接对真实系统代码验证这些不变式会压垮现有 SMT 求解器。为此，Spoq2 自动降低验证复杂度：将迁移分解为单个执行路径，把 cone-of-influence 分析扩展到单个迁移级别，在调用 SMT 求解器前消除无关的机器状态、子句与控制流路径；并通过指针抽象优化指针操作的建模与验证，从 SMT 查询中消除昂贵的位运算。作者以极少人工投入在四个未修改的真实系统代码库上验证了安全属性，证明了 Spoq2 的有效性。
System software is often complex and hides exploitable security vulnerabilities. Formal verification promises bug-free software but comes with a prohibitive proof cost. We present Spoq2, the first verification framework to highly automate security verification of unmodified system software. Spoq2 is based on the observation that many security properties, such as noninterference, can be reduced to establishing inductive invariants on individual transitions of a transition system that models system software. However, directly verifying such invariants for real system code overwhelms existing SMT solvers. Spoq2 makes this possible by automatically reducing verification complexity. It decomposes transitions into individual execution paths, extends cone-of-influence analysis to the individual transition level, and eliminates irrelevant machine states, clauses, and control-flow paths before invoking the SMT solver. Spoq2 further optimizes how pointer operations are modeled and verified through pointer abstractions that eliminate expensive bit-wise operations from SMT queries. We demonstrate the effectiveness of Spoq2 by verifying security properties of four unmodified, real-world system codebases with minimal manual effort.
@inproceedings{YangQRLYNG26,
title = {Highly Automated Verification of Security Properties for Unmodified System Software},
author = {Ganxiang Yang and Wei Qiang and Yi Rong and Xuheng Li and Fanqi Yu and Jason Nieh and Ronghui Gu},
booktitle = {ASPLOS},
year = {2026},
doi = {10.1145/3779212.3790171}
}