Kani项目在Ubuntu 24.04上的开发环境支持

Kani是一个基于模型验证的Rust程序验证工具，它依赖于CBMC（C Bounded Model Checker）作为底层验证引擎。近期在Ubuntu 24.04系统上搭建Kani开发环境时遇到了CBMC安装包兼容性问题，这促使项目团队对开发环境支持进行了改进。

问题背景

在Ubuntu 24.04系统上安装Kani开发环境时，安装脚本会尝试获取对应系统的CBMC二进制包。然而，当时Diffblue官方发布的CBMC 6.4.0版本仅提供了针对Ubuntu 20.04和22.04的预编译包，缺少对24.04的支持。这导致开发者在24.04系统上无法直接通过安装脚本获取CBMC，影响了开发环境的搭建。

解决方案

针对这一问题，解决方案分为两个层面：

1. CBMC层面的改进：Diffblue团队在CBMC 6.4.1版本中增加了对Ubuntu 24.04的官方支持，提供了对应的.deb安装包。这一改进确保了CBMC可以在最新的Ubuntu系统上正常运行。

2. Kani项目层面的完善：虽然CBMC已经提供了24.04的支持，但Kani项目仍需完善持续集成(CI)测试环节，确保在Ubuntu 24.04系统上的完整开发流程都能正常工作。这包括：

   • 添加针对Ubuntu 24.04的CI测试任务
   • 更新开发环境设置脚本
   • 验证整个工具链在新系统上的兼容性

技术意义

这一改进体现了开源项目对最新操作系统版本的前瞻性支持，具有以下技术意义：

1. 兼容性保障：确保开发者可以在最新的Ubuntu LTS版本上使用Kani工具链，跟上操作系统的发展步伐。

2. 开发体验优化：通过自动化脚本和CI测试，简化了开发环境的搭建过程，降低了新贡献者的入门门槛。

3. 工具链维护：展示了项目对依赖项管理的重视，及时跟进底层工具(CBMC)的更新，保持整个验证工具链的健壮性。

未来展望

随着Ubuntu 24.04逐渐成为主流开发环境，Kani项目团队将继续完善相关支持：

1. 全面测试Kani在24.04上的各项功能
2. 优化性能表现
3. 收集并解决可能出现的兼容性问题
4. 为后续Ubuntu版本提前做好准备

这一系列工作将确保Kani验证工具能够在最新的开发环境中稳定运行，为Rust程序的可靠性验证提供有力支持。