C是Linux內(nèi)核中使用的主要語言，因具有無窮無盡的漏洞源而臭名昭著。只需查看模糊測試機器人syzbot自動報告的一長串開放錯誤，這些錯誤仍在等待修復(fù)。

小組討論圍繞著適合內(nèi)核開發(fā)的替代更安全的語言，如Ada和Rust，以及形式驗證的需求，以超越編譯器可以提供的保證。事實上，目前在Linux內(nèi)核上報告的許多內(nèi)存和安全漏洞都會在Ada或Rust中完全停止該程序，這只會稍微好一點。查看內(nèi)核補丁可以發(fā)現(xiàn)，通過在代碼上指定簡單的屬性可以檢測到許多問題，例如在哪種模式下哪些調(diào)用是合法的，應(yīng)該保留的數(shù)據(jù)類型不變量，以及如何使用適當(dāng)?shù)墓ぞ哽o態(tài)驗證它們。

令人驚訝的是，在討論中根本沒有提到MISRA C，盡管它已經(jīng)將自己確立為許多行業(yè)的必備品，以防止C語言的謬誤。MISRA C于1998年作為C的編碼標(biāo)準(zhǔn)出現(xiàn)，最初是汽車行業(yè)的編碼標(biāo)準(zhǔn)，并已進行了兩次修訂。當(dāng)前版本是 米斯拉 C：2012。它側(cè)重于避免 C 編程語言中容易出錯的功能，而不是強制實施特定的編程風(fēng)格。由Les Hatton撰寫的一項關(guān)于C編碼標(biāo)準(zhǔn)的研究發(fā)現(xiàn)，與十個典型的C編碼標(biāo)準(zhǔn)相比，MISRA C是唯一一個專注于避免錯誤而不是樣式執(zhí)行的標(biāo)準(zhǔn)，并且有很大的差距。

C編程語言的普及，以及它的許多陷阱和陷阱，導(dǎo)致了MISRA C在C用于高完整性軟件的領(lǐng)域中的巨大成功。這一成功促使工具供應(yīng)商提出了許多競爭性的MISRA C檢查器實現(xiàn)。工具在它們幫助執(zhí)行的MISRA C指南的覆蓋范圍上尤其相互競爭，因為不可能執(zhí)行MISRA C的所有16項指令和143條規(guī)則（統(tǒng)稱為指南）。

特別是，143 條規(guī)則中有 27 條是不可判定的，因此沒有工具可以始終檢測所有違反這些規(guī)則的行為，而不會同時報告不構(gòu)成違規(guī)的代碼的“誤報”。不可判定規(guī)則的一個例子是規(guī)則1.3：“不得發(fā)生未定義或關(guān)鍵的未指定行為。MISRA C：2012 的附錄 H 列出了 C 編程語言標(biāo)準(zhǔn)中數(shù)百個未定義和關(guān)鍵未指定行為的案例，其中大多數(shù)無法單獨確定。在大多數(shù)情況下，MISRA C檢查器忽略了規(guī)則1.3等不可判定的規(guī)則，盡管已知違反這些規(guī)則會對軟件質(zhì)量產(chǎn)生巨大影響。

但是，對于其他編程語言，可以使用靜態(tài)分析技術(shù)來解決這一挑戰(zhàn)，而不會使用戶被誤報淹沒。一個例子是由AdaCore，亞創(chuàng)和因里亞開發(fā)的SPARK工具集，它基于四個原則：

基礎(chǔ)語言Ada通過定義良好的語言標(biāo)準(zhǔn)、強類型和豐富的規(guī)范功能，為靜態(tài)分析提供了堅實的基礎(chǔ)。

Ada 的 SPARK 子集通過控制歧義的來源（如函數(shù)中的副作用和名稱的別名）來以基本方式限制基礎(chǔ)語言以支持靜態(tài)分析。

靜態(tài)分析工具主要在單個函數(shù)的粒度上工作，使分析更加精確，并最大限度地減少誤報的可能性。

靜態(tài)分析工具是交互式的，允許用戶在必要或需要時指導(dǎo)分析，并在無法證明用戶提供的合同時提供反例。

SPARK可以在C代碼庫中逐步采用，通過SPARK采用的五個級別和支持將形式分析（SPARK）與傳統(tǒng)基于測試的方法（C）相結(jié)合的“混合驗證”，逐步獲得保證。

火花石水平 - 基本保證

SPARK采用的第一個級別稱為石頭級別。它對應(yīng)于符合 Ada 的 SPARK 子集的代碼。僅采用此級別就可以保證許多無法對 C 強制執(zhí)行的一致性屬性。這些包括：

使用適當(dāng)?shù)拇虬到y(tǒng)，而不是C使用基于文本的文件，在翻譯單元之間沒有一致性要求;

嚴(yán)格且可讀的語法，強調(diào)清晰度并最小化“陷阱”，而不是C的非常寬松的語法，這使得編寫效果不是預(yù)期的程序變得容易，

遵守Ada和SPARK的強類型規(guī)則，而不是C的“糟糕的類型安全性，允許發(fā)生各種隱式類型轉(zhuǎn)換，這可能會損害安全性，因為它們的實現(xiàn)定義方面可能會導(dǎo)致開發(fā)人員混淆。（米斯拉C：2012，附件C）

MISRA C試圖通過各種指南來馴服C語言的這些可能的不一致。它特別定義了更強的類型規(guī)則（“基本類型模型”），并限制了函數(shù)參數(shù)/結(jié)果和控制結(jié)構(gòu)的使用。雖然這些避免了開發(fā)人員混淆的常見來源，但它們故意不是防彈的，否則它們會使大多數(shù)C程序非法。

這些基本保證在SPARK中很容易通過一個名為GNATprove的工具進行簡單的類似編譯器的分析來實現(xiàn)，這要歸功于定義ADA的SPARK子集的更強大的規(guī)則。

SPARK銀級 - 強大的安全保障

MISRA-C指南還旨在防止更細(xì)微的錯誤，讀取未初始化的數(shù)據(jù)，表達式中相互沖突的副作用以及未定義的行為，例如除以零或緩沖區(qū)溢出（這可能具有安全性和安全性后果）。所有這些都屬于不可判定規(guī)則的范疇，很少有MISRA C檢查器提供完整的檢測。

這些在SPARK采用的白銀級別上是完全被阻止的，這對應(yīng)于使用流程分析（達到稱為青銅的SPARK采用的第二級）和沒有運行時錯誤的證明（達到第三級，即白銀）來分析程序。要達到此級別，開發(fā)人員通常需要使用特定約束來定義類型，這些約束旨在支持這些約束，并為文件之間導(dǎo)出的函數(shù)提供合同 - 使用所謂的前提條件來指定調(diào)用方的義務(wù)，并使用后置條件來指定被調(diào)用方的義務(wù)。

達到白銀級的過程涉及與 IDE 的交互。開發(fā)人員可能在程序的子集上運行 GNATprove 工具，調(diào)查 GNATprove 診斷，相應(yīng)地更新程序，然后重復(fù)。GNATprove在每一步提供的詳細(xì)信息都有助于促進這種互動，以指導(dǎo)開發(fā)人員。以下是 GNATprove 顯示的消息示例：

在找到可能導(dǎo)致溢出的加法運算后，GNATprove給出了一個觸發(fā)問題的值的示例，這里是最大的整數(shù)值（在SPARK中表示為整數(shù)‘Last）?！皺z查原因”清楚地解釋了加法的結(jié)果應(yīng)該適合機器整數(shù)，如果 X 是加法前的最大整數(shù)值，則情況并非如此。然后，GNATprove建議向函數(shù)Incr添加一個合適的前提條件可能會解決這個問題，在這里指定X不能是最大值。

超越白銀級的火花

使用SPARK還有其他好處，遠(yuǎn)遠(yuǎn)超出了MISRA C檢查器可以提供的。在黃金和白金級別，開發(fā)人員通過 SPARK 合約指定程序的屬性，然后可以使用 GNATprove 來保證滿足這些屬性。開發(fā)人員還可以使用構(gòu)成 GNATprove 分析基礎(chǔ)的強大證明技術(shù)，使 GNATprove 警告能夠檢測死代碼（也是 MISRA C 追求的目標(biāo)）和代碼中的不一致。

結(jié)論

從本質(zhì)上講，MISRA C追求的所有目標(biāo)都可以在SPARK中最好地實現(xiàn)，它結(jié)合了更強大的基礎(chǔ)語言（Ada）和強大的分析工具（GNATprove）。計劃使用 MISRA C 規(guī)則的開發(fā)人員可以通過對其部分應(yīng)用程序采用 SPARK 來獲得更高的保證。

MISRA C中的規(guī)則代表了在關(guān)鍵應(yīng)用程序中提高C代碼可靠性的令人印象深刻的集體努力，重點是避免容易出錯的功能，而不是強制實施特定的編程風(fēng)格。然而，在基本層面上，MISRA C仍然建立在基礎(chǔ)語言之上，而這種基礎(chǔ)語言并不是真正以支持大型高保證應(yīng)用程序為目標(biāo)而設(shè)計的。很難將可靠性，安全性和安全性改造成一種從一開始就沒有這些目標(biāo)的語言。

由于C仍將是像Linux內(nèi)核這樣的大型程序的基礎(chǔ)語言，我們可以預(yù)見兩種趨勢的共存，以更好地防止C程序中的謬誤，其中MISRA C可以發(fā)揮作用，并用更安全的語言（如Rust和SPARK Ada）取代C作為部分代碼。汽車行業(yè)的主要參與者已經(jīng)開始走上后一條道路，如英偉達和捷太格特。

審核編輯：郭婷