Rust形式化验证工具Kani-verifier的使用，Kani-verifier提供Rust代码的模型检查和自动定理证明功能

Rust形式化验证工具Kani-verifier的使用

Kani Rust Verifier 是一个针对 Rust 的位精确模型检查器。

Kani 特别适用于验证 Rust 中的不安全代码块，这些代码块的"不安全超级能力"不被编译器检查。

Kani Logo

Kani 验证以下内容：

  • 内存安全（例如，空指针解引用）
  • 用户指定的断言（即 assert!(...)）
  • 无 panic（例如，在 None 值上调用 unwrap()）
  • 不存在某些类型的意外行为（例如，算术溢出）

安装

要安装最新版本的 Kani（需要 Rust 1.58+；支持 Linux 或 Mac），运行：

cargo install --locked kani-verifier
cargo kani setup

如何使用 Kani

类似于测试，你需要编写一个 harness（测试用例），但使用 Kani 时，你可以使用 kani::any() 检查所有可能的值：

use my_crate::{function_under_test, meets_specification, precondition};

#[kani::proof]
fn check_my_property() {
   // 创建一个非确定性输入
   let input = kani::any();

   // 根据函数的先决条件约束它
   kani::assume(precondition(input));

   // 调用要验证的函数
   let output = function_under_test(input);

   // 检查它是否符合规范
   assert!(meets_specification(input, output));
}

Kani 将尝试证明所有有效输入都会产生可接受的输出，而不会 panic 或执行意外行为。否则 Kani 会生成指向失败的跟踪记录。

完整示例

下面是一个完整的 Kani 验证示例，展示如何验证一个简单的函数：

// 这是一个简单的绝对值函数示例
fn absolute_value(x: i32) -> i32 {
    if x < 0 {
        -x
    } else {
        x
    }
}

#[kani::proof]
fn verify_absolute_value() {
    // 创建任意整数输入
    let input = kani::any::<i32>();
    
    // 调用绝对值函数
    let result = absolute_value(input);
    
    // 验证结果总是非负的
    assert!(result >= 0);
    
    // 验证对于非负输入，结果等于输入
    if input >= 0 {
        assert!(result == input);
    } else {
        assert!(result == -input);
    }
}

要运行这个验证，你需要：

  1. 将上述代码保存为 src/lib.rs
  2. 在项目目录中运行 cargo kani

这个示例展示了 Kani 如何验证一个简单的绝对值函数总是返回非负值，并且对于非负输入返回原值，对于负输入返回其相反数。

另一个完整示例

下面是一个验证数组边界检查的完整示例：

// 验证数组访问是否越界
fn safe_get(arr: &[i32], index: usize) -> Option<i32> {
    if index < arr.len() {
        Some(arr[index])
    } else {
        None
    }
}

#[kani::proof]
fn verify_array_access() {
    // 创建任意数组和索引
    let arr: [i32; 5] = kani::any();
    let index = kani::any();
    
    // 调用安全访问函数
    let result = safe_get(&arr, index);
    
    // 验证结果
    if index < 5 {
        assert!(result.is_some());
    } else {
        assert!(result.is_none());
    }
}

GitHub Action

你可以在 CI 中使用 Kani，使用 model-checking/kani-github-action@VERSION。

许可证

Kani 采用 MIT 许可证和 Apache 许可证（版本 2.0）双重授权。


1 回复

Rust形式化验证工具Kani-verifier的使用指南

什么是Kani-verifier?

Kani-verifier是一个用于Rust代码的形式化验证工具，它提供了模型检查和自动定理证明功能。Kani可以帮助开发者验证Rust代码的正确性，特别是对于unsafe代码和关键系统组件。

主要特性

  • 基于模型检查的验证方法
  • 支持Rust的所有权系统和类型系统
  • 可以验证内存安全和未定义行为
  • 支持用户指定的不变量和断言
  • 自动定理证明能力

安装方法

首先确保你已经安装了Rust工具链，然后运行：

cargo install --locked kani-verifier

或者将Kani作为开发依赖添加到你的项目中：

cargo add --dev kani

基本使用方法

1. 编写验证代码

#[kani::proof]
fn check_abs() {
    let x: i32 = kani::any();  // 生成任意i32值
    let result = if x >= 0 { x } else { -x };  // 计算绝对值
    assert!(result >= 0);  // 验证结果非负
}

2. 运行验证

cargo kani

高级功能示例

验证数据结构不变量

// 定义非空向量结构体
struct NonEmptyVec<T> {
    first: T,
    rest: Vec<T>,
}

impl<T> NonEmptyVec<T> {
    #[kani::proof]
    fn new(first: T) -> Self {
        Self { first, rest: Vec::new() }  // 永远保证至少有一个元素
    }

    #[kani::proof]
    fn len(&self) -> usize {
        1 + self.rest.len()  // 长度至少为1
    }
}

验证unsafe代码

#[kani::proof]
fn unsafe_slice_check() {
    let mut arr = [1, 2, 3, 4];  // 初始化数组
    let ptr = arr.as_mut_ptr();  // 获取可变原始指针
    
    unsafe {
        *ptr.add(3) = 5;  // 修改第4个元素
        assert!(*ptr.add(3) == 5);  // 验证修改成功
    }
}

完整示例demo

// 验证二分查找的正确性
#[kani::proof]
fn binary_search_verify() {
    let mut arr = [1, 2, 3, 4, 5, 6, 7, 8, 9];
    let target: i32 = kani::any();
    kani::assume(target >= 1 && target <= 9);  // 假设目标值在数组范围内
    
    let mut left = 0;
    let mut right = arr.len();
    
    #[kani::unwind(10)]  // 设置循环最大展开次数
    while left < right {
        let mid = left + (right - left) / 2;
        if arr[mid] == target {
            assert!(arr[mid] == target);  // 验证找到正确元素
            return;
        } else if arr[mid] < target {
            left = mid + 1;
        } else {
            right = mid;
        }
    }
    
    // 如果没找到，应该是我们的假设不成立
    assert!(false, "Target should be found in the array");
}

常用宏和函数

  • kani::any(): 生成任意值用于验证
  • kani::assume(condition): 添加前提条件
  • kani::cover!: 检查某个条件是否可能为真
  • #[kani::unwind(n)]: 设置循环展开界限

实际项目集成建议

  1. 为关键算法和数据结构编写验证代码
  2. 将验证作为CI/CD流程的一部分
  3. 逐步增加验证覆盖率，从最关键的组件开始
  4. 结合单元测试和属性测试使用

限制和注意事项

  • 验证复杂代码可能需要较长时间
  • 某些Rust特性支持有限
  • 需要手动指定循环展开界限
  • 对于大型项目可能需要分模块验证

Kani-verifier是提高Rust代码可靠性的强大工具，特别适合安全关键系统和基础库的开发。

回到顶部