C 是 Linux 內核中使用的主要語言，因漏洞無窮無盡而臭名昭著。只需查看由模糊機器人 syzbot 自動報告的一長串未解決的錯誤，這些錯誤仍在等待修復。

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

令人驚訝的是，在討論中根本沒有提到 MISRA C，盡管它已成為許多行業(yè)的必備工具，以防止 C 語言的錯誤。MISRA C 于 1998 年作為 C 的編碼標準出現(xiàn)，最初用于汽車行業(yè)，經過兩次修訂。當前版本是 MISRA C:2012。它側重于避免 C 編程語言容易出錯的特性，而不是強制執(zhí)行特定的編程風格。Les Hatton編寫的 C 編碼標準研究發(fā)現(xiàn)，與十種典型的 C 編碼標準相比，MISRA C 是唯一一個專注于避免錯誤而不是風格強制的標準，而且差距很大。

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

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

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

基礎語言 Ada 通過定義明確的語言標準、強類型和豐富的規(guī)范特性為靜態(tài)分析提供了堅實的基礎。

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

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

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

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

SPARK Stone Level - 基本保證

SPARK 采用的第一級稱為 Stone Level。它對應于符合 Ada 的 SPARK 子集的代碼。僅僅采用這個級別就可以保證許多 C 語言無法強制執(zhí)行的一致性屬性。其中包括：

使用適當?shù)陌到y(tǒng)，而不是 C 使用基于文本的文件包含，并且沒有跨翻譯單元的一致性要求；

嚴格且易讀的語法強調清晰并最大限度地減少“陷阱”，而不是 C 的非常寬松的語法，這使得編寫效果與預期不符的程序變得容易，

遵守 Ada 和 SPARK 的強類型規(guī)則，而不是 C 的“較差的類型安全性 ［that］ 允許發(fā)生廣泛的隱式類型轉換 ［which］ 可能會損害安全性，因為它們的實現(xiàn)定義方面可能會導致開發(fā)人員混淆。 “（MISRA C:2012，附件 C）

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

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

SPARK 銀級 - 強大的安全保障

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

這些在 SPARK 采用的 Silver 級別上完全被阻止，這對應于使用流分析（達到 SPARK 采用的第二級，稱為 Bronze）和不存在運行時錯誤的證明（達到第三級，即銀）。為了達到這個水平，開發(fā)人員通常需要定義具有特定約束的類型，這些約束旨在支持和提供文件之間導出的函數(shù)的合同——使用所謂的前置條件來指定調用者的義務，并使用后置條件來指定調用者的義務。被叫方的義務。

達到 Silver 級別的過程涉及與 IDE 的交互。開發(fā)人員可能在程序的子集上運行 GNATprove 工具，調查 GNATprove 診斷，相應地更新程序，然后重復。GNATprove 在每一步都提供了詳細的信息來指導開發(fā)人員，從而促進了此類交互。以下是 GNATprove 顯示的消息示例：

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

SPARK 超越白銀級

使用 SPARK 還有其他好處，遠遠超出 MISRA C 檢查器所能提供的。在 Gold 和 Platinum 級別，開發(fā)人員通過 SPARK 合同指定程序的屬性，然后可以使用 GNATprove 來保證這些屬性將得到滿足。開發(fā)人員還可以啟用 GNATprove 警告以檢測死代碼（也是 MISRA C 追求的目標）和代碼中的不一致，使用構成 GNATprove 分析基礎的強大證明技術。

結論

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

MISRA C 中的規(guī)則代表了一項令人印象深刻的集體努力，旨在提高關鍵應用程序中 C 代碼的可靠性，重點是避免容易出錯的功能，而不是強制執(zhí)行特定的編程風格。然而，從根本上說，MISRA C 仍然建立在一種基礎語言之上，而這種語言并不是真正為支持大型高保證應用程序而設計的。很難將可靠性、安全性和安全性改造成一門從一開始就沒有這些目標的語言。

由于 C 仍將是 Linux 內核等大型程序的基礎語言，我們可以預見兩種趨勢的共存，以更好地防止 C 程序中的錯誤，其中 MISRA C 可以發(fā)揮作用，并用更安全的語言（如 Rust 和SPARK Ada 用于部分代碼。

審核編輯：郭婷