Categories
程式開發

ZetZ:受Rust啟發的C方言


ZetZ(或簡稱ZZ),是一種受Rust啟發的C方言,它能夠在虛擬機編譯時象徵性地執行代碼,從而形式化驗證代碼。

ZZ針對的是那些在接近底層硬件的位置上運行的軟件,但它也可用於構建跨平台、符合ANSI-C標準的庫。實際上,ZZ充當了C代碼的轉譯器,然後將其輸入到任何標準的C編譯器中。與許多現代語言更強調安全性不同,ZZ並不排除或限制那些被認為“不安全”的特性,例如原始指針訪問。相反,它使用靜態單賦值形式( static single assignment form,SSA),在編譯時通過諸如yices2z3之類的SMT定理證明器(SMT prover)來證明我們的代碼是沒有未定義行為(undefined behavior)的。

下面的代碼片段展示了ZZ代碼的寫法:

using ::{printf}

export fn main() -> int {
    let r = Random{
        num: 42,
    };
    printf("your lucky number: %un", r.gen());
    return 0;
}

struct Random {
    u32 num;
}

fn gen(Random *self) -> u32 {
    return self->num;
}

為了防止任何未定義的行為洩漏到我們的代碼中,ZZ要求所有內存訪問都是正確的。例如,數組索引需要使用where關鍵字告訴編譯器被訪問的索引是有效的,該關鍵字允許我們指定調用方必須滿足的約束:

fn bla(int * a)
    where len(a) >= 3
{
    a[2];
}

類似地,可以使用model關鍵字指定對函數行為的約束:

fn bla(int a) -> int
    model return == 2 * a
{
    return a * a;           //-- This would fail here
}

為了做到這些,ZZ在C語法上添加了許多約束,使其更適合形式化檢查。例如,ZZ強制執行 east-constness ,並通過函數類型啟用函數指針。

InfoQ採訪了ZZ的創建者和維護者Avid Picciani,以進一步了解更多關於ZZ的信息。

InfoQ:您能描述一下您的背景和目前從事的專業工作嗎?

Picciani:我的背景是大眾硬件領域,具體來說,我參與過諾基亞的所有Linux手機項目。

目前,我是devguard.io的創始人。我們提供了雲下的物聯網管理工具以實現數據主權。

讓開發人員興奮不已的殺手級特性是carrier shell,它允許我們在不配置任何網絡的情況下,向數百萬台設備打開一個遠程shell。只需一個ed25519標識,我們就可以與任何物理網絡背後的任何設備通信,當然也有對等加密,我們也不會看到或存儲任何數據。

我們發布了大約25萬台Rust設備,但是我們想要擴展到更低層次的嵌入式設備中,Rust不能也不想將這些設備作為目標。

InfoQ:您能介紹下ZZ是怎麼誕生的嗎?

Picciani:為了向更低級別的硬件(ESP32,一個AVR 8位)提供我們的產品,我們需要能夠實現極高存儲效率和可移植性的工具。但是放棄Rust語言,轉回C語言讓我感到有點難過。這裡的每個人都很喜歡Rust, 而且C充滿了陷阱。

與此同時,存在許多我們需要但在Rust中無法使用的C語言商業工具,比如用於模糊芯片的編譯器和監管審批流程。

ZZ是一個為期6個月研究的成果,我們努力從現在的計算機科學領域中探索編程的改進途徑。具體來說,它的靈感來自於微軟研究(比如F和Z3)。它只是將其轉換成為一種更實用的語言。我們在devguard上也使用了F,特別是用於加密用途。同樣值得一提的是Alloy,它激發了我們基於反例(counter-example)檢查的想法。

InfoQ:ZZ的主要優勢是什麼?可用於什麼場景?可以將其視為通用語言還是利基語言?

Picciani:雖然Rust有一種使編程更安全的魔法彈(只是不允許可變借入兩次),但ZZ實際上只是C之上的一層。我們可以做任何我們想做的不安全的事情,只要我們另外為它編寫一個形式化驗證即可。這是一種非常獨特的編程方式,更像是與一位數學教授進行結對編程,他不斷地向外拋出極端情況,在這些情況下,我們的代碼將會崩潰。

形式化驗證可能會非常枯燥和冗長,因此ZZ並不是一種真正的通用編程語言。我們完全可以用ZZ編寫一個web服務,事實上我們也這樣做了,但它永遠無法與NodeJS這樣的快速開發特性相匹敵。但當我們將alloy直接集成到狀態機生成器中時,這種情況可能會改變,這時我們可能希望嘗試在ZZ中實現安全性至關重要的Web應用程序。

InfoQ:您如何看待ZZ目前的成熟狀態?

Picciani:不管怎樣,ZZ是一個非常新的概念,它的兩大功能(C語言轉換器和符號驗證)仍然需要在細節上進一步充實。今天它已經可以使用,我鼓勵人們嘗試用它來構建東西,但是要做好面對許多編譯器關鍵錯誤和重大語言變更的準備。對於商業代碼,我建議大家謹慎地將ZZ和Rust一起使用,特別是ZZ非常適合與C系統代碼交互。

我的公司devguard.io將在4月左右發布一款用於無雲汽車遙測的新產品,該產品主要是在Zephyr OS 和Nordic NRF91的基礎上基於ZZ構建的,因此我們在全力投入其中。 ZZ中最大的開源代碼庫可能是devguard carrier中的ZZ分支。完成之後,我覺得ZZ就可以投入生產了。

要使用ZZ,需要安裝Rust以進行引導,並提供一個.toml文件,Rust包管理器Cargo使用該文件來編譯代碼。

原文鏈接:

ZetZ is a Formally Verified Dialect of C