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

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

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

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

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

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

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

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

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

系統(tǒng)提供商需要通過提供各種工件（“數(shù)據(jù)項”）來證明符合目標，這些工件將由國家機構(gòu)認證機構(gòu)授權(quán)的指定工程代表 （DER） 進行審查。在接受數(shù)據(jù)項后，系統(tǒng)被認為是經(jīng)過認證的。

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

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

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

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

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

? 通過檢查和分析增強測試，以增加及早發(fā)現(xiàn)錯誤的可能性。

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

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

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

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

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

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

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

? 面向?qū)ο?a href="http://www.brongaenegriffin.com/v/tag/1315/" target="_blank">編程的主要特性——繼承、多態(tài)性和動態(tài)綁定——引發(fā)了包括代碼覆蓋率和時間和空間可預(yù)測性在內(nèi)的目標問題。

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

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

? DO-331用于基于模型的開發(fā)和驗證， ? DO-332用于面向?qū)ο蠹夹g(shù)和相關(guān)技術(shù)，以及 ? DO-333用于形式方法。

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

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

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

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

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

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

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

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

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

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

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

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

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

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

? 使用能夠及早發(fā)現(xiàn)潛在問題的編程語言。如 DO-178C 第 4.4 節(jié)所述：

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

Ada 編程語言特別適用 ，因為它旨在促進健全的軟件工程實踐，并強制執(zhí)行檢查以防止諸如“緩沖區(qū)溢出”和整數(shù)溢出等弱點。該語言的最新版本 Ada 2012 包括一個特別相關(guān)的功能，稱為基于合同的編程，它有效地將低級軟件需求嵌入到源代碼中，可以在其中靜態(tài)驗證它們（使用適當?shù)墓ぞ咧С郑┗蛟谶\行時（使用編譯器生成的檢查）。

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

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

? 考慮高保證應(yīng)用的正式方法?；谛问交椒ǖ撵o態(tài)分析工具可以證明程序?qū)傩裕òò踩院桶踩裕?，范圍從不存在運行時錯誤到符合正式規(guī)定的要求。使用這些工具提供了基于數(shù)學的保證，同時也消除了對一些基于需求的低級測試的需要。

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

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

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

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

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