第1章 項目概況

1.1 項目介紹

隨著現代信息技術創新及其廣泛應用，軟件已經成為現代計算機系統的靈魂，成為國家信息化建設的核心，成為當代社會生產力發展和人類文明進步的強大動力，在國民經濟、社會發展和國防建設中發揮著舉足輕重的作用。

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

“可信”是在傳統的“安全”“可靠”等概念基礎上發展起來的一個相對較新的學術概念。一般認為，所謂“可信”，是指一個實體在實現給定目標時，其行為及其結果是可以預期的。它強調目標與實現相符以及行為與結果的可預測性和可控制性。所謂“可信軟件”，是指軟件系統的運行行為及其結果總是符合人們的預期，并且在受到干擾時仍能提供連續的服務。

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

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

國家自然科學基金委員會在廣泛聽取各界專家意見和反復深入研討的基礎上，由信息科學部、數學物理科學部和管理科學部聯合組織，于2007年啟動了“可信軟件基礎研究”重大研究計劃（以下簡稱本重大研究計劃）。這是我國軟件基礎研究領域的一件大事。本重大研究計劃對應對軟件發展的重要科學挑戰，推動我國軟件基礎理論的探索與創新，促進國家軟件產業及相關應用領域的發展，具有非常重大的意義。本重大研究計劃共資助項目107項，其中培育項目73項、重點支持項目24項、集成項目5項，資助總經費達1.9億元，全部資助項目已于2017年底順利結題。

1.1.1 總體科學目標

本重大研究計劃以國家關鍵應用領域中軟件可信性問題為主攻方向，總體科學目標如下：

①采用理論研究和實證研究相結合的方法，揭示軟件可信和環境可信失效、度量和演化的基本規律，建立可信軟件及其環境構造與驗證、演化與控制的方法和關鍵技術體系，研究可信軟件開發工具和運行支撐平臺及環境；

②在典型的嵌入式軟件和網絡應用軟件中進行驗證和示范，促進軟件從傳統的單一度量理論到綜合性的可信度量理論及其構造方法的集成升華，提高我國在可信軟件領域的原始創新能力和國際影響力，為國家相關重大計劃和工程的可信軟件研發提供科學支撐；

③在可信軟件領域集聚和培養一批站在國際前沿、具有理論和源頭技術創新能力的高水平研究人才隊伍，促進我國軟件產業的崛起和發展。

1.1.2 核心科學問題

本重大研究計劃的核心科學問題包括以下四大類。

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

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

軟件可信性度量與建模研究需要解決的基礎科學理論問題及研究要點包括以下幾方面。

①軟件可信性度量系統。研究軟件缺陷與可信性的內在聯系、軟件缺陷預測和缺陷分布規律；研究多維可信屬性的多尺度量化指標系統、度量和評估機制以及測評體系；研究可信屬性之間的交互關系及其涌現特征，包括多屬性/綜合屬性的局部/全局相容與失配等；建立可信軟件度量的技術標準或管理標準方案。

②軟件可信性的演化與預測。研究軟件可信性相關數據的收集、分析和知識挖掘方法；研究軟件在環境和自身演化下可信性的演化規律以及軟件在線演化的基礎理論；研究基于軟件行為的軟件可信性增長和面向威脅的在線評估與預測理論。

③可信軟件的風險及過程管理。研究可信軟件生命周期的風險識別、評估、管理和控制模式及方法；研究可信軟件過程的屬性和度量框架以及相應的量化控制和度量評估方法；研究適應分布性、敏捷性和過程資產復用性等需求的可信軟件過程建模、定制、仿真和優化方法；研究可信軟件的人—信息系統交互作用及優化機理。

（2）可信軟件的構造與驗證

傳統的軟件理論在軟件構造與驗證時注重在封閉環境下追求不可演化的絕對正確和效率優先。對于可信軟件，必須適應開放環境下物理世界中的計算規律，從追求軟件絕對正確和效率優先的軟件方法學變為力求保證在可演化的環境下滿足可信需求的軟件方法學。因此，如何進行可信性算法設計和軟件設計、如何消解多屬性引起的可信性沖突、如何進行可信性保證成為解決可信軟件開發問題的關鍵。

可信軟件的構造與驗證研究需要解決的基礎科學理論問題及研究要點包括以下幾方面。

①可信軟件的程序理論與方法學。研究軟件行為可信特征空間的概念模型及形式化體系，包括程序的近似和漸近正確性理論，以及刻畫軟件的近似可信性與演化可信性理論；針對可信軟件形態的多樣性、動態性和協同性，特別是數據與控制同時動態變化的新特征，研究網絡環境下的可信軟件系統形式化模型；研究軟件系統集成的基礎理論以及對可信性影響的推理基礎；從風險和病態角度，研究可信約束下的軟件病態特征提取技術、軟件病態及環境間的關系，以及相應的預測理論與控制方法；建立可信軟件全周期開發方法學。

②可信軟件的需求工程。研究面向可信性的需求分析方法；研究基于社會的可信模型的需求工程方法；研究風險分析和可信性分析技術；研究軟件可信性的性質獲取與形式規約；研究多維異質非功能需求的沖突消解與完整性表述方式；探索基于領域知識的可信性分析方法和理論。

③可信軟件設計、構造與編譯。研究可信軟件設計的系統化科學體系，包括基于構件的、面向服務的和基于面向方面技術的可信軟件的構造方法和代碼生成技術；研究支持軟件自演化的可信軟件體系結構；研究可信程序設計的基礎要素和語言設計，以及可信編譯技術；研究算法可信性度量和可信算法設計的數學基礎，針對典型科學計算問題，研究誤差可控計算的基礎算法等。

④可信軟件的驗證與測試。研究復雜環境下嵌入式軟件和開放環境中網絡軟件的形式建模與分析技術，以及可信軟件的模型自動抽取技術；研究多層次可信軟件可擴展形式驗證方法和錯誤定位方法；研究面向可信性的測試策略和基于控制理論的自適應測試方法；研究基于模型和規約的可信軟件測試技術；研究可信軟件驗證與測試的集成方法，以及基于測試和驗證數據的可信性評估與預測方法。

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

傳統的軟件理論僅從靜態的角度認識軟件部署后的變化，對于軟件維護往往是事后被動響應；而開放環境下軟件的演化是軟件面向可生存性需求的重要特征。對于可信軟件，需要從事后維護向事前設計、主動監控變化，形成與軟件動態演化中的可信性相適應的控制方法。因此，如何認識環境的演化和軟件自身的演化、如何動態獲取可信性和控制可信性的變化、如何構建可信的運行平臺是解決可信軟件在開放動態環境中可信運行問題的關鍵。

可信軟件的演化與控制研究需要解決的基礎科學理論問題及研究要點包括以下幾方面。

①可信軟件運行監控機理。研究軟件運行時環境變化和軟件變化對可信性的影響；研究復雜開放環境下基于運行監控的可信軟件模型和體系結構；研究面向可信軟件演化特性的軟件運行監控與保障機制。

②軟件可信性動態控制方法。研究軟件運行時的行為監控與可信性監測、診斷、恢復方法，以及基于虛擬化環境的軟件系統故障范圍控制和快速恢復方法與機制，包括基于動態控制更改的可信軟件運行的自主管理機制和代碼維護關鍵技術、多維度監控的關注點分離技術，以及基于運行監控的可信性動態評估機制；研究網絡計算環境的高可信支撐軟件技術。

（4）可信環境的構造與評估

軟件可信性離不開環境的支撐，環境可信是可信軟件的重要方面。目前，可信環境的基礎理論研究滯后于可信計算技術的研究，需要探求在網絡環境下構建一個相對可信的計算環境的理論和方法。因此，如何正確認識可信環境體系結構的形態、如何建立信任鏈并且傳遞和管理信任關系、如何構造可信的安全多方計算環境、如何評價計算環境的可信程度成為必須面對的問題。

①可信環境的數學理論與信任鏈傳遞理論。研究支持可信計算的數學模型、形式化模型，構建可信計算的理論體系；研究可信網絡計算的形式化模型，形成完整性保護的理論體系；研究信任鏈的建立與信任的傳遞機制，重點研究支持信任鏈建立與傳遞的無干擾模型。

②可信計算環境構造機理及方法。研究基于可信硬件層靈活擴展信任邊界的體系結構，可信計算平臺的完整性收集、度量、驗證的體系結構，以及網絡連接與認證的體系結構；研究可信計算與虛擬技術結合的新型可信虛擬平臺架構，重點探索基于可信平臺模塊的虛擬平臺安全體系結構以及可信平臺模塊的虛擬化技術；研究可信的安全多方計算環境的構造方法。

③可信計算環境測評。研究適用于可信計算平臺的安全評估模型；研究可信平臺模塊協議檢測方法，包括可信計算平臺安全功能測試、標準符合性測試、穿透性測試等技術，從而為認證、授權和平臺證明協議的正確性、安全性及性能的驗證提供支持。