第1章 項(xiàng)目概況

1.1 項(xiàng)目介紹

隨著現(xiàn)代信息技術(shù)創(chuàng)新及其廣泛應(yīng)用，軟件已經(jīng)成為現(xiàn)代計(jì)算機(jī)系統(tǒng)的靈魂，成為國(guó)家信息化建設(shè)的核心，成為當(dāng)代社會(huì)生產(chǎn)力發(fā)展和人類文明進(jìn)步的強(qiáng)大動(dòng)力，在國(guó)民經(jīng)濟(jì)、社會(huì)發(fā)展和國(guó)防建設(shè)中發(fā)揮著舉足輕重的作用。

現(xiàn)代信息社會(huì)對(duì)計(jì)算機(jī)系統(tǒng)的依賴，很大程度上體現(xiàn)為對(duì)軟件的依賴，而計(jì)算機(jī)系統(tǒng)很大一部分缺陷都是軟件問題導(dǎo)致的。隨著軟件的應(yīng)用需求越來越多，復(fù)雜度越來越高，可用性要求越來越強(qiáng)，軟件系統(tǒng)也越來越龐大和脆弱，而且并不總是值得信任的。很多時(shí)候它會(huì)不以人們所期望的方式工作，發(fā)生各種故障和失效，從而直接或間接地對(duì)用戶造成巨大損害。這類問題被稱為“軟件可信性”問題。

“可信”是在傳統(tǒng)的“安全”“可靠”等概念基礎(chǔ)上發(fā)展起來的一個(gè)相對(duì)較新的學(xué)術(shù)概念。一般認(rèn)為，所謂“可信”，是指一個(gè)實(shí)體在實(shí)現(xiàn)給定目標(biāo)時(shí)，其行為及其結(jié)果是可以預(yù)期的。它強(qiáng)調(diào)目標(biāo)與實(shí)現(xiàn)相符以及行為與結(jié)果的可預(yù)測(cè)性和可控制性。所謂“可信軟件”，是指軟件系統(tǒng)的運(yùn)行行為及其結(jié)果總是符合人們的預(yù)期，并且在受到干擾時(shí)仍能提供連續(xù)的服務(wù)。

國(guó)際上由軟件可信性問題導(dǎo)致的重大災(zāi)難、事故和嚴(yán)重?fù)p失屢見不鮮：1996年6月4日，在歐洲阿麗亞娜5型火箭的首次發(fā)射過程中，慣性參考系統(tǒng)軟件的數(shù)據(jù)轉(zhuǎn)換錯(cuò)誤導(dǎo)致軟件失效，使得火箭在發(fā)射40秒后爆炸，造成25億美元的經(jīng)濟(jì)損失；2005年11月1日，日本東京證券交易所因軟件升級(jí)出現(xiàn)系統(tǒng)故障，股市嚴(yán)重停擺；2017年5月12日，WannaCry勒索病毒在全球蔓延，滲透了至少150個(gè)國(guó)家的20萬臺(tái)電腦。軟件可信性問題已經(jīng)成為一個(gè)相當(dāng)普遍的問題。在Google上可以搜索到的與軟件錯(cuò)誤相關(guān)的網(wǎng)頁就有100多萬個(gè)。軟件故障和失效所帶來的影響也愈來愈大。據(jù)美國(guó)國(guó)家標(biāo)準(zhǔn)與技術(shù)研究院（National Institute of Standards and Technology, NIST）估計(jì)，美國(guó)軟件失效所造成的年度經(jīng)濟(jì)損失約占其GDP的0.6%。由此可見，如何高效地開發(fā)可信軟件系統(tǒng)，已經(jīng)成為軟件研究領(lǐng)域必須面對(duì)的核心問題和重要挑戰(zhàn)。

可信軟件已成為現(xiàn)代軟件技術(shù)發(fā)展與應(yīng)用的重要趨勢(shì)和必然選擇。一方面，軟件的規(guī)模越來越大，軟件的開發(fā)、集成和持續(xù)演化越來越復(fù)雜，而目前的可信軟件構(gòu)造與運(yùn)行技術(shù)和軟件可信性度量與評(píng)測(cè)工作嚴(yán)重缺乏，使得軟件產(chǎn)品在推出時(shí)就含有很多已知或未知的缺陷，對(duì)軟件系統(tǒng)的安全可靠運(yùn)行構(gòu)成了嚴(yán)重威脅。另一方面，軟件的運(yùn)行環(huán)境和開發(fā)環(huán)境已經(jīng)從傳統(tǒng)的封閉靜態(tài)環(huán)境拓展為開放、動(dòng)態(tài)、多變的互聯(lián)網(wǎng)環(huán)境，網(wǎng)絡(luò)交互、共享、協(xié)同等帶來了很多不可信因素，網(wǎng)絡(luò)上對(duì)信息的濫用和惡意篡改使得可信問題日益突出。在互聯(lián)網(wǎng)環(huán)境下，計(jì)算實(shí)體的行為具有不可控性和不確定性，這既對(duì)傳統(tǒng)的軟件開發(fā)方法和技術(shù)提出了嚴(yán)峻的挑戰(zhàn)，也對(duì)軟件運(yùn)行時(shí)的可信保障提出了苛刻的要求。

國(guó)家自然科學(xué)基金委員會(huì)在廣泛聽取各界專家意見和反復(fù)深入研討的基礎(chǔ)上，由信息科學(xué)部、數(shù)學(xué)物理科學(xué)部和管理科學(xué)部聯(lián)合組織，于2007年啟動(dòng)了“可信軟件基礎(chǔ)研究”重大研究計(jì)劃（以下簡(jiǎn)稱本重大研究計(jì)劃）。這是我國(guó)軟件基礎(chǔ)研究領(lǐng)域的一件大事。本重大研究計(jì)劃對(duì)應(yīng)對(duì)軟件發(fā)展的重要科學(xué)挑戰(zhàn)，推動(dòng)我國(guó)軟件基礎(chǔ)理論的探索與創(chuàng)新，促進(jìn)國(guó)家軟件產(chǎn)業(yè)及相關(guān)應(yīng)用領(lǐng)域的發(fā)展，具有非常重大的意義。本重大研究計(jì)劃共資助項(xiàng)目107項(xiàng)，其中培育項(xiàng)目73項(xiàng)、重點(diǎn)支持項(xiàng)目24項(xiàng)、集成項(xiàng)目5項(xiàng)，資助總經(jīng)費(fèi)達(dá)1.9億元，全部資助項(xiàng)目已于2017年底順利結(jié)題。

1.1.1 總體科學(xué)目標(biāo)

本重大研究計(jì)劃以國(guó)家關(guān)鍵應(yīng)用領(lǐng)域中軟件可信性問題為主攻方向，總體科學(xué)目標(biāo)如下：

①采用理論研究和實(shí)證研究相結(jié)合的方法，揭示軟件可信和環(huán)境可信失效、度量和演化的基本規(guī)律，建立可信軟件及其環(huán)境構(gòu)造與驗(yàn)證、演化與控制的方法和關(guān)鍵技術(shù)體系，研究可信軟件開發(fā)工具和運(yùn)行支撐平臺(tái)及環(huán)境；

②在典型的嵌入式軟件和網(wǎng)絡(luò)應(yīng)用軟件中進(jìn)行驗(yàn)證和示范，促進(jìn)軟件從傳統(tǒng)的單一度量理論到綜合性的可信度量理論及其構(gòu)造方法的集成升華，提高我國(guó)在可信軟件領(lǐng)域的原始創(chuàng)新能力和國(guó)際影響力，為國(guó)家相關(guān)重大計(jì)劃和工程的可信軟件研發(fā)提供科學(xué)支撐；

③在可信軟件領(lǐng)域集聚和培養(yǎng)一批站在國(guó)際前沿、具有理論和源頭技術(shù)創(chuàng)新能力的高水平研究人才隊(duì)伍，促進(jìn)我國(guó)軟件產(chǎn)業(yè)的崛起和發(fā)展。

1.1.2 核心科學(xué)問題

本重大研究計(jì)劃的核心科學(xué)問題包括以下四大類。

（1）軟件可信性度量與建模

傳統(tǒng)的軟件理論是圍繞程序正確性建立的，其正確性的刻畫以定性方法為主，并且是以靜態(tài)確定性的表達(dá)給出的。對(duì)于可信軟件，需要考查正確性、可靠性、安全性等諸多屬性的綜合度量空間，形成對(duì)軟件可信性的科學(xué)理解，從管理科學(xué)的角度，以定量的方式建立可信性建模的系統(tǒng)方法論，以及適應(yīng)環(huán)境依存穩(wěn)定性條件下的可信度動(dòng)態(tài)演化特征。因此，必須從如何認(rèn)知軟件可信性的角度建立新的軟件系統(tǒng)方法論，從如何表述軟件可信性的角度建立可信需求的建模、規(guī)約和分析方法，從如何把握軟件可信性的角度揭示軟件可信性演化的基本規(guī)律，從而解決如何建立軟件系統(tǒng)可信度量標(biāo)準(zhǔn)以及如何在其工作環(huán)境中進(jìn)行評(píng)估的問題，對(duì)軟件系統(tǒng)的可信性進(jìn)行分級(jí)，并提供量化指標(biāo)。

軟件可信性度量與建模研究需要解決的基礎(chǔ)科學(xué)理論問題及研究要點(diǎn)包括以下幾方面。

①軟件可信性度量系統(tǒng)。研究軟件缺陷與可信性的內(nèi)在聯(lián)系、軟件缺陷預(yù)測(cè)和缺陷分布規(guī)律；研究多維可信屬性的多尺度量化指標(biāo)系統(tǒng)、度量和評(píng)估機(jī)制以及測(cè)評(píng)體系；研究可信屬性之間的交互關(guān)系及其涌現(xiàn)特征，包括多屬性/綜合屬性的局部/全局相容與失配等；建立可信軟件度量的技術(shù)標(biāo)準(zhǔn)或管理標(biāo)準(zhǔn)方案。

②軟件可信性的演化與預(yù)測(cè)。研究軟件可信性相關(guān)數(shù)據(jù)的收集、分析和知識(shí)挖掘方法；研究軟件在環(huán)境和自身演化下可信性的演化規(guī)律以及軟件在線演化的基礎(chǔ)理論；研究基于軟件行為的軟件可信性增長(zhǎng)和面向威脅的在線評(píng)估與預(yù)測(cè)理論。

③可信軟件的風(fēng)險(xiǎn)及過程管理。研究可信軟件生命周期的風(fēng)險(xiǎn)識(shí)別、評(píng)估、管理和控制模式及方法；研究可信軟件過程的屬性和度量框架以及相應(yīng)的量化控制和度量評(píng)估方法；研究適應(yīng)分布性、敏捷性和過程資產(chǎn)復(fù)用性等需求的可信軟件過程建模、定制、仿真和優(yōu)化方法；研究可信軟件的人—信息系統(tǒng)交互作用及優(yōu)化機(jī)理。

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

傳統(tǒng)的軟件理論在軟件構(gòu)造與驗(yàn)證時(shí)注重在封閉環(huán)境下追求不可演化的絕對(duì)正確和效率優(yōu)先。對(duì)于可信軟件，必須適應(yīng)開放環(huán)境下物理世界中的計(jì)算規(guī)律，從追求軟件絕對(duì)正確和效率優(yōu)先的軟件方法學(xué)變?yōu)榱η蟊ＷC在可演化的環(huán)境下滿足可信需求的軟件方法學(xué)。因此，如何進(jìn)行可信性算法設(shè)計(jì)和軟件設(shè)計(jì)、如何消解多屬性引起的可信性沖突、如何進(jìn)行可信性保證成為解決可信軟件開發(fā)問題的關(guān)鍵。

可信軟件的構(gòu)造與驗(yàn)證研究需要解決的基礎(chǔ)科學(xué)理論問題及研究要點(diǎn)包括以下幾方面。

①可信軟件的程序理論與方法學(xué)。研究軟件行為可信特征空間的概念模型及形式化體系，包括程序的近似和漸近正確性理論，以及刻畫軟件的近似可信性與演化可信性理論；針對(duì)可信軟件形態(tài)的多樣性、動(dòng)態(tài)性和協(xié)同性，特別是數(shù)據(jù)與控制同時(shí)動(dòng)態(tài)變化的新特征，研究網(wǎng)絡(luò)環(huán)境下的可信軟件系統(tǒng)形式化模型；研究軟件系統(tǒng)集成的基礎(chǔ)理論以及對(duì)可信性影響的推理基礎(chǔ)；從風(fēng)險(xiǎn)和病態(tài)角度，研究可信約束下的軟件病態(tài)特征提取技術(shù)、軟件病態(tài)及環(huán)境間的關(guān)系，以及相應(yīng)的預(yù)測(cè)理論與控制方法；建立可信軟件全周期開發(fā)方法學(xué)。

②可信軟件的需求工程。研究面向可信性的需求分析方法；研究基于社會(huì)的可信模型的需求工程方法；研究風(fēng)險(xiǎn)分析和可信性分析技術(shù)；研究軟件可信性的性質(zhì)獲取與形式規(guī)約；研究多維異質(zhì)非功能需求的沖突消解與完整性表述方式；探索基于領(lǐng)域知識(shí)的可信性分析方法和理論。

③可信軟件設(shè)計(jì)、構(gòu)造與編譯。研究可信軟件設(shè)計(jì)的系統(tǒng)化科學(xué)體系，包括基于構(gòu)件的、面向服務(wù)的和基于面向方面技術(shù)的可信軟件的構(gòu)造方法和代碼生成技術(shù)；研究支持軟件自演化的可信軟件體系結(jié)構(gòu)；研究可信程序設(shè)計(jì)的基礎(chǔ)要素和語言設(shè)計(jì)，以及可信編譯技術(shù)；研究算法可信性度量和可信算法設(shè)計(jì)的數(shù)學(xué)基礎(chǔ)，針對(duì)典型科學(xué)計(jì)算問題，研究誤差可控計(jì)算的基礎(chǔ)算法等。

④可信軟件的驗(yàn)證與測(cè)試。研究復(fù)雜環(huán)境下嵌入式軟件和開放環(huán)境中網(wǎng)絡(luò)軟件的形式建模與分析技術(shù)，以及可信軟件的模型自動(dòng)抽取技術(shù)；研究多層次可信軟件可擴(kuò)展形式驗(yàn)證方法和錯(cuò)誤定位方法；研究面向可信性的測(cè)試策略和基于控制理論的自適應(yīng)測(cè)試方法；研究基于模型和規(guī)約的可信軟件測(cè)試技術(shù)；研究可信軟件驗(yàn)證與測(cè)試的集成方法，以及基于測(cè)試和驗(yàn)證數(shù)據(jù)的可信性評(píng)估與預(yù)測(cè)方法。

（3）可信軟件的演化與控制

傳統(tǒng)的軟件理論僅從靜態(tài)的角度認(rèn)識(shí)軟件部署后的變化，對(duì)于軟件維護(hù)往往是事后被動(dòng)響應(yīng)；而開放環(huán)境下軟件的演化是軟件面向可生存性需求的重要特征。對(duì)于可信軟件，需要從事后維護(hù)向事前設(shè)計(jì)、主動(dòng)監(jiān)控變化，形成與軟件動(dòng)態(tài)演化中的可信性相適應(yīng)的控制方法。因此，如何認(rèn)識(shí)環(huán)境的演化和軟件自身的演化、如何動(dòng)態(tài)獲取可信性和控制可信性的變化、如何構(gòu)建可信的運(yùn)行平臺(tái)是解決可信軟件在開放動(dòng)態(tài)環(huán)境中可信運(yùn)行問題的關(guān)鍵。

可信軟件的演化與控制研究需要解決的基礎(chǔ)科學(xué)理論問題及研究要點(diǎn)包括以下幾方面。

①可信軟件運(yùn)行監(jiān)控機(jī)理。研究軟件運(yùn)行時(shí)環(huán)境變化和軟件變化對(duì)可信性的影響；研究復(fù)雜開放環(huán)境下基于運(yùn)行監(jiān)控的可信軟件模型和體系結(jié)構(gòu)；研究面向可信軟件演化特性的軟件運(yùn)行監(jiān)控與保障機(jī)制。

②軟件可信性動(dòng)態(tài)控制方法。研究軟件運(yùn)行時(shí)的行為監(jiān)控與可信性監(jiān)測(cè)、診斷、恢復(fù)方法，以及基于虛擬化環(huán)境的軟件系統(tǒng)故障范圍控制和快速恢復(fù)方法與機(jī)制，包括基于動(dòng)態(tài)控制更改的可信軟件運(yùn)行的自主管理機(jī)制和代碼維護(hù)關(guān)鍵技術(shù)、多維度監(jiān)控的關(guān)注點(diǎn)分離技術(shù)，以及基于運(yùn)行監(jiān)控的可信性動(dòng)態(tài)評(píng)估機(jī)制；研究網(wǎng)絡(luò)計(jì)算環(huán)境的高可信支撐軟件技術(shù)。

（4）可信環(huán)境的構(gòu)造與評(píng)估

軟件可信性離不開環(huán)境的支撐，環(huán)境可信是可信軟件的重要方面。目前，可信環(huán)境的基礎(chǔ)理論研究滯后于可信計(jì)算技術(shù)的研究，需要探求在網(wǎng)絡(luò)環(huán)境下構(gòu)建一個(gè)相對(duì)可信的計(jì)算環(huán)境的理論和方法。因此，如何正確認(rèn)識(shí)可信環(huán)境體系結(jié)構(gòu)的形態(tài)、如何建立信任鏈并且傳遞和管理信任關(guān)系、如何構(gòu)造可信的安全多方計(jì)算環(huán)境、如何評(píng)價(jià)計(jì)算環(huán)境的可信程度成為必須面對(duì)的問題。

①可信環(huán)境的數(shù)學(xué)理論與信任鏈傳遞理論。研究支持可信計(jì)算的數(shù)學(xué)模型、形式化模型，構(gòu)建可信計(jì)算的理論體系；研究可信網(wǎng)絡(luò)計(jì)算的形式化模型，形成完整性保護(hù)的理論體系；研究信任鏈的建立與信任的傳遞機(jī)制，重點(diǎn)研究支持信任鏈建立與傳遞的無干擾模型。

②可信計(jì)算環(huán)境構(gòu)造機(jī)理及方法。研究基于可信硬件層靈活擴(kuò)展信任邊界的體系結(jié)構(gòu)，可信計(jì)算平臺(tái)的完整性收集、度量、驗(yàn)證的體系結(jié)構(gòu)，以及網(wǎng)絡(luò)連接與認(rèn)證的體系結(jié)構(gòu)；研究可信計(jì)算與虛擬技術(shù)結(jié)合的新型可信虛擬平臺(tái)架構(gòu)，重點(diǎn)探索基于可信平臺(tái)模塊的虛擬平臺(tái)安全體系結(jié)構(gòu)以及可信平臺(tái)模塊的虛擬化技術(shù)；研究可信的安全多方計(jì)算環(huán)境的構(gòu)造方法。

③可信計(jì)算環(huán)境測(cè)評(píng)。研究適用于可信計(jì)算平臺(tái)的安全評(píng)估模型；研究可信平臺(tái)模塊協(xié)議檢測(cè)方法，包括可信計(jì)算平臺(tái)安全功能測(cè)試、標(biāo)準(zhǔn)符合性測(cè)試、穿透性測(cè)試等技術(shù)，從而為認(rèn)證、授權(quán)和平臺(tái)證明協(xié)議的正確性、安全性及性能的驗(yàn)證提供支持。