K60至尊版剛預(yù)熱 一加Ace2 Pro正面硬剛
Redmi這邊剛?cè)缁鹑巛钡男麄髁薑60 Ultra的各種技術(shù)和硬件配置，作為競(jìng)品的一加也坐不住了。一加中國(guó)區(qū)總裁李杰發(fā)布了兩條微博，表示在自家的一加Ace2上早就已經(jīng)采用了和PixelWo
自動(dòng)驗(yàn)證是一種有助于檢查程序是否滿足某些屬性的技術(shù)，例如內(nèi)存安全性和避免在運(yùn)行時(shí)錯(cuò)誤。此外，自動(dòng)驗(yàn)證工具使你能夠驗(yàn)證并發(fā)代碼的正確性，這很難手工測(cè)試。
自動(dòng)驗(yàn)證對(duì)Rust特別重要，因?yàn)樗梢詭椭_保正確使用unsafe的代碼。在這篇文章中，我們將討論五個(gè)最常用的Rust驗(yàn)證工具，以及它們?nèi)绾螏椭銟?gòu)建更可靠的軟件。
我們將討論的第一個(gè)工具是cargo-fuzz，它使用一種稱為模糊測(cè)試的技術(shù)來進(jìn)行自動(dòng)化軟件測(cè)試。通過向程序提供許多有效的、幾乎有效的或無效的輸入，模糊測(cè)試可以幫助開發(fā)人員找到不希望看到的行為或漏洞。
當(dāng)我們編寫測(cè)試時(shí)，我們通常只考慮一些正常輸入，并根據(jù)我們對(duì)系統(tǒng)反應(yīng)的想象來編寫測(cè)試。這種方法可能會(huì)導(dǎo)致遺漏錯(cuò)誤，特別是那些由意外的或不正確的輸入引起的錯(cuò)誤。
模糊測(cè)試可以通過為程序提供各種各樣的輸入(包括無效的和意外的輸入)來幫助你找到這些遺漏的錯(cuò)誤。如果程序在響應(yīng)這些輸入時(shí)崩潰或行為異常，則表示存在錯(cuò)誤。
cargo-fuzz crate可以對(duì)Rust代碼進(jìn)行模糊測(cè)試，它的工作原理是生成隨機(jī)輸入，并將它們輸入到要測(cè)試的函數(shù)中。如果函數(shù)出現(xiàn)故障或崩潰，cargo-fuzz將保存導(dǎo)致故障的輸入。
通過以下命令安裝cargo-fuzz：
cargo install cargo-fuzz下面是一個(gè)如何使用cargo-fuzz對(duì)Rust函數(shù)進(jìn)行模糊測(cè)試的例子：
#![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解析器提供隨機(jī)輸入來測(cè)試它。fuzz_target將持續(xù)被調(diào)用，直到遇到觸發(fā)panic并導(dǎo)致崩潰的輸入。
注意：通過模糊測(cè)試發(fā)現(xiàn)的一些錯(cuò)誤可能在現(xiàn)實(shí)生活中不實(shí)用或不適用，這意味著模糊測(cè)試可能會(huì)產(chǎn)生誤報(bào)。此外，模糊測(cè)試可能是資源密集型的，特別是在對(duì)大型或復(fù)雜的代碼庫進(jìn)行模糊測(cè)試時(shí)。
Kani是一個(gè)現(xiàn)代的自動(dòng)代碼驗(yàn)證工具，可以幫助你在幾秒鐘內(nèi)驗(yàn)證Rust代碼的正確性。它使用一種稱為模型檢查的技術(shù)，一種探索程序所有狀態(tài)的方法，包括通過正常執(zhí)行無法到達(dá)的狀態(tài)。
模型檢查允許Kani檢測(cè)代碼中的問題，這些問題可能是由意外的邏輯引起的。還可以使用Kani來識(shí)別單元測(cè)試、集成測(cè)試甚至手工測(cè)試很難或不可能發(fā)現(xiàn)的問題。
通過以下命令安裝Kani：
cargo install --locked kani-verifiercargo kani setup讓我們看一下下面的代碼：
fn product(a: i32, b: i32) -> i32 { a * b}上面的代碼是有效的Rust代碼，對(duì)嗎？花點(diǎn)時(shí)間再看一遍——你能發(fā)現(xiàn)這段代碼有什么可能出錯(cuò)的地方嗎？
讓我們用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);}運(yùn)行結(jié)果：
圖片
Kani在乘法過程中發(fā)現(xiàn)了溢出的可能性。
這是因?yàn)閜roduct函數(shù)不能確保我們不超過i32的最大值，即2,147,483,647，任何大于該數(shù)的值都會(huì)拋出錯(cuò)誤。本質(zhì)上，無論這個(gè)函數(shù)用于什么，它都不能處理大于20億的數(shù)字。
在這種情況下，使用Kani來識(shí)別這個(gè)潛在的問題允許您要么立即更改數(shù)據(jù)類型，要么保持原樣，如果錯(cuò)誤是預(yù)期的行為，則適當(dāng)?shù)靥幚礤e(cuò)誤。
Proptest使用大量有效和無效的輸入來測(cè)試函數(shù)的屬性，以發(fā)現(xiàn)bug。這與單元測(cè)試等經(jīng)典測(cè)試方法不同，在單元測(cè)試中，指定一些輸入并根據(jù)期望的行為添加斷言。
屬性測(cè)試是模糊測(cè)試的一種形式，它更容易控制，更側(cè)重于驗(yàn)證特定的屬性。這使得它成為測(cè)試復(fù)雜系統(tǒng)的一個(gè)很好的選擇，在這些系統(tǒng)中，傳統(tǒng)的模糊測(cè)試可能太慢或無效。
讓我們來看看如何使用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); }}在上面的代碼中，我們正在測(cè)試一個(gè)簡(jiǎn)單的函數(shù)，它將兩個(gè)數(shù)字相加。這樣一個(gè)簡(jiǎn)單的函數(shù)可能會(huì)出什么問題呢？
讓我們看一下test_add_two_numbers函數(shù)簽名：
fn test_add_two_numbers(first_number in any::<i32>(), second_number in any::<i32>())any::<i32>()是一個(gè)Protest中的類型，它生成隨機(jī)的i32值，包括有效的和無效的。這允許我們使用廣泛的輸入來測(cè)試add_two_numbers()函數(shù)，包括邊緣情況和異常情況。
Proptest測(cè)試函數(shù)將為first_number和second_number參數(shù)生成大量隨機(jī)輸入。如果任何測(cè)試失敗，Proptest將把失敗的輸入打印到控制臺(tái)。
圖片
報(bào)告顯示有溢出的可能，它還顯示了最小的可重復(fù)輸入。有了這些信息，我們就可以繼續(xù)修復(fù)bug了。
雖然屬性測(cè)試可以很好地用于選定的輸入范圍，但它有時(shí)會(huì)遺漏一些邊緣情況，并給你一個(gè)假結(jié)果。換句話說，它可能會(huì)在實(shí)際上沒有錯(cuò)誤的情況下產(chǎn)生錯(cuò)誤，或者在指定的覆蓋范圍之外找不到錯(cuò)誤。
KLEE是一個(gè)符號(hào)執(zhí)行引擎，它智能地探索程序中的所有代碼路徑，以發(fā)現(xiàn)漏洞或錯(cuò)誤。它建立在LLVM編譯器基礎(chǔ)設(shè)施之上，該基礎(chǔ)設(shè)施是用C和C++編寫的。
因此，大多數(shù)KLEE實(shí)現(xiàn)也是用C和C++語言實(shí)現(xiàn)的。然而，KLEE的基本概念可以在任何編程語言中實(shí)現(xiàn)。
Rust Klee是Klee的開源Rust實(shí)現(xiàn)，被設(shè)計(jì)用來檢查特定的屬性。
Rust Klee還沒有準(zhǔn)備好用于生產(chǎn)，但它仍然值得一提，它是一個(gè)很酷的工具，可以幫助在Rust生態(tài)系統(tǒng)中形成正式的驗(yàn)證環(huán)境。
Haybale也是一個(gè)符號(hào)執(zhí)行引擎，具有與Rust Klee相似的功能，Haybale完全是用Rust編寫的，并且在底層基于Rust LLVM IR。
作為一個(gè)符號(hào)執(zhí)行引擎，它專注于將整個(gè)程序變量轉(zhuǎn)換為數(shù)學(xué)表達(dá)式，并對(duì)執(zhí)行路徑進(jìn)行推理，以檢測(cè)錯(cuò)誤或漏洞。Haybale最好的部分是它可以測(cè)試你的Rust代碼，而不需要添加額外的測(cè)試代碼。
讓我們看一個(gè)檢查函數(shù)foo是否返回0的例子。首先，我們寫出要分析的函數(shù)，你可以用任何編程語言寫這個(gè)，然后把它轉(zhuǎn)換成字節(jié)碼：
fn foo(x: f64) -> f64 { x * x - 4.0}字節(jié)碼將保存在項(xiàng)目的某個(gè)地方，你可以在Rust代碼的項(xiàng)目變量中引用它：
let project = Project::from_bc_path("/path/to/file.bc").unwrap();現(xiàn)在，我們可以使用haybale中的find_zero_of_func方法來發(fā)現(xiàn)當(dāng)函數(shù)接收到零輸入時(shí)存在的錯(cuò)誤。
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可以對(duì)整個(gè)代碼進(jìn)行推理，發(fā)現(xiàn)bug，并返回一份報(bào)告，證明代碼是否存在bug。雖然Haybale可能不會(huì)捕獲所有錯(cuò)誤，但它很可能會(huì)捕獲導(dǎo)致運(yùn)行時(shí)崩潰的嚴(yán)重錯(cuò)誤，并給你一個(gè)修復(fù)它們的機(jī)會(huì)。
自動(dòng)驗(yàn)證工具對(duì)于發(fā)現(xiàn)軟件開發(fā)中的bug非常重要，盡管它們可能尚未被開發(fā)人員廣泛采用。這些工具可以發(fā)現(xiàn)使用傳統(tǒng)測(cè)試方法無法發(fā)現(xiàn)的錯(cuò)誤，并且可以提高代碼的可靠性。
本文鏈接：http://www.tebozhan.com/showinfo-26-79831-0.htmlRust的五個(gè)自動(dòng)驗(yàn)證工具，你知道幾個(gè)？
聲明：本網(wǎng)頁內(nèi)容旨在傳播知識(shí)，若有侵權(quán)等問題請(qǐng)及時(shí)與本網(wǎng)聯(lián)系，我們將在第一時(shí)間刪除處理。郵件：2376512515@qq.com
上一篇： .NET Core 服務(wù)實(shí)現(xiàn)監(jiān)控可觀測(cè)性優(yōu)秀實(shí)踐
Copyright ? 2016-2023 天津谷騏科技有限公司 版權(quán)所有 sitemap.xml
違法及侵權(quán)請(qǐng)聯(lián)系：2376512515@qq.com 津ICP備18001702號(hào)
津公網(wǎng)安備 12010102000574號(hào)