可信軟件研究*

俞烈彬，王立杰

(江蘇自動(dòng)化研究所，江蘇 連云港 222061)

現(xiàn)代裝備中大部分電子設(shè)備的關(guān)鍵功能由軟件來(lái)完成，隨著系統(tǒng)自動(dòng)化、智能化水平的不斷提高，軟件規(guī)模和復(fù)雜度也不斷提高，比如在F-22戰(zhàn)機(jī)的綜合航電系統(tǒng)中，軟件實(shí)現(xiàn)的航電功能高達(dá)80%，軟件代碼達(dá)到170萬(wàn)余行。而在F-35戰(zhàn)機(jī)的先進(jìn)綜合航電系統(tǒng)中，軟件代碼達(dá)到500萬(wàn)～800萬(wàn)行。這表明，越來(lái)越多的安全性關(guān)鍵系統(tǒng)軟件日益密集化。另一方面，由軟件引發(fā)的事故或事件卻頻發(fā)不斷:如2004年12月20日，一架F-22因飛行控制軟件故障而墜毀;2007年2月11日，12架F-22在穿越國(guó)際日期變更線時(shí)又因軟件缺陷問(wèn)題造成導(dǎo)航故障，戰(zhàn)機(jī)被迫在無(wú)導(dǎo)航和通信能力下危險(xiǎn)返航。由此可見(jiàn)，武器裝備中的軟件是否具備包括可靠、可用、安全等特性在內(nèi)的可信特征已成為衡量和影響武器裝備效能的最重要的指標(biāo)，構(gòu)建可信的裝備軟件，對(duì)搶占未來(lái)信息化戰(zhàn)爭(zhēng)制高點(diǎn)有著重要的作用。

近十年來(lái)軟件的可信性研究一直受到廣泛重視。美國(guó)政府的“網(wǎng)絡(luò)與信息技術(shù)研究發(fā)展計(jì)劃(NITRD)”［1］中，列出了8個(gè)重點(diǎn)領(lǐng)域，有4個(gè)與“可信軟件”密切相關(guān)。美國(guó)自然科學(xué)基金會(huì)(NSF)在加州大學(xué)伯克利分校建立了科學(xué)與技術(shù)研究中心TRUST［2］，其研究?jī)?nèi)容圍繞可信系統(tǒng)的設(shè)計(jì)、構(gòu)建和運(yùn)行展開(kāi)。國(guó)家自然科學(xué)基金的“可信軟件基礎(chǔ)研究”重大研究計(jì)劃［3］是目前國(guó)內(nèi)可信軟件研究的主要研究計(jì)劃之一，其重點(diǎn)支持對(duì)嵌入式軟件和網(wǎng)絡(luò)應(yīng)用軟件領(lǐng)域的軟件可信性進(jìn)行研究。

1 可信軟件相關(guān)技術(shù)研究現(xiàn)狀

如果一個(gè)軟件系統(tǒng)的行為總是與用戶預(yù)期的行為和結(jié)果相一致，在受到干擾時(shí)仍能提供連續(xù)的服務(wù)，則稱該軟件可信［4］。目前可信軟件的研究方向主要集中在軟件可信性度量與評(píng)估、可信軟件的構(gòu)造與驗(yàn)證、可信軟件的演化與控制等。

1.1 軟件可信性度量與評(píng)估

軟件的可信性是軟件提供服務(wù)時(shí)符合用戶期望的能力，不僅涵蓋了軟件質(zhì)量特性中功能性、可靠性、易用性、效率、可維護(hù)性和可移植性等，還應(yīng)包括安全性、實(shí)時(shí)性、可生存性等其他特性。國(guó)外研究可信軟件比較有成效的是德國(guó)達(dá)姆施塔特大學(xué)的Databases and Distributed Systems Group 的“可信計(jì)劃”［5］，該計(jì)劃的目標(biāo)是解決可信分布式系統(tǒng)的若干問(wèn)題。他們的結(jié)論是可信是一個(gè)綜合的性質(zhì)，包含以下特征:端到端安全，可用性，可靠性，時(shí)效性，一致性，可預(yù)測(cè)性，可擴(kuò)展性等?？尚沤M織Trustie制定的可信規(guī)范中定義軟件可信屬性包括［6］:可用性(Availability)，可靠性(Reliability)，安全性(Security)，實(shí)時(shí)性(Real Time)，可維護(hù)性(Maintainability)和可生存性(Survivability)。上述每個(gè)特性又由若干子特性構(gòu)成，這些屬性構(gòu)成了軟件可信屬性模型，如圖1所示。

圖1 軟件可信屬性

軟件可信評(píng)估是通過(guò)分級(jí)的方式對(duì)用戶的主觀感受進(jìn)行評(píng)價(jià)，用戶根據(jù)證據(jù)描述軟件對(duì)某種可信屬性的滿足程度。一種可信屬性可能通過(guò)多個(gè)可信證據(jù)從不同的角度反映出來(lái)。一個(gè)軟件所有可信證據(jù)的集合以某種結(jié)構(gòu)進(jìn)行組織后，就構(gòu)成了軟件可信證據(jù)模型。Trustie組織在文獻(xiàn)［6］中提出了一種證據(jù)模型，將可信證據(jù)分為開(kāi)發(fā)階段證據(jù)、提交階段證據(jù)和應(yīng)用階段證據(jù)三個(gè)部分，如圖2所示。

圖2 軟件證據(jù)分類

軟件可信評(píng)估是對(duì)軟件可信屬性的綜合分析評(píng)估，是一個(gè)多屬性決策分析［7］(MADA，Multiple Attribute Decision Analysis)問(wèn)題。軟件評(píng)估過(guò)程如圖3所示。針對(duì)MADA問(wèn)題，傳統(tǒng)的方法有字典序法、簡(jiǎn)單加性加權(quán)法、層次分析法［8］等。數(shù)學(xué)評(píng)估模型通過(guò)模糊理論將定性指標(biāo)定量化，很好地解決了現(xiàn)有評(píng)估模型中指標(biāo)單一、原始信息模糊的評(píng)估問(wèn)題。由于屬性權(quán)重和偏好等決策要素的不確定性，近年來(lái)，研究熱點(diǎn)逐漸轉(zhuǎn)向?qū)δ：鄬傩詻Q策問(wèn)題［9］(FMADM，F(xiàn)uzzy Multattribute Decision Making)的研究。

圖3 軟件可信評(píng)估過(guò)程

1.2 可信軟件的構(gòu)造與驗(yàn)證

可信軟件構(gòu)造主要分為工程化方法和形式化方法。工程化方法的核心思想是建立嚴(yán)格的工程規(guī)范，在軟件生命周期內(nèi)的各個(gè)階段，通過(guò)規(guī)范管理和輔助工具，最大限度地減少人為錯(cuò)誤的機(jī)會(huì)，或盡可能早地發(fā)現(xiàn)人為錯(cuò)誤。但隨著對(duì)軟件可信性要求的提高，工程化方法漸漸不能滿足高可信軟件開(kāi)發(fā)的要求。統(tǒng)計(jì)表明，傳統(tǒng)的非形式化的軟件工程技術(shù)對(duì)軟件質(zhì)量的保證具有一個(gè)難以逾越的鴻溝，而形式化方法是提高軟件質(zhì)量的重要途徑。形式化方法的研究分為兩類:一類是直接為以UML為代表的面向?qū)ο笳Z(yǔ)言增加形式化語(yǔ)義，如英國(guó)的pUML組(precise UML group)就致力于運(yùn)用數(shù)學(xué)知識(shí)將UML發(fā)展為一種具備精確數(shù)學(xué)語(yǔ)義的描述語(yǔ)言;另一類是通過(guò)模型轉(zhuǎn)換得到模型對(duì)應(yīng)的形式化語(yǔ)言描述。目前常用的形式化語(yǔ)言工具有自動(dòng)機(jī)、進(jìn)程代數(shù)、Petri網(wǎng)、邏輯學(xué)等。形式化方法研究早期，研究者一般都是手動(dòng)給出系統(tǒng)形式化描述。模型驅(qū)動(dòng)架構(gòu)(MDA)［10］提出以后，基于模型驅(qū)動(dòng)的可信軟件構(gòu)造與驗(yàn)證迅速成為一個(gè)研究熱點(diǎn)，模型驅(qū)動(dòng)方法可以很好地支持形式化的描述和說(shuō)明，可以較為方便對(duì)軟件可信需求進(jìn)行抽象建模，給出形式化的歸約，進(jìn)行模型轉(zhuǎn)換、邏輯推理。模型驅(qū)動(dòng)的形式化方法如圖4所示。澳大利亞昆士蘭大學(xué)的Soon-Kyeong Kim等［11］采用MDA方法，通過(guò)模型轉(zhuǎn)換集成形式化建模語(yǔ)言(Object-Z)與非形式化建模語(yǔ)言(UML)，對(duì)于集成Object-Z和UML的建模語(yǔ)言，使用可重用的MDA轉(zhuǎn)換框架。A.MEKKI［12］在MDA框架下完成了時(shí)間限定系統(tǒng)模型到時(shí)間自動(dòng)機(jī)的自動(dòng)轉(zhuǎn)換。

圖4 模型驅(qū)動(dòng)的形式化方法

對(duì)于軟件的可信驗(yàn)證，在傳統(tǒng)軟件工程中，主要通過(guò)軟件可靠性測(cè)試來(lái)實(shí)現(xiàn)。在高可信軟件工程領(lǐng)域，常采用形式化的驗(yàn)證方法。形式化驗(yàn)證的主要技術(shù)有模型檢驗(yàn)和定理證明。模型檢驗(yàn)技術(shù)［13］是通過(guò)搜索待驗(yàn)證軟件系統(tǒng)模型的有窮狀態(tài)空間來(lái)檢驗(yàn)系統(tǒng)的行為是否具備預(yù)期性質(zhì)的一種有窮狀態(tài)系統(tǒng)自動(dòng)驗(yàn)證技術(shù)，其過(guò)程如圖5所示。RWTH Aachen University的Schlich B提出了一種基于嵌入式軟件匯編碼的模型檢驗(yàn)方法［14］，該方法結(jié)合了模型檢驗(yàn)、靜態(tài)分析和抽象解釋等手段，同時(shí)使用一個(gè)定制的模擬器建立了狀態(tài)矢量空間來(lái)控制不確定性。隨著國(guó)內(nèi)外對(duì)模型檢驗(yàn)技術(shù)的深入研究，為了驗(yàn)證系統(tǒng)以及系統(tǒng)性質(zhì)，出現(xiàn)了SPIN、DESIGN/CPN、UPPAAL等模型檢驗(yàn)工具。

圖5 模型檢驗(yàn)過(guò)程

模型檢驗(yàn)過(guò)程與模型檢驗(yàn)技術(shù)不同，定理證明方法可以直接處理無(wú)限的狀態(tài)空間。定理證明技術(shù)將軟件系統(tǒng)和性質(zhì)用邏輯方法來(lái)規(guī)約，通過(guò)基于公理和推理規(guī)則組成的形式系統(tǒng)，以類似數(shù)學(xué)中定理證明的方法來(lái)證明軟件系統(tǒng)是否具備所期望的關(guān)鍵性質(zhì)［15］。明尼蘇達(dá)大學(xué)軟件學(xué)院數(shù)字科技中心針對(duì)引導(dǎo)規(guī)則被劃分為同步階段和異步階段的一階規(guī)約與聯(lián)合規(guī)約邏輯定義，提出了一種集中證明系統(tǒng)［16］，集中證明方法中定理證據(jù)搜索被集中在一個(gè)交叉的、可計(jì)算的區(qū)間內(nèi)，而且更具有一般推導(dǎo)性。我國(guó)在幾何定理及其證明方面處于國(guó)際領(lǐng)先地位，吳文俊院士提出數(shù)學(xué)機(jī)械化證明方法推動(dòng)了定理機(jī)器證明的研究［17］，通過(guò)該方法可在微機(jī)上很快地證明困難的幾何定理。但目前定理證明方法的效率還較低，很難用于大系統(tǒng)的驗(yàn)證。

1.3 可信軟件的演化與控制

軟件的動(dòng)態(tài)演化是指軟件系統(tǒng)投入運(yùn)行后，隨環(huán)境和需求變化而進(jìn)行的變更［18］。在開(kāi)放環(huán)境下，隨著軟件多變性的發(fā)展，新技術(shù)與新功能的演變?cè)絹?lái)越復(fù)雜，因此必須對(duì)軟件的動(dòng)態(tài)行為進(jìn)行監(jiān)控，形成對(duì)軟件動(dòng)態(tài)演化中的可信性控制方法。軟件行為監(jiān)控和控制的基本框架如圖6所示。

圖6 軟件行為監(jiān)控和控制框架

目前研究者一般采用形式化方法進(jìn)行軟件行為描述，如Petri網(wǎng)、自動(dòng)機(jī)和進(jìn)程代數(shù)等。得到系統(tǒng)行為描述后，一般需要進(jìn)行形式化驗(yàn)證。軟件行為監(jiān)控是行為可信評(píng)估的基礎(chǔ)，為了對(duì)軟件行為進(jìn)行全面、準(zhǔn)確、實(shí)時(shí)的監(jiān)控，很多研究者提出了相應(yīng)的軟件監(jiān)控方法。Diakov［19］等人提出了一種基于CORBA中間件平臺(tái)的軟件行為監(jiān)控框架，能自動(dòng)生成監(jiān)測(cè)代碼來(lái)監(jiān)測(cè)構(gòu)件之間的交互行為。Li Jun［20］提出了一個(gè)軟件行為監(jiān)測(cè)框架，基于全局因果跟蹤技術(shù)捕獲多維軟件系統(tǒng)行為。Chen Feng［21］等人提出了一種運(yùn)行時(shí)行為監(jiān)測(cè)框架MOP，該框架能根據(jù)給定的行為規(guī)約自動(dòng)生成監(jiān)測(cè)器，動(dòng)態(tài)監(jiān)測(cè)系統(tǒng)運(yùn)行行為，一旦發(fā)現(xiàn)違約行為，能立即觸發(fā)用戶定義的操作進(jìn)行容錯(cuò)處理。為了提高軟件的持續(xù)可用性和軟件行為的可信性，有必要對(duì)軟件行為進(jìn)行控制，其主要包括異常行為控制和演化行為控制。Garlan［22］等人研究了基于運(yùn)行時(shí)體系結(jié)構(gòu)的自適應(yīng)系統(tǒng)Rainbow。它采用外置運(yùn)行時(shí)體系結(jié)構(gòu)，通過(guò)Probe-Gauge-Consumer三層監(jiān)控機(jī)制，獲取和度量系統(tǒng)變化來(lái)觸發(fā)自適應(yīng)規(guī)則實(shí)現(xiàn)自適應(yīng)演化。文獻(xiàn)［23］也提出了一種面向體系結(jié)構(gòu)的自適應(yīng)系統(tǒng)Artennis-ARC。它采用內(nèi)置運(yùn)行時(shí)體系結(jié)構(gòu)，通過(guò)Agent-Gauge-Monitor三層監(jiān)控機(jī)制，驅(qū)動(dòng)軟件系統(tǒng)進(jìn)行自適應(yīng)演化。

2 可信軟件技術(shù)面臨的挑戰(zhàn)

現(xiàn)代裝備軟件大部分是以嵌入式軟件的形式存在。嵌入式軟件具有高復(fù)雜性的特點(diǎn)，同時(shí)對(duì)以實(shí)時(shí)性、可生存性、安全性為代表的高可信特征具有迫切需求，這些都對(duì)傳統(tǒng)的軟件可信技術(shù)提出了挑戰(zhàn)。目前研究可信裝備軟件技術(shù)中存在的問(wèn)題主要為以下三個(gè)方面。

1)可信性度量和評(píng)估:目前裝備軟件沒(méi)有形成完整統(tǒng)一的可信指標(biāo)體系，缺乏軟件評(píng)估技術(shù)標(biāo)準(zhǔn)或規(guī)范;可信屬性單獨(dú)進(jìn)行度量評(píng)估，沒(méi)有形成正確性、可靠性、安全性等屬性的綜合度量空間。

2)可信軟件構(gòu)造與驗(yàn)證:模型驅(qū)動(dòng)技術(shù)為可信軟件構(gòu)造提供了一個(gè)極好的基礎(chǔ)架構(gòu)，但是針對(duì)現(xiàn)代國(guó)防武器領(lǐng)域中復(fù)雜嵌入式軟件系統(tǒng)的高可信需求，目前已有的模型驅(qū)動(dòng)相關(guān)技術(shù)中并沒(méi)有提供有效的模型精化、轉(zhuǎn)換以及生成可信代碼的有效方法，以及全過(guò)程連接方法;缺少異構(gòu)模型語(yǔ)義保持和一致性理論和方法;缺少裝備軟件可信構(gòu)造與驗(yàn)證的系統(tǒng)方法，缺少可信軟件開(kāi)發(fā)工具和支撐平臺(tái);模型檢驗(yàn)應(yīng)用面臨的主要挑戰(zhàn)是狀態(tài)爆炸問(wèn)題，必須設(shè)計(jì)可以處理大型搜索空間的算法和數(shù)據(jù)結(jié)構(gòu)，因此這方面的研究主要針對(duì)模型抽象技術(shù)和系統(tǒng)狀態(tài)空間的存儲(chǔ)和搜索技術(shù)［24］。

3)傳統(tǒng)軟件監(jiān)控需求表達(dá)能力不強(qiáng)，監(jiān)控代碼分散。沒(méi)有形成開(kāi)放和復(fù)雜環(huán)境下的可信軟件運(yùn)行監(jiān)控模型和體系結(jié)構(gòu);缺乏可信軟件演化的保障機(jī)制;在行為描述方面，需要建立軟件可信性與軟件行為之間的內(nèi)在聯(lián)系和嚴(yán)格描述;在行為監(jiān)測(cè)方面，需要設(shè)計(jì)有效的收集可信性相關(guān)數(shù)據(jù)的行為監(jiān)測(cè)機(jī)制;在行為可信管理方面，需要研究基于行為監(jiān)測(cè)的可信評(píng)估方法，構(gòu)建基于行為監(jiān)測(cè)的可信管理框架;在行為控制方面，需要研究支持行為可信的軟件動(dòng)態(tài)演化機(jī)制。

3 結(jié)束語(yǔ)

高可信軟件技術(shù)已成為國(guó)防信息技術(shù)及武器裝備中嵌入式軟件研發(fā)與應(yīng)用過(guò)程中最為關(guān)鍵的核心技術(shù)。目前國(guó)內(nèi)非常缺乏這方面的基礎(chǔ)理論、實(shí)現(xiàn)技術(shù)以及工具的研究。我國(guó)可信軟件的標(biāo)準(zhǔn)大多參考國(guó)外標(biāo)準(zhǔn)，整體落后于發(fā)達(dá)國(guó)家水平，從長(zhǎng)遠(yuǎn)發(fā)展來(lái)看，不利于我國(guó)國(guó)防基礎(chǔ)技術(shù)研究能力的提高和創(chuàng)新能力的培養(yǎng)。因此，為了適應(yīng)武器裝備的快速發(fā)展，加強(qiáng)和提高我國(guó)在國(guó)防領(lǐng)域中高可信裝備軟件的基礎(chǔ)技術(shù)研究能力和創(chuàng)新能力，提高軍工高精尖裝備產(chǎn)品的質(zhì)量，需要展開(kāi)高可信相關(guān)技術(shù)的研究，構(gòu)建擁有自主知識(shí)產(chǎn)權(quán)的裝備軟件可信平臺(tái)，這對(duì)于減少因軟件缺陷帶來(lái)的巨大損失與生命傷害，以及有效保障和提升我國(guó)國(guó)防武器裝備的作戰(zhàn)效能具有極其重要的意義。

［1］網(wǎng)絡(luò)與信息技術(shù)研究發(fā)展計(jì)劃(NITRD).http:∥www.nitrd.gov

［2］TURST.http:∥www.truststc.org/

［3］劉克，單志廣，王戟，等.可信軟件基礎(chǔ)研究重大研究計(jì)劃綜述［J］.中國(guó)科學(xué)基金，2008，22(3):145-151.

［4］WANG Huai min，LIU Xu dong.etc.Software trustworthiness classification specification(TRUSTIE STCV2.0)［EB/OL］，2009.

［5］T.Anderson，A.Avizienis，W.Carter，et al.Dependability:basic concepts and terminology［J］.Series:Dependable Computing and Fault-Tolerant Systems，1994，5

［6］Trustie Group.A trustworthy software production environment for large scale software resource sharing and cooperativedevelopment［EB/OL］.2008:http:∥ www.trustie.org.

［7］J.B.Yang，Y.M.Wang，D.L.Xu，et al.The evidential reasoning approach for MADA under both probabilistic and fuzzy uncertainties［J］.European Journal of Operational Research，2006，171(1):309-343.

［8］J.B.Yang，J.Liu，J.Wang，et al.Belief rule-base inference methodology using the evidential reasoning approach-RIMER［J］.Systems，Man and Cybernetics，Part A:Systems and Humans，IEEE Transactions on，2006，36(2):266-285.

［9］姚爽，郭亞軍，黃瑋強(qiáng).基于證據(jù)距離的改進(jìn) DS/AHP多屬性群決策方法［J］.控制與決策，2010，25(6):894-898.

［10］OMG MDA Guide Version 1.0.1.http:∥www.omg.org/cgi-bin/doc?omg/03-06-01，retrieved at 2009.

［11］Soon-Kyeong Kim，Damian Burger，David Carrington.An MDA Approach towards Integrating Formal and Informal Modeling Languages［J］.Formal Method，2005，LNCS P:448-464.

［12］A.MEKKI，M.GHAZEL.Time-constrained Systems Validation Using Mdamodel Transformation.A Railway Case Study.8th International Conference of Modeling and Simulation.May，2010:10-12.

［13］E.Clarke，K.Mcmillan，S.Campos，et al.Symbolic Model Checking［A］;Proceedings of the LNCS 1102［C］，1996.Springer:419-422.

［14］Schlich B.Model Checking of Software for Microcontrollers［J］.ACM TRANSACTIONS ON EMBEDDED COMPUTING SYSTEMS，2010，9(4).

［15］COOK S A.The Complexity of Theorem-Proving Procedures［A］;Proc.3rdAnnu.ACM sympos.On Theory of Computing(NewYork)，assoc.Comput，1971:151-158.

［16］David Baelde，Dale Miller，Zachary Snow.Focused Inductive Theorem Proving［J］.Lecture Notes in Computer Science，2010，6173:278-292.

［17］吳文俊.初等幾何判定問(wèn)題與機(jī)械化證明［J］.中國(guó)科學(xué)，1977(7):507-516.

［18］萬(wàn)燦軍等.動(dòng)態(tài)演化環(huán)境中可信軟件行為監(jiān)控研究與進(jìn)展.計(jì)算機(jī)應(yīng)用研究.2009，26(4):1201-1204.

［19］DIAKOVK.etc.Monitoring of Distributed Component Interactions.Proc of IFIP International Conference on Distributed Systems Platforms and Open Distributed Processing.NewYork，2000:229-243.

［20］LI Jun.Monitoring and Characterization of Componentbased Systems with Global Causality Capture［C］.Proc of the 23rd International Conference on Distributed Computing System，2003:422-431.

［21］CHEN Feng.etc.MOP:An Efficient and Generic Run Time Verification Framework. Proc of OOPSLA2007，2007:569-588.

［22］GARLAN D.etc.Rain-bow:Architecture-based Self-adaptation with Reusable Infrastructure.IEEE Computer，2004，37(10):46-54.

［23］徐鋒，呂建，鄭瑋.一個(gè)軟件服務(wù)協(xié)同中信任評(píng)估模型的設(shè)計(jì)［J］.軟件學(xué)報(bào)，2003，14(6):1043-1051.

［24］薛克.基于SPIN的UML活動(dòng)圖驗(yàn)證［D］.華東師范大學(xué)，2008.