6月iOS設備好評榜：第一蟬聯榜首近一年
作為安兔兔各種榜單里變化最小的那個，2023年6月的iOS好評榜和上個月相比沒有任何排名上的變化，僅僅是部分設備好評率的下降，長年累月的用戶評價和逐漸退出市場的老款機器讓這
自動驗證是一種有助于檢查程序是否滿足某些屬性的技術，例如內存安全性和避免在運行時錯誤。此外，自動驗證工具使你能夠驗證并發代碼的正確性，這很難手工測試。
自動驗證對Rust特別重要，因為它可以幫助確保正確使用unsafe的代碼。在這篇文章中，我們將討論五個最常用的Rust驗證工具，以及它們如何幫助你構建更可靠的軟件。
我們將討論的第一個工具是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并導致崩潰的輸入。
注意：通過模糊測試發現的一些錯誤可能在現實生活中不實用或不適用，這意味著模糊測試可能會產生誤報。此外，模糊測試可能是資源密集型的，特別是在對大型或復雜的代碼庫進行模糊測試時。
Kani是一個現代的自動代碼驗證工具，可以幫助你在幾秒鐘內驗證Rust代碼的正確性。它使用一種稱為模型檢查的技術，一種探索程序所有狀態的方法，包括通過正常執行無法到達的狀態。
模型檢查允許Kani檢測代碼中的問題，這些問題可能是由意外的邏輯引起的。還可以使用Kani來識別單元測試、集成測試甚至手工測試很難或不可能發現的問題。
通過以下命令安裝Kani：
cargo install --locked kani-verifiercargo 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來識別這個潛在的問題允許您要么立即更改數據類型，要么保持原樣，如果錯誤是預期的行為，則適當地處理錯誤。
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了。
雖然屬性測試可以很好地用于選定的輸入范圍，但它有時會遺漏一些邊緣情況，并給你一個假結果。換句話說，它可能會在實際上沒有錯誤的情況下產生錯誤，或者在指定的覆蓋范圍之外找不到錯誤。
KLEE是一個符號執行引擎，它智能地探索程序中的所有代碼路徑，以發現漏洞或錯誤。它建立在LLVM編譯器基礎設施之上，該基礎設施是用C和C++編寫的。
因此，大多數KLEE實現也是用C和C++語言實現的。然而，KLEE的基本概念可以在任何編程語言中實現。
Rust Klee是Klee的開源Rust實現，被設計用來檢查特定的屬性。
Rust Klee還沒有準備好用于生產，但它仍然值得一提，它是一個很酷的工具，可以幫助在Rust生態系統中形成正式的驗證環境。
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非常重要，盡管它們可能尚未被開發人員廣泛采用。這些工具可以發現使用傳統測試方法無法發現的錯誤，并且可以提高代碼的可靠性。
本文鏈接：http://www.www897cc.com/showinfo-26-79831-0.htmlRust的五個自動驗證工具，你知道幾個？
聲明：本網頁內容旨在傳播知識，若有侵權等問題請及時與本網聯系，我們將在第一時間刪除處理。郵件：2376512515@qq.com
下一篇： 15個值得推薦的開源免費圖像標注工具
Copyright ? 2016-2023 天津谷騏科技有限公司 版權所有 sitemap.xml
違法及侵權請聯系：2376512515@qq.com 津ICP備18001702號
津公網安備 12010102000574號