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

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

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

驗證挑戰(zhàn)

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

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

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

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

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

DO-178B 測試覆蓋率分析

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

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

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

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

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

（B1然后B2）或者B3

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

在 A 級，需要 MC/DC：

· 程序中的每個條件都必須通過真假測試來執(zhí)行。

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

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

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

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

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

源與對象覆蓋

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

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

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

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

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

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

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

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

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

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

覆蓋分析

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

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

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

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

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

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

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

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

（B1然后B2）或者B3

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

表 1：（B1 和 B2）或 B3 的對象分支覆蓋測試。

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

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

把它們放在一起

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

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

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

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

審核編輯：郭婷