商業航空電子設備的 DO-178B 等認證標準要求有證據表明系統源代碼完全通過源自需求的測試來執行。傳統工具通過代碼檢測來獲取覆蓋率數據，但這會使分析變得復雜，因為被測試的代碼并不是最終將執行的代碼。

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

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

驗證挑戰

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

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

· 目標硬件：雖然最終的軟硬件集成測試必須在實際部署的配置上進行，但在組件開發過程中需要目標板既昂貴又不方便。基于主機的解決方案更簡單且更具成本效益。

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

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

DO-178B 測試覆蓋率分析

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

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

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

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

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

（B1然后B2）或者B3

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

在 A 級，需要 MC/DC：

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

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

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

MC/DC 并不要求每個決策都使用其構成條件的每個可能的真值組合進行測試。這對于復雜的決策是不現實的，并且在條件耦合時（當相同的輸入變量出現在多個條件中時）可能是不可能的。

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

圖 1：程序片段顯示了不同種類的 DO-178B 結構覆蓋。

源與對象覆蓋

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

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

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

通過虛擬化進行目標仿真

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

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

QEMU 是可以擴展以提供附加功能的開源技術。為了處理 DO-178B 要求的結構覆蓋分析，一個有用的增強是支持生成執行跟蹤。兩種跟蹤信息是相關的：

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

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

生成這些執行跟蹤的 QEMU 的改編版本是覆蓋分析技術的關鍵組成部分。

覆蓋分析

盡管執行跟蹤數據提供了對象指令覆蓋率和對象分支覆蓋率信息，但仍需要進一步分析以滿足 DO-178B 的覆蓋率目標：

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

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

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

· 調試信息（DWARF），它將每個目標代碼指令與源代碼位置（文件、行、列）相關聯。

· Source Coverage Obligations （SCO），它提供了計劃結構的簡潔表示，需要證明實現某些覆蓋目標的證據。SCO 捕獲程序中所有決策的結構。

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

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

（B1然后B2）或者B3

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

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

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

當提出目標代碼覆蓋率作為 MC/DC 的證據時要解決的其他問題記錄在多個認證機構報告中［8，第 20 節］。

把它們放在一起

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

圖 2：虛擬化和覆蓋分析準確評估結構覆蓋。

這些工具目前適用于用 Ada 編寫的應用程序，Ada 是一種在安全關鍵領域中經常使用的語言。未來版本將支持其他語言，包括 C。目前支持的目標架構包括 PowerPC 和 LEON。

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

審核編輯：郭婷