AI 辅助程序验证

研究背景

形式化验证的目标，是通过数学证明来判断程序是否满足预先定义的性质。

传统测试只能检查有限数量的输入，而形式化证明可以在明确的模型和假设下，对所有符合要求的输入进行推理。

在形式化方法中，常用 Hoare Triple（霍尔三元组）表示这种关系： 其中：

• (P)：程序执行前必须满足的条件。
• (C)：待验证程序。
• (Q)：程序执行后必须满足的条件。

但是，证明代码通常需要人工编写，成本可能远远超过程序本身，大概是1：20的代码比例。

研究目标

希望将大模型与成熟的程序验证工具结合，其基本思想是：人类定义程序需要满足的性质，AI 生成证明步骤，并由定理证明器检查是否成立。

因此，系统的可靠性主要来自形式化证明检查机制，而不是大模型推断

核心方法

实验结果

说明 AI 已经能够完成一些经典算法的功能正确性证明，比如插入排序算法

相比 Anthropic 的研究，重要的差别是：函数规约允许用数学语言，来定义程序的复杂功能。它可以把数学公式来作为规约，要求返回值满足相应数学性质。而只依赖有限的测试样例作为规约，很难完整表达这类数学通用性质。

尚未解决的问题

1. 正确的规约从何而来？证明器能够证明程序满足某个规约，但不能保证这就是用户真正想要的功能
2. 复杂程序的自动证明仍可能失败。AI 即使可以编写证明代码，不代表能发现所有复杂程序所需的条件。
3. 如果编译器或底层运行环境存在错误，仅凭源码级证明不能保证最终机器代码的全部行为
4. QCP 等程序验证工具非常重要，虽然有ai辅助，但仍十分依赖成熟的验证基础设施。

核心结论：AI 解决的是证明过程中的人工成本，形式化工具提供正确性检查，复杂功能规约仍然是整个验证体系的基础。

AgentSentinel——面向 Computer-Use Agent 的实时安全防御

研究背景

Agent 带来了新的安全威胁，传统大模型主要生成文字。但 Computer-Use Agent 已经能够完成多种复杂行为，执行 Shell 命令，访问和修改文件，操作浏览器，调用第三方工具，访问网络服务等，这使得模型的错误行为可能产生真实的系统副作用。

1. 传统防御机制无法充分理解 Agent 的行为意图。
2. 工具种类繁多，无法逐一编写安全策略
3. 实时审计会产生性能开销

研究目标

设计一个尽量不改变现有 Agent 运行架构的安全防御框架，实现：系统行为实时观测 → 威胁识别 → 安全审计 → 操作拦截或恢复。同时希望同时兼顾安全性、通用性和性能效率。

核心方法

同时防御模块内部也利用了大模型，通过理解用户任务和操作上下文，判断某个系统行为是否危险

C2Btor——基于硬件模型检查的 C 程序验证

研究背景

新算法很难直接在传统程序验证工具之间复用

研究目标

把 C 程序转换成硬件模型，让成熟的硬件验证算法来证明 C 程序是否安全，提升 C 程序的安全性质验证能力

核心方法

把硬件模型检查的成熟技术迁移到 C 程序验证中

基于安全属性的 Rust 程序验证

研究背景

研究背景：Rust 为什么还需要安全验证？ Rust 通过所有权、借用检查和类型系统提供较强的内存安全保障。但 Unsafe API 仍然可能引入未定义行为。

核心方法

1. 统一描述和维护 Unsafe API 的安全要求
2. 复用这些安全要求，自动验证函数调用是否满足相应的安全契约 创新点：把原本供人阅读的安全文档转化为可自动验证的安全契约，减少人工编写验证代码的成本。