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

自動驗證對Rust特別重要，因為它可以幫助確保正確使用unsafe的代碼。在這篇文章中，我們將討論五個最常用的Rust驗證工具，以及它們?nèi)绾螏椭銟?gòu)建更可靠的軟件。

1，cargo-fuzz

我們將討論的第一個工具是cargo-fuzz，它使用一種稱為模糊測試的技術(shù)來進行自動化軟件測試。通過向程序提供許多有效的、幾乎有效的或無效的輸入，模糊測試可以幫助開發(fā)人員找到不希望看到的行為或漏洞。

當我們編寫測試時，我們通常只考慮一些正常輸入，并根據(jù)我們對系統(tǒng)反應(yīng)的想象來編寫測試。這種方法可能會導致遺漏錯誤，特別是那些由意外的或不正確的輸入引起的錯誤。

模糊測試可以通過為程序提供各種各樣的輸入(包括無效的和意外的輸入)來幫助你找到這些遺漏的錯誤。如果程序在響應(yīng)這些輸入時崩潰或行為異常，則表示存在錯誤。

cargo-fuzz crate可以對Rust代碼進行模糊測試，它的工作原理是生成隨機輸入，并將它們輸入到要測試的函數(shù)中。如果函數(shù)出現(xiàn)故障或崩潰，cargo-fuzz將保存導致故障的輸入。

通過以下命令安裝cargo-fuzz：

cargo install cargo-fuzz

下面是一個如何使用cargo-fuzz對Rust函數(shù)進行模糊測試的例子：

#![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將持續(xù)被調(diào)用，直到遇到觸發(fā)panic并導致崩潰的輸入。

注意：通過模糊測試發(fā)現(xiàn)的一些錯誤可能在現(xiàn)實生活中不實用或不適用，這意味著模糊測試可能會產(chǎn)生誤報。此外，模糊測試可能是資源密集型的，特別是在對大型或復雜的代碼庫進行模糊測試時。

2，Kani

Kani是一個現(xiàn)代的自動代碼驗證工具，可以幫助你在幾秒鐘內(nèi)驗證Rust代碼的正確性。它使用一種稱為模型檢查的技術(shù)，一種探索程序所有狀態(tài)的方法，包括通過正常執(zhí)行無法到達的狀態(tài)。

模型檢查允許Kani檢測代碼中的問題，這些問題可能是由意外的邏輯引起的。還可以使用Kani來識別單元測試、集成測試甚至手工測試很難或不可能發(fā)現(xiàn)的問題。

通過以下命令安裝Kani：

cargo install --locked kani-verifier
cargo kani setup

讓我們看一下下面的代碼：

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

上面的代碼是有效的Rust代碼，對嗎？花點時間再看一遍——你能發(fā)現(xiàn)這段代碼有什么可能出錯的地方嗎？

讓我們用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);
}

運行結(jié)果：

圖片

Kani在乘法過程中發(fā)現(xiàn)了溢出的可能性。

這是因為product函數(shù)不能確保我們不超過i32的最大值，即2,147,483,647，任何大于該數(shù)的值都會拋出錯誤。本質(zhì)上，無論這個函數(shù)用于什么，它都不能處理大于20億的數(shù)字。

在這種情況下，使用Kani來識別這個潛在的問題允許您要么立即更改數(shù)據(jù)類型，要么保持原樣，如果錯誤是預期的行為，則適當?shù)靥幚礤e誤。

3，Proptest

Proptest使用大量有效和無效的輸入來測試函數(shù)的屬性，以發(fā)現(xiàn)bug。這與單元測試等經(jīng)典測試方法不同，在單元測試中，指定一些輸入并根據(jù)期望的行為添加斷言。

屬性測試是模糊測試的一種形式，它更容易控制，更側(cè)重于驗證特定的屬性。這使得它成為測試復雜系統(tǒng)的一個很好的選擇，在這些系統(tǒng)中，傳統(tǒng)的模糊測試可能太慢或無效。

讓我們來看看如何使用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);
    }
}

在上面的代碼中，我們正在測試一個簡單的函數(shù)，它將兩個數(shù)字相加。這樣一個簡單的函數(shù)可能會出什么問題呢？

讓我們看一下test_add_two_numbers函數(shù)簽名：

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

any::<i32>()是一個Protest中的類型，它生成隨機的i32值，包括有效的和無效的。這允許我們使用廣泛的輸入來測試add_two_numbers()函數(shù)，包括邊緣情況和異常情況。

Proptest測試函數(shù)將為first_number和second_number參數(shù)生成大量隨機輸入。如果任何測試失敗，Proptest將把失敗的輸入打印到控制臺。

圖片

報告顯示有溢出的可能，它還顯示了最小的可重復輸入。有了這些信息，我們就可以繼續(xù)修復bug了。

雖然屬性測試可以很好地用于選定的輸入范圍，但它有時會遺漏一些邊緣情況，并給你一個假結(jié)果。換句話說，它可能會在實際上沒有錯誤的情況下產(chǎn)生錯誤，或者在指定的覆蓋范圍之外找不到錯誤。

4，Rust KLEE

KLEE是一個符號執(zhí)行引擎，它智能地探索程序中的所有代碼路徑，以發(fā)現(xiàn)漏洞或錯誤。它建立在LLVM編譯器基礎(chǔ)設(shè)施之上，該基礎(chǔ)設(shè)施是用C和C++編寫的。

因此，大多數(shù)KLEE實現(xiàn)也是用C和C++語言實現(xiàn)的。然而，KLEE的基本概念可以在任何編程語言中實現(xiàn)。

Rust Klee是Klee的開源Rust實現(xiàn)，被設(shè)計用來檢查特定的屬性。

• 安全檢查
• 不變量
• 參數(shù)化的檢查
• 檢查Rust程序的功能正確性

Rust Klee還沒有準備好用于生產(chǎn)，但它仍然值得一提，它是一個很酷的工具，可以幫助在Rust生態(tài)系統(tǒng)中形成正式的驗證環(huán)境。

5，Haybale

Haybale也是一個符號執(zhí)行引擎，具有與Rust Klee相似的功能，Haybale完全是用Rust編寫的，并且在底層基于Rust LLVM IR。

作為一個符號執(zhí)行引擎，它專注于將整個程序變量轉(zhuǎn)換為數(shù)學表達式，并對執(zhí)行路徑進行推理，以檢測錯誤或漏洞。Haybale最好的部分是它可以測試你的Rust代碼，而不需要添加額外的測試代碼。

讓我們看一個檢查函數(shù)foo是否返回0的例子。首先，我們寫出要分析的函數(shù)，你可以用任何編程語言寫這個，然后把它轉(zhuǎn)換成字節(jié)碼：

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

字節(jié)碼將保存在項目的某個地方，你可以在Rust代碼的項目變量中引用它：

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

現(xiàn)在，我們可以使用haybale中的find_zero_of_func方法來發(fā)現(xiàn)當函數(shù)接收到零輸入時存在的錯誤。

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可以對整個代碼進行推理，發(fā)現(xiàn)bug，并返回一份報告，證明代碼是否存在bug。雖然Haybale可能不會捕獲所有錯誤，但它很可能會捕獲導致運行時崩潰的嚴重錯誤，并給你一個修復它們的機會。

總結(jié)

自動驗證工具對于發(fā)現(xiàn)軟件開發(fā)中的bug非常重要，盡管它們可能尚未被開發(fā)人員廣泛采用。這些工具可以發(fā)現(xiàn)使用傳統(tǒng)測試方法無法發(fā)現(xiàn)的錯誤，并且可以提高代碼的可靠性。