Rust 这 5 个自动验证工具，你知道几个？

自动验证是一种有助于检查程序是否满足某些属性的技术，例如内存安全性和避免在运行时错误。此外，自动验证工具使你能够验证并发代码的正确性，这很难手工测试。

自动验证对 Rust 特别重要，因为它可以帮助确保正确使用 unsafe 的代码。在这篇文章中，我们将讨论五个最常用的 Rust 验证工具，以及它们如何帮助你构建更可靠的软件。

开始之前，介绍一下​最近很火的开源技术，低代码。

作为一种软件开发技术逐渐进入了人们的视角里，它利用自身独特的优势占领市场一角——让使用者可以通过可视化的方式，以更少的编码，更快速地构建和交付应用软件，极大程度地降低了软件的开发、配置、部署和培训成本。

应用地址：https://www.jnpfsoft.com

开发语言：Java/.net

这是一个基于 Java Boot/.Net Core 构建的简单、跨平台快速开发框架。前后端封装了上千个常用类，方便扩展；采用微服务、前后端分离架构，集成了代码生成器，支持前后端业务代码生成，满足快速开发；框架集成了表单、报表、图表、大屏等各种常用的 Demo 方便直接使用；后端框架支持 Vue2、Vue3，平台即可私有化部署，也支持 K8S 部署。

1，cargo-fuzz

我们将讨论的第一个工具是 cargo-fuzz，它使用一种称为模糊测试的技术来进行自动化软件测试。通过向程序提供许多有效的、几乎有效的或无效的输入，模糊测试可以帮助开发人员找到不希望看到的行为或漏洞。

当我们编写测试时，我们通常只考虑一些正常输入，并根据我们对系统反应的想象来编写测试。这种方法可能会导致遗漏错误，特别是那些由意外的或不正确的输入引起的错误。

模糊测试可以通过为程序提供各种各样的输入(包括无效的和意外的输入)来帮助你找到这些遗漏的错误。如果程序在响应这些输入时崩溃或行为异常，则表示存在错误。

cargo-fuzz crate 可以对 Rust 代码进行模糊测试，它的工作原理是生成随机输入，并将它们输入到要测试的函数中。如果函数出现故障或崩溃，cargo-fuzz 将保存导致故障的输入。

通过以下命令安装 cargo-fuzz：

复制 cargo install cargo-fuzz

下面是一个如何使用 cargo-fuzz 对 Rust 函数进行模糊测试的例子：

复制 #![no_main] #[macro_use] extern crate libfuzzer_sys; fuzz_target!(|data: &[u8]| { let json_string = std::str::from_utf8(data).unwrap(); let _ = serde_json::from_str::<serde_json::Value>(&json_string).unwrap(); });

上面的代码通过向 JSON 解析器提供随机输入来测试它。fuzz_target 将持续被调用，直到遇到触发 panic 并导致崩溃的输入。

注意：通过模糊测试发现的一些错误可能在现实生活中不实用或不适用，这意味着模糊测试可能会产生误报。此外，模糊测试可能是资源密集型的，特别是在对大型或复杂的代码库进行模糊测试时。

2，Kani

Kani 是一个现代的自动代码验证工具，可以帮助你在几秒钟内验证 Rust 代码的正确性。它使用一种称为模型检查的技术，一种探索程序所有状态的方法，包括通过正常执行无法到达的状态。

模型检查允许 Kani 检测代码中的问题，这些问题可能是由意外的逻辑引起的。还可以使用 Kani 来识别单元测试、集成测试甚至手工测试很难或不可能发现的问题。

通过以下命令安装 Kani：

复制 cargo install --locked kani-verifier cargo kani setup

让我们看一下下面的代码：

复制 fn product(a: i32, b: i32) -> i32 { a * b }

上面的代码是有效的 Rust 代码，对吗？花点时间再看一遍——你能发现这段代码有什么可能出错的地方吗？

让我们用 Kani 来找出答案：

复制 fn product(a: i32, b: i32) -> i32 { a * b } #[kani::proof] fn main() { let a = kani::any(); let b = kani::any(); let result = product(a, b); println!("The product of {} and {} is {}", a, b, result); }

运行结果：

添加图片注释，不超过 140 字（可选）

图片

Kani 在乘法过程中发现了溢出的可能性。

这是因为 product 函数不能确保我们不超过 i32 的最大值，即 2,147,483,647，任何大于该数的值都会抛出错误。本质上，无论这个函数用于什么，它都不能处理大于 20 亿的数字。

在这种情况下，使用 Kani 来识别这个潜在的问题允许您要么立即更改数据类型，要么保持原样，如果错误是预期的行为，则适当地处理错误。

3，Proptest

Proptest 使用大量有效和无效的输入来测试函数的属性，以发现 bug。这与单元测试等经典测试方法不同，在单元测试中，指定一些输入并根据期望的行为添加断言。

属性测试是模糊测试的一种形式，它更容易控制，更侧重于验证特定的属性。这使得它成为测试复杂系统的一个很好的选择，在这些系统中，传统的模糊测试可能太慢或无效。

让我们来看看如何使用 Proptest crate：

复制 use proptest::prelude::{any, proptest}; fn add_two_numbers(first_number: i32, second_number: i32) -> i32 { first_number + second_number } proptest! { #[test] fn test_add_two_numbers(first_number in any::<i32>(), second_number in any::<i32>()) { let expected = first_number + second_number; let actual = add_two_numbers(first_number, second_number); assert_eq!(actual, expected); } }

在上面的代码中，我们正在测试一个简单的函数，它将两个数字相加。这样一个简单的函数可能会出什么问题呢？

让我们看一下 test_add_two_numbers 函数签名：

复制 fn test_add_two_numbers(first_number in any::<i32>(), second_number in any::<i32>())

any::<i32>()是一个 Protest 中的类型，它生成随机的 i32 值，包括有效的和无效的。这允许我们使用广泛的输入来测试 add_two_numbers()函数，包括边缘情况和异常情况。

Proptest 测试函数将为 first_number 和 second_number 参数生成大量随机输入。如果任何测试失败，Proptest 将把失败的输入打印到控制台。

报告显示有溢出的可能，它还显示了最小的可重复输入。有了这些信息，我们就可以继续修复 bug 了。

虽然属性测试可以很好地用于选定的输入范围，但它有时会遗漏一些边缘情况，并给你一个假结果。换句话说，它可能会在实际上没有错误的情况下产生错误，或者在指定的覆盖范围之外找不到错误。

4，Rust KLEE

KLEE 是一个符号执行引擎，它智能地探索程序中的所有代码路径，以发现漏洞或错误。它建立在 LLVM 编译器基础设施之上，该基础设施是用 C 和 C++编写的。

因此，大多数 KLEE 实现也是用 C 和 C++语言实现的。然而，KLEE 的基本概念可以在任何编程语言中实现。

Rust Klee 是 Klee 的开源 Rust 实现，被设计用来检查特定的属性。

• 安全检查

• 不变量

• 参数化的检查

• 检查 Rust 程序的功能正确性

Rust Klee 还没有准备好用于生产，但它仍然值得一提，它是一个很酷的工具，可以帮助在 Rust 生态系统中形成正式的验证环境。

5，Haybale

Haybale 也是一个符号执行引擎，具有与 Rust Klee 相似的功能，Haybale 完全是用 Rust 编写的，并且在底层基于 Rust LLVM IR。

作为一个符号执行引擎，它专注于将整个程序变量转换为数学表达式，并对执行路径进行推理，以检测错误或漏洞。Haybale 最好的部分是它可以测试你的 Rust 代码，而不需要添加额外的测试代码。

让我们看一个检查函数 foo 是否返回 0 的例子。首先，我们写出要分析的函数，你可以用任何编程语言写这个，然后把它转换成字节码：

复制 fn foo(x: f64) -> f64 { x * x - 4.0 }

字节码将保存在项目的某个地方，你可以在 Rust 代码的项目变量中引用它：

复制 let project = Project::from_bc_path("/path/to/file.bc").unwrap();

现在，我们可以使用 haybale 中的 find_zero_of_func 方法来发现当函数接收到零输入时存在的错误。

复制 use haybale::{find_zero_of_func, Project}; fn main() { let project = Project::from_bc_path("/path/to/file.bc").unwrap(); match find_zero_of_func("foo", &project, haybale::Config::default(), None) { Ok(None) => println!("foo() can never return 0"), Ok(Some(inputs)) => println!("Inputs for which foo() returns 0: {:?}", inputs), Err(e) => panic!("{}", e), } }

Haybale 可以对整个代码进行推理，发现 bug，并返回一份报告，证明代码是否存在 bug。虽然 Haybale 可能不会捕获所有错误，但它很可能会捕获导致运行时崩溃的严重错误，并给你一个修复它们的机会。

总结

自动验证工具对于发现软件开发中的 bug 非常重要，尽管它们可能尚未被开发人员广泛采用。这些工具可以发现使用传统测试方法无法发现的错误，并且可以提高代码的可靠性。