在 1976 年電影“馬拉松人”中的一個懸疑場景中，一個虐待狂的納粹牙醫（勞倫斯·奧利維爾爵士）用他的各種工具擺出威脅性的姿勢。談到他來收集的一批被盜鉆石，奧利維爾反復問他害怕的俘虜（達斯汀霍夫曼），“它安全嗎？” 霍夫曼不知道這意味著什么，但他的無知遠非幸福，因為他遭受了未經麻醉的后果。

作為現代軟件的生產者，我們還需要面對這個問題，“它安全嗎？” 不知道答案很容易導致災難——即使它不會帶來牙齒折磨。實際上，軟件開發人員的問題不是“安全嗎？” 而是，“它足夠安全嗎？” 安全不是布爾條件；這是一個連續統一體，反映了我們對系統的安全特性得到滿足的信心。安全意味著安全，因為漏洞可以被利用來產生不可接受的危害。在最高的保證級別上，我們需要相應地高度確信我們的軟件做了它應該做的事情，而不做它不應該做的事情。

軟件安全和安保歷來在電子產品領域受到不同程度的關注。對這些要求的高度重視顯然與醫療器械相關；然而，有時會發生重大失誤，造成傷害或死亡。在 1980 年代的 Therac-25 放射治療機事件中，并發活動之間的“競爭條件”導致要進行大量放射治療，幾年前，胰島素輸液泵的軟件缺陷也導致劑量不當，有時甚至是致命的劑量。

在更一般的小型電子產品領域中，軟件的安全和安保要求是相當新的。以前，此類系統中的軟件相對簡單，設備通常是獨立的，并且通過機械手段強制執行安全性。但如今，該軟件執行的功能越來越復雜，連接到互聯網的“智能”設備可以被遠程控制。

本文重點介紹了軟件開發人員需要面對的主要問題，重點關注DO-178C認證標準（機載系統和設備認證中的軟件注意事項）作為一個行業方法的示例。DO-178C 中的指南并非專門針對航空，文章建議如何將其調整到需要高度保證的其他領域。

大圖 圖 1摘自 DO-178C 中的一個圖，顯示了 系統生命周期過程 與 軟件和硬件生命周期過程之間的關系。關鍵要點是，必須在系統級別確定安全（以及隱含的安全）要求和責任，但要得到其他生命周期過程的反饋。每個軟件組件都有一個相應的軟件級別（也稱為開發保證級別，或 DAL），基于該組件的異常行為對飛機持續安全運行的影響。正如Rick Hearn在 2016 年 10 月號 電子產品中關于 DO-254 的文章中所述，A 級是最苛刻的，因為異常行為可能會導致災難性故障，從而導致飛機失事。

許多標準為執行系統生命周期過程提供了推薦做法，例如ARP 4754A和IEC 61508。危害和安全評估方法包括官方標準中提出的方法，例如ARP 4761。

可以在通用標準中找到安全功能和保證要求的目錄。保證要求分為評估保證級別 （EAL），最高級別 （EAL 7） 要求對安全功能進行形式驗證。更具體地說，一個國際工作組已經準備好 DO-326A（適航安全流程規范），以“增強當前的飛機認證指南，以處理故意未經授權的電子交互對飛機安全的威脅?！?此類系統級分析可作為 DO-178C 流程的輸入，但反過來可能會受到 DO-178C 活動反饋的影響。

軟件工程常識 DO-178C 面向飛機軟件供應商，包含與各種軟件生命周期過程相關的特定目標形式的指南。組件的 DAL 確定哪些目標是相關的、配置管理控制的嚴格性以及負責實現目標和驗證目標是否已實現的各方是否需要獨立。目標列在一組表格中，詳細信息請參考文檔正文；作為說明， 圖 2 顯示了表 A-5 中的目標 6。

系統提供商需要通過提供各種工件（“數據項”）來證明符合目標，這些工件將由國家機構認證機構授權的指定工程代表 （DER） 進行審查。在接受數據項后，系統被認為是經過認證的。

圖 3 顯示 DO-178C 的主要元素；即各種軟件生命周期過程，包括規劃、開發和幾個相關的“整體”過程。這不是火箭科學。本質上，該標準是軟件工程常識的實例化。任何軟件都是針對一組需求設計和實現的，因此開發包括從系統需求中細化軟件需求（高級和低級），并可能梳理出額外的（“派生的”）需求，指定軟件架構，并實現設計。每個步驟都需要驗證（其中一個不可或缺的過程）。例如，軟件需求是否完整且一致？實施是否滿足要求？驗證涉及可追溯性：

補充實際開發過程的是各種外圍活動。該軟件不僅僅是代碼、數據和文檔的靜態集合；它隨著檢測到的缺陷、客戶變更請求等而發展。因此，完整的過程包括配置管理和質量保證，并且定義良好的程序至關重要。

DO-178C 不偏向或反對任何特定的軟件開發方法。盡管它似乎面向新的開發工作，但可以采用現有系統并追溯執行相關活動以獲取必要的數據項。該標準還處理諸如商業現貨 （COTS） 組件的合并和使用服務歷史來獲得認證信用等問題。

軟件驗證 DO-178C 中的大部分指南都涉及驗證：審查、分析和測試的組合，以證明每個軟件生命周期過程的輸出相對于其輸入是正確的。在 A 級軟件的 71 個總目標中，43 個適用于驗證，其中一半以上涉及源代碼和目標代碼。出于這個原因，DO-178C 有時被稱為“正確性”標準而不是安全標準；通過認證獲得的主要保證是對軟件滿足其要求的信心。代碼驗證目標的重點是測試。

但是測試有一個眾所周知的內在缺陷。正如已故計算機科學家 Edsger Dijkstra 所說，它可以顯示 bug 的存在，但永遠不會顯示它們的缺失。DO-178C 通過多種方式緩解了這個問題：

? 通過檢查和分析增強測試，以增加及早發現錯誤的可能性。

? DO-178C 要求進行基于需求的測試，而不是“白盒”或單元測試。每個需求都必須有相關的測試，執行正常處理和錯誤處理，以證明需求得到滿足并且無效輸入得到了正確處理。測試的重點是系統應該做什么，而不是每個模塊的整體功能。

? 源代碼必須完全被基于需求的測試所覆蓋。不允許使用“死代碼”（測試未執行且不符合要求的代碼）。

? 代碼覆蓋目標適用于 DAL C 的語句級別。在更高的 DAL 中，需要更精細的粒度，在完整的布爾表達式（“決策”）及其原子成分（“條件”）級別也需要覆蓋。DAL B 需要決策覆蓋（測試需要同時驗證真假結果）。DAL A 需要修改條件/決策覆蓋。給定決策的一組測試必須滿足以下條件 ： o 對于決策中的每個條件，條件在某些測試中為真，在另一個測試中為假；和 o 每個條件都需要獨立影響決策的結果。也就是說，對于每個條件，必須有兩個測試，其中： 》 一個條件為真，另一個條件為假， 》 其他條件在兩個測試中具有相同的值， 》 兩個測試中的決定結果是不同的。

MC/DC 測試將檢測某些類型的邏輯錯誤，這些錯誤不一定會出現在決策覆蓋范圍內，但如果在多條件決策中需要 True 和 False 的所有可能組合，則不會出現測試的指數爆炸式增長。它還具有強制開發人員制定明確的低級需求的好處，這些需求將適用于各種條件。

圖 4 顯示了與示例“if”語句的不同級別的源代碼覆蓋相關的可能測試用例集。

軟件方法學 軟件方法學 的進步為驗證帶來了機遇和挑戰：

? 基于模型的開發以圖形語言表達控制邏輯，自動生成源代碼，可能與手動生成的代碼混合。鑒于該計劃的多種形式，尚不清楚哪些目標適用于哪種形式。

? 面向對象編程的主要特性——繼承、多態性和動態綁定——引發了包括代碼覆蓋率和時間和空間可預測性在內的目標問題。

? 對于最高級別的安全關鍵性，應用形式化方法可以幫助提高保證（例如，證明沒有運行時錯誤等安全屬性）并消除對一些低級別需求測試的需要。但是，目前尚不清楚如何向認證機構證明正式證明可以取代此類測試。

這些問題是修訂早期 DO-178B 標準的主要動力，它們在 DO-178C 的補充中得到了解決：

? DO-331用于基于模型的開發和驗證， ? DO-332用于面向對象技術和相關技術，以及 ? DO-333用于形式方法。

工具鑒定 工具在軟件生命周期中有一系列用途。一些輔助驗證，例如檢查源代碼是否符合編碼標準、計算最大堆棧使用量或檢測對未初始化變量的引用。其他影響可執行代碼，例如基于模型的設計的代碼生成器。工具可以節省大量勞動力，但我們需要確信它們的輸出是正確的；否則，我們將不得不手動驗證輸出。

使用 DO-178C，我們通過稱為工具鑒定的過程獲得了這種信心，這基本上證明了該工具滿足其操作要求。所需的工作量——所謂的工具認證級別，或 TQL——取決于工具將要處理的軟件的 DAL 以及在存在工具缺陷：

? 標準1：工具輸出是機載軟件的一部分，工具可能會插入錯誤。 ? 標準2：該工具可能無法檢測到錯誤，其輸出用于減少其他開發或驗證活動。 ? 標準3：該工具可能無法檢測到錯誤。

TQL 的重要性范圍從 5（最低）到 1（最高）。TQL-1 適用于滿足標準 1 的工具，用于 DAL A 的軟件。大多數靜態代碼分析工具將采用 TQL-4 或 TQL-5。

輔助標準DO-330（工具鑒定注意事項）定義了與各種 TQL 相關的特定目標、活動和數據項。DO-330 可與其他軟件標準結合使用；它不是特定于 DO-178C。

有什么問題？ 盡管已經發生了一些危急關頭，但迄今為止，還沒有發現軟件出現故障的商用飛機事故造成人員傷亡。所以 DO-178C（及其前身 DO-178B）似乎很有效。盡管如此，還是出現了一些問題。

正確是否意味著安全？ 如上所述，DO-178C 確實是一個正確性標準，可以確保軟件滿足其要求。這如何轉化為整體系統安全性以及由此產生的低故障概率？約翰·拉什比 （ John Rushby） 的一篇論文認為，機載系統的成功記錄與其說歸功于軟件標準，不如說歸功于該行業的企業安全文化以及技術相對不頻繁的變化。其他行業使用 DO-178C 指南可能不會產生相同的好處。

軟件正確性和系統安全之間的關系確實不是那么簡單；許多因素會影響飛機或任何其他基于計算機的系統的整體安全（例如，也許最明顯的是，操作員的培訓和技能）。然而，即使代碼正確性顯然不足以實現安全，但在電傳操縱等沒有“B 計劃”后備的情況下，這是必要的。即使暫時忽略安全問題，許多行業中的錯誤軟件也可能導致代價高昂的召回，從而產生直接的財務成本并損害公司的聲譽。底線：對代碼正確性有信心的原則和實踐值得遵循，因為它們可以幫助挽救生命和金錢。

認證過程是否不必要地繁重？ 系統認證并不便宜。應將注意力集中在出現最嚴重問題的領域；即，在需求階段而不是在編碼級別。一個自然的問題是是否可以以更低的成本實現 DO-178C 的優勢。系統供應商和美國國會都提出了這個成本與收益的問題，因為機載軟件的安全認證過程被認為對新進入者來說過于復雜，但未能充分解決如何處理新方法和新技術。FAA 負責調查此問題的工作組舉辦了簡化保證流程研討會在 2016 年 9 月，他們提出了三個高級別的“總體屬性”，這些屬性可能構成更簡單的認證方法的基礎：

? 意圖——定義的預期功能對于所需的系統行為是正確和完整的。 ? 正確性——在可預見的操作條件下，就其定義的預期功能而言，實施是正確的。 ? 必要性——所有實施要么是所定義的預期功能所要求的，要么沒有不可接受的安全影響。

正在進行的這項工作可能會導致用于認證機載軟件的替代框架。

經驗教訓 總之，DO-178C 中的指南主要用于提供軟件滿足其要求的信心——而不是驗證要求實際上反映了系統的預期功能。因此，獲得正確的代碼是不夠的，但這是必要的，而且 DO-178C 方法的許多好處可以在不經過正式認證的情況下實現。以下是一些建議：

? 注意整個軟件生命周期。源代碼版本控制和配置管理可能看起來并不性感，但它們是必不可少的。實施源簽入“掛鉤”（例如，調用靜態分析工具來強制執行代碼質量的某些方面）并定期安排完整的回歸測試運行。實施處理缺陷報告和變更控制的流程，以便在不引入新問題的情況下提供軟件更新。確保已知問題有解決方法。

? 審查 DO-178C 中的目標并決定要達到的目標。在沒有官方認證的情況下，不需要提供各種數據項，但是如果故意遺漏某個目標，請確保您了解遺漏的原因以及不遵守可能造成的后果。

? 使用能夠及早發現潛在問題的編程語言。如 DO-178C 第 4.4 節所述：

基本原則是選擇限制引入錯誤機會的需求開發和設計方法、工具和編程語言，以及確保檢測到引入的錯誤的驗證方法。

Ada 編程語言特別適用 ，因為它旨在促進健全的軟件工程實踐，并強制執行檢查以防止諸如“緩沖區溢出”和整數溢出等弱點。該語言的最新版本 Ada 2012 包括一個特別相關的功能，稱為基于合同的編程，它有效地將低級軟件需求嵌入到源代碼中，可以在其中靜態驗證它們（使用適當的工具支持）或在運行時（使用編譯器生成的檢查）。

? 無論選擇哪種語言，都要選擇適合您應用程序需求的子集。C、C++、Ada 和 Java 等通用語言提供的特性在高保證上下文中可能存在問題。一個特性可能容易出錯，它的語義可能沒有完全指定，或者它可能需要復雜的運行時支持。選擇并執行合適的子集（或 DO-178C 用語中的“軟件代碼標準”）。

例如，MISRA-C中的規則旨在解決 C 語言的各種有問題的特性。但是，某些 MISRA 規則是不可檢查的（例如，文檔要求），而其他規則可能會以不同的方式執行（例如，禁止懸空引用）。在 Ada 中，稱為“pragma Restrictions”的標準功能允許程序員指定要禁止的功能。因此，相關子集可以按 點菜的 方式定義，幾乎所有的限制都由編譯時而不是運行時檢查強制執行。Ada 語言標準還定義了一組對并發（任務）特性的特定限制，稱為Ravenscar 配置文件。 Ravenscar 任務子集的表現力足以在實踐中使用，但對于安全或安全認證系統來說足夠簡單。

? 考慮高保證應用的正式方法?；谛问交椒ǖ撵o態分析工具可以證明程序屬性（包括安全性和安全性），范圍從不存在運行時錯誤到符合正式規定的要求。使用這些工具提供了基于數學的保證，同時也消除了對一些基于需求的低級測試的需要。

一個例子是Frama C技術，它可以證明 C 程序的屬性，盡管在 C 中普遍使用指針是一個挑戰。SPARK是 Ada 的一個形式上可分析的子集；諸如指針和異常等難以分析的特性不存在，證明技術可以利用 Ada 的基本特性，如強類型、標量范圍和基于合約的編程。

? 使用合格的工具自動化手動流程。靜態分析工具是你的朋友；除其他外，他們可以檢查編碼標準的合規性、計算復雜性指標，并檢測潛在的錯誤或潛在漏洞（例如對未初始化變量的引用、緩沖區溢出、整數溢出以及在沒有保護的情況下對共享變量的并發訪問）。用于識別此類錯誤的 Ada 靜態分析工具的一個示例是 AdaCore 的CodePeer. 要考慮的實用性包括可靠性（該工具是否檢測到它正在尋找的所有錯誤實例？），“誤報”率（報告的問題，實際上是真正的錯誤嗎？）和可用性（例如可擴展性到大系統，無需完整代碼庫即可分析系統部分的能力，以及易于集成到組織的軟件生命周期基礎架構中）。

對于動態分析，代碼覆蓋工具在源和對象級別都是必不可少的。該領域的典型技術會在可執行文件中生成特殊的跟蹤代碼，但這意味著真正的可執行文件與派生覆蓋數據的可執行文件不同。因此，需要額外的工作來證明為檢測的可執行文件和實際的可執行文件獲得的覆蓋結果是等效的。另一種方法是非侵入式的，編譯器與可執行文件分開生成源覆蓋義務數據。使用從具有適當跟蹤功能的目標板或儀表仿真環境生成的跟蹤數據，覆蓋工具可以識別和報告哪些源構造和目標代碼指令已經執行或未執行。GNATcoverage，它可以導出高達 MC/DC 的覆蓋率數據。

對于這些工具中的任何一個，資格證書都將提供更多的信心，并減少確認工具結果的額外工作的需要。

將 DO-178C 的原則應用到您的軟件生命周期過程中可能無法將您從邪惡的“馬拉松人”牙醫中解救出來，但是當與系統級安全原則結合使用時，它將幫助您自信地回答“是”問：“安全嗎？”