首页
/ Kani项目中的函数合约验证问题分析

Kani项目中的函数合约验证问题分析

2025-06-30 21:25:51作者:吴年前Myrtle

背景介绍

Kani是一个用于Rust程序形式化验证的工具,它能够帮助开发者发现程序中的潜在错误。在Kani的最新版本中,引入了一个名为"函数合约"的功能,允许开发者对函数的行为进行规范定义和验证。然而,在使用过程中发现了一个有趣的问题:某些被普通验证接受的代码,在函数合约验证中却会失败。

问题现象

开发者提供了一个简单的测试用例,包含一个嵌套循环的函数foo,以及两个验证函数:一个使用kani::proof,另一个使用kani::proof_for_contract。令人意外的是,前者验证成功,而后者却报告了失败,错误信息指出"Check that self->start is assignable"失败。

技术分析

底层机制差异

通过深入分析,我们发现这个问题源于Kani底层使用的CBMC工具在处理函数合约验证时的特殊行为。具体来说,函数合约验证会引入额外的写入集(write set)检查机制,这种机制与普通验证路径有所不同。

具体问题原因

  1. 存储生命周期事件处理不完整:goto-instrument工具未能正确处理动态的storageLive事件,导致写入集管理出现问题。当内层循环结束时,迭代器变量被标记为"dead",但在下一次循环开始时,没有正确重新激活。

  2. 符号执行混淆:symex引擎错误地将两个不同的迭代器变量视为同一个对象。当第一个内层循环结束时,迭代器被标记为不可写,这影响了后续外层循环的验证。

  3. MIR到GOTO转换问题:当前的转换规则可能没有准确反映MIR的语义。特别是变量生命周期的处理方式可能存在偏差,导致验证时出现意外行为。

解决方案

CBMC团队已经提交了一个修复方案,通过忽略storageLivestorageDead事件来解决这个问题。这个修改消除了由于只跟踪storageDead而导致的虚假反例。同时,默认的指针检查仍然能够检测到无效的指针访问。

技术启示

这个问题揭示了形式化验证工具中几个重要的技术点:

  1. 变量生命周期管理:在程序验证中,准确跟踪变量的生命周期至关重要,特别是在循环和嵌套结构的情况下。

  2. 不同验证路径的一致性:工具的不同验证路径(如普通验证和合约验证)应该保持一致的语义理解,否则会导致令人困惑的结果。

  3. 底层转换的准确性:从高级语言中间表示到验证工具内部表示的转换必须精确反映原始语义,任何偏差都可能导致验证结果的不一致。

结论

这个问题虽然表面上看起来是一个简单的验证失败,但实际上涉及到了形式化验证工具的多个核心组件。它不仅展示了Kani工具的内部工作机制,也提醒我们在使用验证工具时需要注意不同验证路径可能带来的差异。随着CBMC修复方案的合并,这个问题将得到彻底解决,使函数合约验证更加可靠和一致。

登录后查看全文
热门项目推荐

热门内容推荐

最新内容推荐

项目优选

收起
docsdocs
OpenHarmony documentation | OpenHarmony开发者文档
Dockerfile
149
1.95 K
kernelkernel
deepin linux kernel
C
22
6
openHiTLSopenHiTLS
旨在打造算法先进、性能卓越、高效敏捷、安全可靠的密码套件,通过轻量级、可剪裁的软件技术架构满足各行业不同场景的多样化要求,让密码技术应用更简单,同时探索后量子等先进算法创新实践,构建密码前沿技术底座!
C
980
395
ohos_react_nativeohos_react_native
React Native鸿蒙化仓库
C++
192
274
RuoYi-Vue3RuoYi-Vue3
🎉 (RuoYi)官方仓库 基于SpringBoot,Spring Security,JWT,Vue3 & Vite、Element Plus 的前后端分离权限管理系统
Vue
931
555
openGauss-serveropenGauss-server
openGauss kernel ~ openGauss is an open source relational database management system
C++
145
190
nop-entropynop-entropy
Nop Platform 2.0是基于可逆计算理论实现的采用面向语言编程范式的新一代低代码开发平台,包含基于全新原理从零开始研发的GraphQL引擎、ORM引擎、工作流引擎、报表引擎、规则引擎、批处理引引擎等完整设计。nop-entropy是它的后端部分,采用java语言实现,可选择集成Spring框架或者Quarkus框架。中小企业可以免费商用
Java
8
0
金融AI编程实战金融AI编程实战
为非计算机科班出身 (例如财经类高校金融学院) 同学量身定制,新手友好,让学生以亲身实践开源开发的方式,学会使用计算机自动化自己的科研/创新工作。案例以量化投资为主线,涉及 Bash、Python、SQL、BI、AI 等全技术栈,培养面向未来的数智化人才 (如数据工程师、数据分析师、数据科学家、数据决策者、量化投资人)。
Jupyter Notebook
75
66
openHiTLS-examplesopenHiTLS-examples
本仓将为广大高校开发者提供开源实践和创新开发平台,收集和展示openHiTLS示例代码及创新应用,欢迎大家投稿,让全世界看到您的精巧密码实现设计,也让更多人通过您的优秀成果,理解、喜爱上密码技术。
C
65
519
CangjieCommunityCangjieCommunity
为仓颉编程语言开发者打造活跃、开放、高质量的社区环境
Markdown
1.11 K
0