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

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

但是，對(duì)于其他編程語(yǔ)言，可以使用靜態(tài)分析技術(shù)來(lái)應(yīng)對(duì)這一挑戰(zhàn)，而不會(huì)使用戶(hù)誤報(bào)淹沒(méi)。一個(gè)例子是由AdaCore，Altran和Inria開(kāi)發(fā)的SPARK工具集，它基于四個(gè)原則：

基礎(chǔ)語(yǔ)言 Ada 通過(guò)定義明確的語(yǔ)言標(biāo)準(zhǔn)、強(qiáng)大的類(lèi)型化和豐富的規(guī)范功能為靜態(tài)分析提供了堅(jiān)實(shí)的基礎(chǔ)。

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

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

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

SPARK 可以在 C 代碼庫(kù)中逐步采用，通過(guò)SPARK 采用的五個(gè)級(jí)別以及支持將形式分析 （SPARK） 與傳統(tǒng)的基于測(cè)試的方法 （C） 相結(jié)合的“混合驗(yàn)證”來(lái)逐步獲得保證。

火花石等級(jí) - 基本保證

SPARK采用的第一級(jí)稱(chēng)為石頭級(jí)。它對(duì)應(yīng)于符合 Ada 的 SPARK 子集的代碼。僅采用此級(jí)別即可保證許多無(wú)法對(duì) C 強(qiáng)制執(zhí)行的一致性屬性。其中包括：

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

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

遵守 Ada 和 SPARK 的強(qiáng)類(lèi)型規(guī)則，而不是 C 的“糟糕的類(lèi)型安全性，允許發(fā)生廣泛的隱式類(lèi)型轉(zhuǎn)換，這可能會(huì)損害安全性，因?yàn)樗鼈兊膶?shí)現(xiàn)定義方面可能會(huì)導(dǎo)致開(kāi)發(fā)人員混淆。（MISRA C：2012，附件C）

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

這些基本保證在SPARK中很容易實(shí)現(xiàn)，通過(guò)一個(gè)名為GNATprove的工具進(jìn)行簡(jiǎn)單的類(lèi)似編譯器的分析，這要?dú)w功于定義Ada的SPARK子集的更強(qiáng)大的規(guī)則。

SPARK 銀級(jí) - 強(qiáng)大的安全和安保保證

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

在 SPARK 采用的銀牌級(jí)別完全可以防止這些情況，這對(duì)應(yīng)于通過(guò)流分析（達(dá)到稱(chēng)為銅牌的 SPARK 采用的第二級(jí)）和證明沒(méi)有運(yùn)行時(shí)錯(cuò)誤（達(dá)到第三級(jí)，即白銀）來(lái)分析程序。要達(dá)到此級(jí)別，開(kāi)發(fā)人員通常需要定義具有特定約束的類(lèi)型，這些約束旨在支持和提供文件之間導(dǎo)出的函數(shù)的協(xié)定 - 使用所謂的前提條件來(lái)指定調(diào)用方的義務(wù)，以及后置條件來(lái)指定被調(diào)用方的義務(wù)。

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

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

超越銀級(jí)的火花

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

結(jié)論

從本質(zhì)上講，MISRA C追求的所有目標(biāo)都可以在SPARK中最好地實(shí)現(xiàn)，結(jié)合更強(qiáng)大的基礎(chǔ)語(yǔ)言（Ada）和強(qiáng)大的分析工具（GNATprove）。計(jì)劃使用 MISRA C 規(guī)則的開(kāi)發(fā)人員可以通過(guò)在其部分應(yīng)用程序中采用 SPARK 來(lái)增強(qiáng)安全性。

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

由于 C 仍將是像 Linux 內(nèi)核這樣的大型程序的基礎(chǔ)語(yǔ)言，我們可以預(yù)見(jiàn)兩種趨勢(shì)的共存，以更好地防止 C 程序中的錯(cuò)誤，MISRA C 可以發(fā)揮作用，并用更安全的語(yǔ)言（如 Rust 和 SPARK Ada ）替換 C 作為部分代碼。

審核編輯：郭婷