商業(yè)航空電子設(shè)備的 DO-178B 等認(rèn)證標(biāo)準(zhǔn)要求有證據(jù)表明系統(tǒng)源代碼完全通過(guò)源自需求的測(cè)試來(lái)執(zhí)行。傳統(tǒng)工具通過(guò)代碼檢測(cè)來(lái)獲取覆蓋率數(shù)據(jù)，但這會(huì)使分析變得復(fù)雜，因?yàn)楸粶y(cè)試的代碼并不是最終將執(zhí)行的代碼。

主機(jī)駐留兩部分技術(shù)提供了一種高效且具有成本效益的替代解決方案：目標(biāo)仿真器與非侵入式覆蓋分析器相結(jié)合。模擬器不是解釋器；相反，它將目標(biāo)代碼動(dòng)態(tài)轉(zhuǎn)換為本地主機(jī)指令。因此，測(cè)試套件通常比在實(shí)際目標(biāo)硬件上執(zhí)行得更快。覆蓋分析器從從模擬器上的程序執(zhí)行中檢索到的對(duì)象分支信息中獲取源覆蓋數(shù)據(jù)，并執(zhí)行符合最嚴(yán)格覆蓋要求所需的任何附加分析。

簡(jiǎn)化目標(biāo)平臺(tái)的最終驗(yàn)證；它需要重新運(yùn)行測(cè)試并顯示結(jié)果與模擬器上的相同。這種方法完全支持 DO-178B 及其即將修訂的 DO-178C 的所有級(jí)別的安全認(rèn)證。

驗(yàn)證挑戰(zhàn)

DO-178B 等安全認(rèn)證標(biāo)準(zhǔn)中規(guī)定的一項(xiàng)主要驗(yàn)證活動(dòng)是測(cè)試覆蓋率分析，這涉及證明每個(gè)軟件需求都得到滿足，并表明基于需求的測(cè)試完全覆蓋了源代碼。覆蓋率分析提出了幾個(gè)問(wèn)題：

· 插裝：一種常見(jiàn)的方法是使用生成應(yīng)用程序源代碼的修改（插裝）版本的工具，或者使用特殊開(kāi)關(guān)編譯應(yīng)用程序以生成插裝目標(biāo)代碼。添加的代碼包含對(duì)適當(dāng)日志記錄函數(shù)的調(diào)用。但是，檢測(cè)代碼不是將在最終系統(tǒng)上運(yùn)行的代碼。要使用覆蓋數(shù)據(jù)，開(kāi)發(fā)人員必須證明它也適用于未檢測(cè)的可執(zhí)行文件。這不一定是一項(xiàng)簡(jiǎn)單的任務(wù)。

· 目標(biāo)硬件：雖然最終的軟硬件集成測(cè)試必須在實(shí)際部署的配置上進(jìn)行，但在組件開(kāi)發(fā)過(guò)程中需要目標(biāo)板既昂貴又不方便?；谥鳈C(jī)的解決方案更簡(jiǎn)單且更具成本效益。

· 源代碼與對(duì)象覆蓋率： DO-178B 要求源代碼覆蓋率，但覆蓋率數(shù)據(jù)是根據(jù)執(zhí)行程序計(jì)算得出的。在最高安全關(guān)鍵性（A 級(jí)）下，可能需要進(jìn)行特殊分析來(lái)證明修改后的條件/決策覆蓋率 （MC/DC）。

此處描述的技術(shù)解決了這些問(wèn)題。它基于從運(yùn)行未檢測(cè)版本的應(yīng)用程序軟件的主機(jī)駐留目標(biāo)仿真器生成的執(zhí)行跟蹤數(shù)據(jù)中獲取源覆蓋率指標(biāo)。

DO-178B 測(cè)試覆蓋率分析

DO-178B 規(guī)定了兩種類型的測(cè)試覆蓋分析 ［1， §6.4.4］：

· 基于需求的測(cè)試覆蓋分析：開(kāi)發(fā)人員必須展示從每個(gè)需求到實(shí)現(xiàn)需求的源代碼以及測(cè)試套件的可追溯性，該套件的執(zhí)行提供了正確實(shí)現(xiàn)需求的信心。

· 結(jié)構(gòu)覆蓋分析：開(kāi)發(fā)人員必須證明代碼結(jié)構(gòu)已經(jīng)完全通過(guò)基于需求的測(cè)試。如果這些測(cè)試沒(méi)有完全覆蓋源代碼，那么開(kāi)發(fā)人員必須添加更多需求、添加更多測(cè)試和/或刪除代碼——稱為“死代碼”（DO-178B）或“無(wú)關(guān)代碼”代碼”（DO-178C）——不能追溯到需求。

所需覆蓋范圍取決于軟件組件的安全關(guān)鍵級(jí)別。在 C 級(jí)，只需要聲明覆蓋率；即程序中的每條語(yǔ)句必須至少執(zhí)行一次。

在 B 級(jí)，需要決策覆蓋。在 DO-178B 用語(yǔ)中，決策是一個(gè)完整的布爾表達(dá)式，由原子布爾項(xiàng)（條件）和布爾運(yùn)算符組成。例如，以下布爾表達(dá)式是具有三個(gè)條件的決策：

（B1然后B2）或者B3

此示例使用 Ada和 then和或 else短路形式，僅在必要時(shí)評(píng)估其右操作數(shù)，分別對(duì)應(yīng)于 && 和 || C 中的運(yùn)算符。決策覆蓋要求程序中的每個(gè)決策都通過(guò)真假測(cè)試來(lái)執(zhí)行。

在 A 級(jí)，需要 MC/DC：

· 程序中的每個(gè)條件都必須通過(guò)真假測(cè)試來(lái)執(zhí)行。

· 程序中的每一個(gè)決定都必須經(jīng)過(guò)真假測(cè)試。

· 必須證明每個(gè)條件獨(dú)立地影響決策的結(jié)果（該條件變化，而所有其他條件保持不變）。

MC/DC 并不要求每個(gè)決策都使用其構(gòu)成條件的每個(gè)可能的真值組合進(jìn)行測(cè)試。這對(duì)于復(fù)雜的決策是不現(xiàn)實(shí)的，并且在條件耦合時(shí)（當(dāng)相同的輸入變量出現(xiàn)在多個(gè)條件中時(shí)）可能是不可能的。

圖 1 顯示了一個(gè)程序片段，說(shuō)明了各種結(jié)構(gòu)覆蓋之間的差異。MC/DC 具有一些微妙的特征，在 Hayhurst等人［2］ 的教程和Chilenski ［3］ 的詳細(xì)研究中進(jìn)行了全面討論。

圖 1：程序片段顯示了不同種類的 DO-178B 結(jié)構(gòu)覆蓋。

源與對(duì)象覆蓋

DO-178B 中一個(gè)通常被誤解的要求涉及必須在 A 級(jí)證明的覆蓋類型（源代碼與目標(biāo)代碼）。第 6.4.4.2 節(jié)指出：

可以對(duì)源代碼執(zhí)行結(jié)構(gòu)覆蓋分析，除非軟件級(jí)別為 A 并且編譯器生成的目標(biāo)代碼不能直接追溯到源代碼語(yǔ)句。然后，應(yīng)該對(duì)目標(biāo)代碼執(zhí)行額外的驗(yàn)證，以建立這些生成的代碼序列的正確性。目標(biāo)代碼中編譯器生成的數(shù)組綁定檢查是不能直接追溯到源代碼的目標(biāo)代碼示例。

這一要求（其措辭在 DO-178C 中正在修訂）并不是說(shuō)必須為 A 級(jí)證明對(duì)象覆蓋。相反，它解決了源語(yǔ)言構(gòu)造的問(wèn)題，其編譯的目標(biāo)代碼包含條件分支或從源代碼。在這種情況下，開(kāi)發(fā)人員必須驗(yàn)證生成的代碼，例如通過(guò)解釋每個(gè)不可追蹤的目標(biāo)代碼序列的效果。但是覆蓋分析仍然必須與源代碼結(jié)構(gòu)相關(guān)。僅顯示目標(biāo)代碼覆蓋率是不夠的，除非進(jìn)一步分析可以證明其與源代碼覆蓋率等價(jià)。

通過(guò)虛擬化進(jìn)行目標(biāo)仿真

在主機(jī)系統(tǒng)上模擬目標(biāo)處理器的概念并不新鮮，但虛擬化技術(shù)的最新進(jìn)展催生了一種高效且可移植的方法，例如開(kāi)源 Quick EMUlator （QEMU） 工具。QEMU 支持客戶操作系統(tǒng)的完整系統(tǒng)仿真，并允許通過(guò)機(jī)器描述模擬特定的嵌入式設(shè)備。它在主機(jī)平臺(tái)上運(yùn)行，并在一個(gè)兩階段的過(guò)程中，使用緩存方案將目標(biāo)代碼動(dòng)態(tài)轉(zhuǎn)換為本地主機(jī)指令以提高效率。該工具首先將目標(biāo)代碼翻譯成中間語(yǔ)言，然后將中間表示編譯成主機(jī)二進(jìn)制指令。

動(dòng)態(tài)翻譯器一次對(duì)未插樁的目標(biāo)代碼段進(jìn)行操作，將翻譯（或高速緩存提取）與翻譯后的指令的執(zhí)行交錯(cuò)。當(dāng) QEMU 開(kāi)始處理一段目標(biāo)代碼時(shí)，它會(huì)將指令轉(zhuǎn)換為宿主代碼，直到它到達(dá)下一個(gè)分支。翻譯后的目標(biāo)代碼（稱為翻譯塊）存儲(chǔ)在緩存中（如果尚未存在），并執(zhí)行其相應(yīng)的主機(jī)指令。QEMU 然后繼續(xù)翻譯它停止的地方。由于緩存，目標(biāo)指令塊只需要解碼一次。在實(shí)踐中，由于主機(jī)處理器通常比嵌入式目標(biāo)硬件更快，QEMU 的虛擬化方法提供了比直接在目標(biāo)上執(zhí)行更好的性能。

QEMU 是可以擴(kuò)展以提供附加功能的開(kāi)源技術(shù)。為了處理 DO-178B 要求的結(jié)構(gòu)覆蓋分析，一個(gè)有用的增強(qiáng)是支持生成執(zhí)行跟蹤。兩種跟蹤信息是相關(guān)的：

· 摘要跟蹤：輸出標(biāo)識(shí)已執(zhí)行指令的地址范圍，以及對(duì)于條件分支，哪些分支被（被）采用。輸出數(shù)據(jù)的大小是有限的（實(shí)際上與目標(biāo)程序大小呈線性關(guān)系），因?yàn)樗伙@示執(zhí)行了哪些指令/分支，而不是整個(gè)執(zhí)行歷史。

· 指定地址范圍的完整歷史跟蹤：除了指示已執(zhí)行的指令外，輸出還顯示了在每次評(píng)估相關(guān)條件表達(dá)式時(shí)采用了哪個(gè)分支。輸出數(shù)據(jù)的大小取決于執(zhí)行歷史。

生成這些執(zhí)行跟蹤的 QEMU 的改編版本是覆蓋分析技術(shù)的關(guān)鍵組成部分。

覆蓋分析

盡管執(zhí)行跟蹤數(shù)據(jù)提供了對(duì)象指令覆蓋率和對(duì)象分支覆蓋率信息，但仍需要進(jìn)一步分析以滿足 DO-178B 的覆蓋率目標(biāo)：

· 跟蹤必須映射到源代碼結(jié)構(gòu)，尤其是源代碼中具有覆蓋要求的結(jié)構(gòu)（語(yǔ)句、決策、條件）。

· 必須評(píng)估所達(dá)到的覆蓋水平——聲明、決定、MC/DC。

為了啟用這種分析，編譯器可以在對(duì)象控制流圖中保留源程序的決策結(jié)構(gòu)并生成兩種輸出：

· 調(diào)試信息（DWARF），它將每個(gè)目標(biāo)代碼指令與源代碼位置（文件、行、列）相關(guān)聯(lián)。

· Source Coverage Obligations （SCO），它提供了計(jì)劃結(jié)構(gòu)的簡(jiǎn)潔表示，需要證明實(shí)現(xiàn)某些覆蓋目標(biāo)的證據(jù)。SCO 捕獲程序中所有決策的結(jié)構(gòu)。

使用來(lái)自仿真器的跟蹤數(shù)據(jù)以及編譯器提供的 DWARF 和 SCO 信息，覆蓋分析工具可以推斷測(cè)試的執(zhí)行是否達(dá)到了所需的覆蓋級(jí)別（語(yǔ)句、決策、MC/DC）。

確定執(zhí)行跟蹤數(shù)據(jù)是否暗示 MC/DC 存在一些挑戰(zhàn)。一個(gè)問(wèn)題是如何從對(duì)象分支覆蓋范圍推斷源條件評(píng)估。如果程序統(tǒng)一使用短路形式（“然后”、“或其他”）而不是非短路運(yùn)算符（“和”、“或”），則可以處理此問(wèn)題。根據(jù)選項(xiàng)的指示，編譯器在生成的目標(biāo)代碼中保留源代碼的條件結(jié)構(gòu)。第二個(gè)問(wèn)題是，出于效率原因，是否可以僅使用摘要跟蹤而不使用完整的歷史跟蹤。一般來(lái)說(shuō)，答案是“不”，一個(gè)相對(duì)簡(jiǎn)單的決定說(shuō)明了原因：

（B1然后B2）或者B3

該決策的目標(biāo)代碼可以僅由三個(gè)測(cè)試用例覆蓋，如表 1 所示。

表 1：（B1 和 B2）或 B3 的對(duì)象分支覆蓋測(cè)試。

但是，當(dāng)有n 個(gè)獨(dú)立條件時(shí)， MC/DC 至少需要n+1次測(cè)試，因此這里需要進(jìn)行 4 次（再次參見(jiàn)圖 1）。這意味著跟蹤摘要數(shù)據(jù)（對(duì)象分支覆蓋率）是不夠的；需要完整的歷史跟蹤數(shù)據(jù)。Bordin等人和 Comar等人［7］給出了何時(shí)對(duì)象分支覆蓋足以推斷 MC/DC 的數(shù)學(xué)表征。

當(dāng)提出目標(biāo)代碼覆蓋率作為 MC/DC 的證據(jù)時(shí)要解決的其他問(wèn)題記錄在多個(gè)認(rèn)證機(jī)構(gòu)報(bào)告中［8，第 20 節(jié)］。

把它們放在一起

目標(biāo)虛擬化方法已作為 Couverture （Coverage） 項(xiàng)目 的一部分實(shí)施，旨在為安全關(guān)鍵型軟件開(kāi)發(fā)的覆蓋分析提供一個(gè)開(kāi)放框架。AdaCore 的 GNATemulator 工具是對(duì) QEMU 的改編，用于收集執(zhí)行跟蹤數(shù)據(jù)。GNAT 編譯器編譯帶有開(kāi)關(guān)的應(yīng)用程序源程序，這些開(kāi)關(guān)保留目標(biāo)代碼中的條件控制流并生成 DWARF 和 SCO 數(shù)據(jù)。然后在 GNATemulator 上運(yùn)行未檢測(cè)的可執(zhí)行文件，生成執(zhí)行跟蹤數(shù)據(jù)。使用編譯器和仿真器生成的信息，GNATcoverage 工具評(píng)估是否已實(shí)現(xiàn)所需的結(jié)構(gòu)覆蓋。如有必要，該工具會(huì)分析完整的歷史跟蹤數(shù)據(jù)以驗(yàn)證 MC/DC。圖 2 描述了一個(gè)典型的開(kāi)發(fā)場(chǎng)景。

圖 2：虛擬化和覆蓋分析準(zhǔn)確評(píng)估結(jié)構(gòu)覆蓋。

這些工具目前適用于用 Ada 編寫的應(yīng)用程序，Ada 是一種在安全關(guān)鍵領(lǐng)域中經(jīng)常使用的語(yǔ)言。未來(lái)版本將支持其他語(yǔ)言，包括 C。目前支持的目標(biāo)架構(gòu)包括 PowerPC 和 LEON。

高效的目標(biāo)虛擬化，再加上一個(gè)從執(zhí)行跟蹤數(shù)據(jù)中推斷出精確的源級(jí)覆蓋率指標(biāo)的工具，用于非儀器化/未修改的用戶程序，標(biāo)志著現(xiàn)有技術(shù)的進(jìn)步。該技術(shù)在安全關(guān)鍵環(huán)境中特別有價(jià)值，支持各級(jí)安全認(rèn)證，同時(shí)簡(jiǎn)化認(rèn)證工作。

審核編輯：郭婷