Rust 的 5 個自動驗證工具

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

自動驗證對 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::() 是一個 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 非常重要，儘管它們可能尚未被開發人員廣泛採用。這些工具可以發現使用傳統測試方法無法發現的錯誤，並且可以提高代碼的可靠性。

本文由 Readfog 進行 AMP 轉碼，版權歸原作者所有。
來源：https://mp.weixin.qq.com/s/eQhs2TvmofyFhbwo5LdB9Q