美军启动RSSA计划：形式化验证正在成为网络安全新基石

    DARPA在会上强调，随着军事系统数字化和网络化程度的不断深化，任何微小的软件漏洞都可能直接危及作战效能乃至国家安全。传统依赖漏洞修复与补丁更新的被动防御模式，已难以应对日益复杂和快速演进的网络威胁。因此，美军必须转向“设计即安全”的主动防御战略，而形式化方法正是实现该目标的核心技术途径。

    DARPA 自2012 年起便通过“高可靠性网络军事系统”项目，探索以形式化方法确保无人机与军用车辆代码的正确性，并取得“三周内无人机系统零成功入侵”的标志性成果。此后，通过“可扩展验证”（CRASH/CASE）、“微内核安全”（MILS）及“迷你顶点”（Mini-VERTEX）等一系列项目，DARPA 不断将形式化验证技术深度集成至国防工业的软件供应链与嵌入式系统设计中。其根本目标是以数学证明替代事后补救，使软件在部署前即具备可验证的高安全性与高可靠性。

    RSSA 计划的推出，是 DARPA 推动形式化方法走向规模化应用的关键举措，其影响将超越军事范畴，逐步渗透至关键基础设施领域——从操作系统内核到通信协议栈，从自动驾驶控制软件到卫星地面系统，形式化方法的适用边界正在持续扩展。

    形式化验证被 DARPA 称为软件安全的"终极手段"，因其通过数学方法严格证明软件或硬件系统的正确性和安全性，而非依赖有限场景的测试来推测可能存在的问题。它将系统行为建模为数学公式，用逻辑推理工具验证设计是否满足预先定义的安全属性。常见方法包括模型检查、定理证明和抽象解释，能够覆盖所有可能的运行状态，要么证明系统绝对安全，要么提供精确的漏洞反例。与传统测试方法只能覆盖部分输入场景相比，形式化方法在理论上能够实现"全覆盖"，这正是 DARPA 将其视为未来国防软件安全基石的根本原因。

    DARPA 的 RSSA 计划凸显了形式化验证的重要性，也为全球软件与网络安全产业带来启示：安全不应依赖事后修补，而应在设计阶段就通过数学手段获得保证。望安科技积极布局形式化验证领域，自主研发了基础软硬件形式化建模与验证工具W-Cert、软件源码形式化测试与验证工具 W-AVC 等核心工具。

    W-Cert 可以有效支持企业从安全要求、安全策略、安全功能规范到安全设计的形式化建模与验证，并提供符合统一准则（CC）评估要求的形式化证据，该工具基于 CC 标准推荐使用的 lsabelle 定理证明器，可提供安全性质所需的一阶高阶逻辑描述方法、安全策略模型和功能规范所需的抽象状态机统一建模。

    W-AVC 则依托形式化验证技术，通过数学证明排查代码中的缺陷和安全隐患。该工具可以允许开发验证⼈员基于规约编写基准代码，⾃动检查代码中的安全漏洞，从而在开发流程早期增强系统的安全性，有效降低现代⼤型软件架构带来的潜在⻛险。

    随着国际安全标准日趋严格、认证门槛不断提升，企业亟需提前布局形式化方法，构建符合全球标准的软件安全能力。望安科技将继续深耕形式化验证领域，助力中国企业在国际竞争中掌握安全话语权，为软件系统的安全性、可靠性及合规性提供坚实支撑。