劉 晗， 陶紅偉， 陳儀香*

1. 華東師范大學軟件工程學院，教育部軟硬件協同設計技術與應用工程研究中心，上海 200062 2. 鄭州輕工業(yè)大學計算機與通信工程學院，鄭州 450002

0 引 言

近年來，航天技術迅猛發(fā)展，軟件作為航天技術中必不可少的部分，其功能越來越復雜，規(guī)模越來越大，航天軟件已經成為人們關注和研究的重點之一.但是，作為安全攸關領域，航天軟件日益復雜化帶來很多潛在安全問題，一旦軟件發(fā)生事故，其損失無法估計.因此，航天軟件可信性研究不容忽視.

自1972年Anderson JP首次提出可信系統(tǒng)的概念[1]，人們便開始研究可信系統(tǒng).早期，人們對可信系統(tǒng)的研究主要集中在硬件環(huán)境和操作系統(tǒng)，直到美國國防部首先在可信計算機系統(tǒng)測評標準中提出可信計算機系統(tǒng)的軟件也要是可信的[2]，人們才更加關注軟件可信性.此后，LAPRIE[3]給出軟件可信性與可靠性的區(qū)別，認為軟件可靠性是可信性的一個子集，可信性比可靠性復雜得多.美國科學與技術委員會 (national science and technology council, NSTC)也在之后提出高可信系統(tǒng)[4]，他們認為高可信系統(tǒng)主要關注功能正確性、防危性、容錯性、實時性和安全性等性質，并且他們強調用戶體驗，認為高可信系統(tǒng)必須能在任何情況下都能按照用戶預期的情況運行.美國國家研究委員會(national research council, NRC)也認為可信系統(tǒng)需要強調用戶體驗，可信系統(tǒng)必須在任何情況下都能按照用戶預期的目標運行，但是他們提出的可信定義主要關注正確性、私密性、可靠性、防危性、可生存性和安全性，其中安全性包括機密性、完整性、可用性[5].德國奧爾登堡大學可信軟件研究院在2006年提出軟件可信性應該包括正確性、安全性、服務質量、保密性和隱私性，其中服務質量又包括可用性、可靠性和性能[6].

我國自2000年以來也有很多軟件可信研究團隊提出了軟件可信性定義.陳火旺院士認為高可信性質包括可靠性、防危性、安全性、可生存性、容錯性和實時性[7].劉克等[8]也認為可信性是軟件諸多屬性的綜合反映，提出可信軟件是指軟件系統(tǒng)的動態(tài)運行及其結果總是符合人們預期，并且在受到干擾時仍能提供連續(xù)服務.

由于軟件可信性是多種屬性的綜合反映，對其量化評估往往非常困難.國內外學者從各種不同角度提出一系列方法來度量評估軟件可信性.SANDRO等[9]通過將問卷調查和多元統(tǒng)計分析技術相結合的方法，建立兼顧主觀評價和客觀度量的軟件可信性度量模型.美國國家標準與技術研究院(National Institute of Standards and Technology, NIST)提出一個評估軟件可信性的初步框架，它以自上而下的方式，使用形式化的方法得出可信因素的確切數值[10-12].ALEXOPOULOS等[13]以貝葉斯概率和Dempster-Shafer證據理論為基礎，提出M-STAR模塊化軟件可信性體系結構框架.JIN等[14]提出一個可容納四個子度量標準的系統(tǒng)級信任度度量標準框架STRAM，該框架提供一種分層結構，其中每個子度量定義一個子本體.

國內許多研究團隊同樣在軟件可信性度量領域取得系列成果.鄭志明院士和李未院士等人將動力學統(tǒng)計分析引入到軟件可信性度量，通過動力學基本方法研究軟件可信性及其演化過程[15-17].楊善林院士等[18]將效用理論和Dempster-Shafer證據理論相結合，提出一種基于可信指標樹的證據推理算法.王懷民院士等[19]提出一種分層的軟件可信分級模型，并通過驗證方法對軟件進行評估.沈昌祥院士從軟件行為角度出發(fā)，提出基于并發(fā)理論的軟件可信性度量方法[20-21].王德鑫等[22]則專注于軟件過程，將可信證據融入軟件開發(fā)的全過程，建立基于過程的軟件可信度評估方法.田俊峰等[23]通過檢查點來捕獲軟件行為軌跡，并通過機器學習和余弦相似性的方法來預測軟件可信性.陳儀香等[24]則基于公理化方法，將軟件屬性進行分解，提出基于屬性分解的軟件可信度量模型.此外，陳儀香等人還通過Extensive結構，研究了面向源代碼的軟件可信性度量模型.

本文在文獻[24]的基礎上，從源代碼角度入手，建立面向航天型號軟件C語言可信證據規(guī)范，該證據規(guī)范區(qū)分關鍵證據和非關鍵證據以及可信正證據與可信負證據.此外，本文提出了一種面向源代碼可信證據的航天軟件可信度量模型和可信性分級模型，最后，本文在NASA開源軟件Core Flight Executive 上驗證了度量方法的有效性和實用性.

1 軟件失效模型與可信證據

1.1 軟件失效模型

文獻[25]中指出軟件失效是指程序動態(tài)運行結果與預期結果不一致，這種情況是在軟件運行過程中觸發(fā)軟件缺陷造成的.為了更好地描述這一過程，本文首先給出一個軟件失效模型來描述不同因素對軟件失效的影響，如圖1所示.

圖1 軟件失效模型Fig.1 Software failure model

軟件在編碼開發(fā)過程中難免會留下一些缺陷，這些缺陷在正常情況下不會影響軟件的預期功能，隨著時間的推移或者在某些外部干擾情況下，這些缺陷極有可能被激活，成為錯誤，導致軟件失效，從而使得軟件失信，其可信性降低.

1.2 可信證據

國防科技大學的Trustie團隊在文獻[26]中給出可信證據的一種定義，該定義指出任何與軟件相關并能反映其某種可信屬性的數據、文檔或者其他信息都稱為軟件可信證據.

由此可見，可信證據是軟件可信性的反映，而軟件可信性由軟件諸多屬性的綜合構成.本文主要面向源代碼來度量軟件可信性，因此，本文將軟件代碼中用來衡量軟件可信性的指標依據定義為可信證據.

定義1(源代碼可信證據).源代碼可信證據是指在軟件源代碼中用來衡量軟件可信性指標的依據，包括表達式類可信證據、聲明定義類可信證據、語句類可信證據和參數注釋類可信證據.

不同的可信證據對軟件可信性有著不同的影響，有些可信證據的出現可能會對軟件產生致命的影響，例如，航天類軟件代碼中一旦出現數組越界情況，軟件的運行便很可能偏離用戶預期.鑒于此，本文把證據分為關鍵證據和非關鍵證據，用來區(qū)分不同證據對軟件可信性的影響.

定義2(關鍵證據與非關鍵證據).關鍵證據是指源代碼中一旦出現或缺失會對軟件產生巨大影響的可信證據，非關鍵證據是除關鍵證據外的所有可信證據，其出現或缺失不會對軟件產生致命影響.

對于不同類別、不同應用場景的軟件，用戶所期望的預期結果往往不同，相應源代碼中會產生致命影響的證據也不完全相同，很難通過統(tǒng)一的關鍵證據集來衡量.因此，不同類型的軟件需要根據軟件自身的特性來定義關鍵證據和非關鍵證據.表1展示了三個不同類別軟件的關鍵證據.

表1 關鍵證據示例Tab.1 Examples of key evidence

通過關鍵證據和非關鍵證據，可以區(qū)分不同證據對軟件可信性的不同程度影響，并且可以建立應用于不同領域的可信證據.

此外，可信證據對軟件可信性的影響還有正面和負面兩種.因此本文還將可信證據分為正證據和負證據，正證據對軟件可信性有著正面影響，負證據對軟件可信性有著負面影響.

在軟件失效過程中，代碼中存在的缺陷可以被防護或者可以減輕其影響使得程序按照預期運行.這些防護措施或者減輕缺陷影響的方法的可信證據即為正證據.

定義3(正證據).正證據是指在源代碼中所有對缺陷進行防護或者使得缺陷不影響程序按照預期運行的可信證據，它與軟件可信性正相關，防護缺陷程度越高或者使得缺陷不影響程序按照預期運行的能力越大，軟件可信性就越高.正證據可以用如下的三元組表示：

PositiveEvidence=

其中，Name表示正證據的名稱，Metric表示正證據的度量元，分別用A、B、C、D四個等級表示，每一等級包含不同要求，MetricValue表示正證據的度量值，取值范圍為[1,10]，由度量元的評級映射得到，其中A級映射為10，B級映射為7，C級映射為4，D級映射為1.例如，表2展示了Name為“過程體、循環(huán)體、then/else中語句必須用括號括起”的正證據.

表2 正證據示例Tab.2 An example of positive evidence

代碼的缺陷受到外部干擾或者隨著時間推移，這些缺陷在沒有防護的情況下就可能導致軟件失效，從而使得軟件失信，這些缺陷所對應的證據即為負證據.

定義4(負證據).負證據是指隱藏在源代碼中使得軟件受到外部干擾和時間推移可能導致軟件失信的證據，它與軟件的可信性負相關，其風險程度越高，出現的次數越多，軟件的可信性越低，可以用如下的二元組表示：

NegativeEvidence=

其中，Name表示負證據的名稱，RiskValue為負證據的風險值，取值范圍為[1,10]，表示該負證據一旦被激活，所產生的負面影響，風險值越大，其產生的負面影響越大.例如，表3列舉了三個風險值不同的負證據.

表3 負證據示例Tab.3 Examples of negative evidence

本文在標準[27]給出的航天型號軟件C語言安全子集和文獻[24]中提出的面向源代碼的軟件可信規(guī)范基礎上，建立面向源代碼的航天型號軟件C語言可信證據規(guī)范.該可信證據規(guī)范分為表達式類、聲明定義類、語句類、參數與注釋類等四類，共109個正可信證據，其中，正證據共57個，負證據共52個，關鍵證據36個，非關鍵證據73個，具體各類數目如表4所示.

表4 負證據示例Tab.4 Trustworthy evidence statistics

2 面向源代碼的航天軟件可信性度量模型

2.1 面向源代碼的航天軟件可信性度量模型框架

為了便于從源代碼角度對航天軟件可信性進行度量，本文提出了一個面向C語言源代碼可信證據的航天軟件可信性度量模型框架.該框架如圖2所示，首先對源代碼進行分析，結合證據集，找出其中存在的正證據和負證據；根據基于正證據類的航天軟件可信性度量模型和基于負證據類的航天軟件可信度度量模型分別計算基于每類證據的軟件可信值；然后根據基于混合證據的航天軟件可信性度量模型對得到的可信值進行融合得到最終的軟件可信值；最后根據軟件可信性分級模型得到軟件的可信等級.

圖2 面向源代碼的航天軟件可信性度量模型框架Fig.2 Aerospace software trustworthiness measurement framework oriented to source code

2.2 基于正證據的航天軟件可信性度量模型

在面向源代碼的軟件可信性度量中，從源代碼出發(fā)得到正證據，這些正證據按照其特點劃分為多種類別，在本文中，我們將其劃分為4個類別，分別為表達式類、聲明定義類、語句類、參數與注釋類等4類.根據每類中每個關鍵正證據和其所占權重計算出關鍵正證據可信度量值，每個非關鍵正證據的度量值和其所占權重計算出非關鍵正證據的可信度量值，由此計算出這一類正證據的可信度量值，基于此本文給出如下基于正證據的航天軟件可信性度量模型.

假設正證據共有cp類，第p類正證據共有m個關鍵證據，s個非關鍵證據，則基于正證據類的航天軟件可信性度量模型計算公式為：

其中，α表示所有關鍵正證據在正證據中所占權重，β表示所有非關鍵正證據在正證據中所占權重，yi(1≤i≤m)為關鍵正證據可信度量值，yj(m+1≤j≤m+s)為非關鍵正證據可信度量值，αi為關鍵正證據ei在所有關鍵正證據中所占權重，βj為非關鍵正證據ej在所有非關鍵正證據中所占權重.

該模型符合文獻[24]中基于公理化方法所提出的非負性、比例合適性、單調性、凝聚性、靈敏性、替代性和可期望性7個度量屬性.該模型還符合“木桶原理”，即單個正證據的度量值較高，最終的度量值不一定很高，但是如果有一個正度量值很低，那么最終的度量值一定很低.

2.3 基于負證據的航天軟件可信性度量模型

負證據出現次數越多，軟件失效可能性就越大，軟件就越有可能向用戶預期之外的情況運行，軟件可信性就越低.此外，如果源代碼中出現的負證據風險值較高，該負證據被激活產生的影響就越大，軟件的可信性也就越低.因此，本文給出如下基于負證據的航天軟件可信性度量模型.

假設負證據共有cn類，第q類負證據集中共有l(wèi)條負證據，則此軟件在第q類負證據影響下的總風險值為：

(2)

其中，ni為負證據ei在程序中出現的次數，RiskValuei為負證據ei風險值.

軟件的風險值表示軟件會向用戶預期之外運行的風險程度，軟件風險值越大，軟件可信性就越小.文獻[28-29]中提出了一個基于失信證據的軟件可信性度量模型，本文在此基礎上，將軟件在該類負證據影響下的風險值SRValue作為自變量，該類負證據的可信度量值TNq作為因變量，可得到基于負證據的航天軟件可信性度量模型計算公式為

(3)

其中，λ為參數，用來調節(jié)軟件風險值對軟件可信性影響大小，一般選擇使用軟件行數來調節(jié)影響.

考慮到式(1)的取值范圍是[1,10],而式(3)的取值范圍是[0,1]，為了使得式(3)的取值范圍和式(1)一致，通過分段函數將軟件可信度的取值范圍映射到[1,10]，即

(4)

該模型綜合考慮了負證據的出現次數和其風險程度，而且當總風險值較低的情況下，其可信度隨總風險值下降幅度較大.反之，當總風險值較高的情況下，其可信度隨總風險值下降幅度較小.

2.4 基于混合證據的航天軟件可信性度量模型

軟件可信性是由源代碼中所有可信證據共同決定的，僅通過某類正證據或者某類負證據來度量軟件可信性都會忽略源代碼中很多要素，因此軟件可信性度量要綜合考慮軟件中所有可信證據.根據每類正證據和負證據所占的權重對正負證據所計算出的軟件可信值進行融合，得到基于混合證據的軟件可信值，然后根據每類證據所占的權重對各個類的正負證據所計算出的軟件可信值進行融合，得到基于混合證據的可信值.基于此，本文給出如下基于混合證據的航天軟件可信性度量模型.

(5)

其中，ωh為第h類證據所占權重，γ為參數，表示正證據和負證據對軟件可信度的不同影響.

該模型綜合考慮了正負證據的共同影響，而且在由各類證據可信度計算整體可信度時，計算公式同樣符合木桶原理.

3 軟件可信性分級模型

王靖等[30]在航天嵌入式軟件可信性評估時根據計算出的軟件整體可信值和各個屬性的可信值把軟件分為5個等級.在王婧等人的基礎上，結合之前所給出的計算模型和關鍵證據與非關鍵證據的定義，給出面向源代碼的軟件可信性分級模型，如表5所示，其中l(wèi)ine表示程序行數.

表5 軟件可信性分級模型Tab.5 Software trustworthy classification model

該軟件可信性分級模型滿足以下性質：

性質1.門限性

門限性是指某一可信等級的軟件可信值必須要達到此等級所要求最低可信值，其所有正證據都要達到某一等級，出現負證據的風險值不能超過最高要求的風險值.該性質表明要達到某一可信等級的軟件，除了其可信值需要達到要求以外，還需要滿足正證據的度量值不能太低，出現負證據的風險值不能太高.因此，僅僅某一個正證據度量值或負證據風險值改變不一定能提高軟件可信等級，還要提高可信值最低的正證據度量值和避免風險值較高的負證據出現.

性質2.關鍵性

關鍵性是指某一可信等級的軟件需要滿足其關鍵證據的可信值或總風險值要滿足一定的要求.由于不同類型的軟件關鍵證據和非關鍵證據不同，該性質對于不同類型提出了不同要求.

4 實驗與分析

NASA作為美國國家航空航天局，負責規(guī)劃和實施美國國家航天計劃，并展開科學研究.自其成立以來，NASA實施了多項成功的太空計劃，其成功必然離不開其高可信軟件.本文選取了NASA在代碼開源托管平臺Github上開源的Core Flight Executive代碼(https:∥github.com/nasa/cFE)，它是Core Flight System的框架組件.本節(jié)將以該系統(tǒng)代碼的msg模塊為度量對象，驗證本文所提出的面向源代碼的航天軟件可信性度量方法的有效性與實用性.該模塊代碼行數1256行，包含11個文件，文件結構如圖3所示.

圖3 文件結構Fig.3 File structure

4.1 證據提取

本文已經根據標準[27]和文獻[24]建立了面向航天嵌入式C語言代碼的可信證據規(guī)范，區(qū)分關鍵證據與非關鍵證據以及可信正證據與可信負證據.

本文首先依照可信正證據對該源代碼進行評估，得到各條正證據的評估結果，其結果如表6所示.其中表達式類共有13個證據被評為A，4個證據被評為B；聲明定義類共有10個證據被評為A，4個證據被評為B；語句類所有15個證據都被評為A；參數注釋類共有8個證據被評為A，2個證據被評為B.數組下標越界關鍵證據評為B，其他為A.

表6 正證據度量結果Tab.6 Positive Evidence measurement results

然后根據可信負證據，在源代碼中判斷負證據的出現次數，結果如表7所示.其中，表達式類負證據沒有出現；聲明定義類負證據出現3次，總風險值為15；語句類負證據出現17次，總風險值為51；參數注釋類負證據沒有出現；沒有出現關鍵負證據.

表7 負證據度量結果Tab.7 Negative Evidence measurement results

4.2 可信度計算

本小節(jié)通過4.1節(jié)中得到的證據度量結果和本文提出的度量方法對msg模塊進行可信度計算.本文采用的參數和權重值如表8所示.

表8 參數和權重值表Table 8 Parameters and weight values

其中，為了便于計算，在正證據可信度計算中，由于關鍵證據每類均是5個，令關鍵正證據ei在所有關鍵證據中所占的權重αi均相等，因此αi的值均取1/5，令每類非關鍵正證據ej在每類所有非關鍵正證據中所占的權重βj均相等，因此，表達式類權重為1/12，聲明定義類權重為1/9，語句類權重為0.1，參數注釋類權重為0.2.每類正證據所占的權重均為1/4，每類負證據所占的權重均為1/4.

通過每個正證據的度量結果計算出的此類正證據的可信度量值為：

TP1=0.6×10+0.4×8.87=9.55,

TP2=0.6×9.31+0.4×8.53=9.00,

TP3=0.6×10+0.4×10=10.00,

TP4=0.6×10+0.4×8.67=9.47,

通過各類負證據計算的此類負證據的可信度量值為：

TN1=e0=1.000,

TN2=e-0.015=0.985,

TN3=e-0.051=0.950,

TN4=e0=1.000,

基于混合證據計算的軟件可信度為：

T1=9.550.5×10.000.5=9.77,

T2=9.000.5×9.850.5=9.42,

T3=10.000.5×9.500.5=9.75,

T4=9.470.5×10.000.5=9.73,

T=9.770.25×9.420.25×9.750.25×9.730.25=9.6

最終計算得出軟件的可信度為9.67，可信度量值大于9.5，但是關鍵正證據“數組下標越界檢查”度量值為B，因此該軟件的可信等級為Ⅳ級.

Core Flight Executive作為NASA Core Flight System的核心軟件，在開源社區(qū)Github獲得較多好評，并且NASA在開源該代碼之前也使用其作為部分飛行器的代碼，因此其可信性較高，本文的可信量化評估結果符合該軟件的實際情況.

5 結 論

作為安全攸關的領域之一，航天軟件的可信性至關重要.通過有效的方法評估航天軟件可信性，并用形象易懂的方式體現出軟件的可信程度可以為提高軟件可信性和減少因軟件不可信而導致的災難提供依據和參考.

本文首先建立了面向航天型號軟件的C語言可信證據規(guī)范，并提出了一種面向源代碼的航天軟件可信性度量方法，分別計算在每類可信正證據和可信負證據的可信度量值，然后使用基于混合證據的軟件可信度量模型計算最終的軟件可信度.在此基礎上，本文提出了一種面向航天領域的軟件可信分級模型，用來展現軟件的可信程度，并且使用NASA的開源軟件Core Flight Executive驗證了本文所提出的可信量化評估方法具有很好的有效性和實用性.