[發明專利]一種基于圖爾敏模式的軟件安全性論證方法

無效

• 申請號: 201210232486.2
• 申請日: 2012-07-05
• 公開（公告）號: CN102779253A
• 公開（公告）日: 2012-11-14
• 發明（設計）人: 曾福萍;張大健;王栓奇;陸民燕
• 申請（專利權）人: 北京航空航天大學
• 主分類號: G06F21/00
• 分類號: G06F21/00
• 代理公司: 暫無信息
• 代理人: 暫無信息

技術領域

本發明屬于軟件安全性工程領域，涉及其中的軟件安全性論證方法，具體涉及一種基于圖爾敏模式的軟件安全性論證方法。

背景技術

安全性是指不發生導致人員傷亡、職業病、設備損壞或財產損失的意外事件的能力。安全關鍵系統（Safety-Critical?System）的控制和安全防護是計算機的一個非常重要的應用領域。隨著安全關鍵系統中軟件（被稱為安全軟件（Safety-Critical?Software））比重的增加，軟件也存在安全性問題，因此，安全關鍵軟件在投入使用前對其進行認證，判定是否達到了系統所要求的安全性是一項基本要求。

目前，對于軟件安全性論證國內外不同行業有不同的標準，例如民航的DO-178B[1]、鐵路的EN?50128[2]、美軍的NASA-STD-8719[3][4]及三軍聯合手冊[5]等。這些軟件安全性標準從實際可操作的角度更加深入地認識到保證軟件系統安全的難度。由于技術的不成熟，目前標準中很少包含軟件的定量（基于概率的）安全性論證，而是定義了軟件安全認證所需的實踐。雖然這些標準在提倡的技術和驗證的方法等一些細節上存在不一致，但論證的基本原理是一致的：根據提供軟件安全性工程過程的一些證據（Evidence）來表明軟件的安全性達到了相應的要求，這種面向過程的完全遵循標準的安全認證存在不足：一方面是要求遵循的開發過程、工具和技術與軟件失效率的降低之間沒有必然的聯系，是如何滿足軟件安全性要求并不清楚；另一方面容易造成這樣的誤解：軟件安全性由標準的制定者負責，而不是軟件的開發方。

圖爾敏模式[6]是非形式邏輯刻畫日常論證的一種重要方式，是由英國的非形式邏輯奠基人圖爾敏提出的。圖爾敏提出了一個由主張(claim)、資料(data)、正當理由(warrants)、支援(backing)、限定詞(qualifier)和反駁(rebuttal)等6個功能要素構成的過程性模式,稱為圖爾敏論證模式。其中,主張、資料和正當理由作為圖爾敏論證模式的基本證中都必須出現,構成了論證的基本模式。支援、限定詞和反駁對于所有的論證來說并非必然出現,稱為補充要素。隨著非形式邏輯研究在我國的興起，越來越多的學者已經關注圖爾敏模式。

發明內容

本發明為了克服現有的軟件安全性論證方法的不足，將圖爾敏模式的論證思想運用到軟件安全性論證領域，以安全性目標（Claim）為核心，軟件安全性工程活動為事實證據（Evidence），鏈接安全性目標與證據是正當理由（Warrant），說明事實證據是如何支持目標的成立；而事實證據則是支持正當理由，為正當理由提供事實依據。本發明給軟件安全性論證提供了一個全新的、有效的視角。

本發明提供了一種基于圖爾敏模式的軟件安全性論證方法，該方法包括以下步驟：

步驟1：提出軟件安全性論證目標（Claim），即試圖在軟件安全性論證中證明為已經滿足的結論。

步驟2：提供支持軟件安全性論證目標的事實證據（Data）。如果受到質疑，則需要轉入步驟3，否則轉入步驟5。

步驟3：給出賦予該‘事實證據’具有導出‘軟件安全性論證目標’結論的資格的推論規則，即“正當理由(Warrants)”。如果受到質疑，則轉入步驟4，否則轉入步驟5。

步驟4：明確正當理由背后起保證作用的支援（Backing），用于強化正當理由權威性的支援性陳述。

步驟5：給出“軟件安全性目標”實現程度的限定詞（Qualifier）。

步驟6：如果存在，給出阻止從正當理由得出目標成立、具有保留機能的陳述的例外情況或反駁（Rebuttal）。

所屬步驟1中的軟件安全性論證目標是一個斷言或斷定（assertion），是用來指所陳述的、試圖在論證中證明成立的結論的術語。軟件安全性論證目標是二元的，只能成立或不成立，不存在第三種情況。如“代碼中不存在死循環”。這就是正確的軟件安全性論證目標，而“代碼中存在多少錯誤”就不是一個正確的目標，因為它是無法去論證的。

為了更好地理解所屬步驟1中的軟件安全性目標，可以在軟件安全性目標確定時補充有助于理解的相關附屬信息，包括軟件安全性論證目標所提時的背景信息、包含的術語及縮略語等。目標要被論證，那么它就不能讓人存有疑問，必須對目標涉及的所有需要解釋的術語進行實例化。如目標“軟件的安全性是可接受的嗎？”，為了更好地論證目標，就需要對“軟件”、“可接受”兩個概念做出界定。