自動驗證是一種有助于檢查程序是否滿足某些屬性的技術，例如內存安全性和避免在運行時錯誤。此外，自動驗證工具使你能夠驗證并發代碼的正確性，這很難手工測試。

自動驗證對Rust特別重要，因為它可以幫助確保正確使用unsafe的代碼。在這篇文章中，我們將討論五個最常用的Rust驗證工具，以及它們如何幫助你構建更可靠的軟件。

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);
}

運行結果：

圖片

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非常重要，盡管它們可能尚未被開發人員廣泛采用。這些工具可以發現使用傳統測試方法無法發現的錯誤，并且可以提高代碼的可靠性。