1.2 項目布局

1.2.1 項目部署

本重大研究計劃的實施遵循“有限目標、穩定支持，集成升華、跨越發展”的總體思路，圍繞軟件可信性度量與建模、可信軟件的構造與驗證、可信軟件的演化與控制以及可信環境的構造與評估四大核心科學問題，對相關重點資助領域和方向進行項目部署。指導專家組對四個核心科學問題的難點和要點進行了深入分析和分解，確定優先研究的科學問題，選擇的原則包括：優先支持對于核心科學問題具有創新思路的研究；優先支持基礎較好，條件較為成熟，近期可望取得突破性進展的研究；優先選擇對實現本重大研究計劃總體目標起決定作用的研究方向開展跨學科集成研究。

本重大研究計劃前期立項工作主要集中在前三年，根據申請項目的創新思想、研究價值以及對總體目標的貢獻，以培育項目、重點支持項目和集成項目的形式予以資助。中期后選擇對實現總體目標起決定作用的研究方向予以資助，在前期培育項目和重點支持項目成果的基礎上，重點開展集成創新研究，采取集成項目與重點支持項目相結合的形式，以較大支持力度予以資助。在本重大研究計劃的后兩年，重點進行項目和成果的集成升華。

本重大研究計劃在實施過程中按時間段設立階段性目標，在不同階段設立不同的工作重點。各階段的工作重點內容如下。

（1）2008—2011年，基本建立以可信性為核心的軟件理論體系。

①分別從環境、軟件體系結構和程序缺陷等角度研究軟件可信多維建模、度量評價和管理基礎，建立柔性程序理論、軟件可信性多維多尺度度量系統理論、可信環境的基礎理論，以及統一框架下的軟件可信性指標、演化規律與監控理論。

②提出算法的可信性度量與可信算法設計的數學基礎，發展無誤差計算、容錯計算與誤差可控計算設計理論，探索開放、動態、多變環境下的新型計算模型與計算方法，建立并形成可信軟件設計的基本原理。

③建立可信性需求驅動的軟件構造、驗證和測試理論，解決主要可信屬性在軟件需求和構造中失配與沖突的發現及消解問題。

④建立可信軟件與演化的生命周期理論，以及可信軟件的人—機關系理論。

（2）2008—2012年，基本建立可信軟件開發和運行保障關鍵技術體系。

①構建可信軟件研究基本試驗環境，提出可信軟件的復雜性數據和工程數據的收集與分析技術體系。建立軟件可信性在生命周期各環節的評估與預測方法。

②建立可信軟件的過程建模與管理的方法和技術，形成支持軟件生命全周期的可信軟件開發關鍵技術體系，包括需求工程、設計、語言與編譯、驗證、測試等技術，以及軟件可信性的風險管理指標系統，支持可信性的獲取、設計、編碼和驗證確認。

③建立可信軟件運行監控與可信性主動保障技術體系，支持可信性動態演化的監測和控制機理以及可信性的主動保障等技術。

④建立可信計算環境的體系結構、可信虛擬機技術、可信多方安全協作環境構造技術和可信計算環境的測評技術。

（3）2010—2013年，完成面向嵌入式軟件系統和網絡應用軟件系統的試驗環境，集成可信軟件工具環境并在試驗環境進行示范。

①以航空航天領域嵌入式軟件系統為目標，建立高可信軟件綜合試驗環境，并開展典型應用，突破萬行代碼規模的高可信軟件核心模塊的構建與運行保障。

②以金融和政務領域網絡應用軟件系統為目標，建立可信網絡軟件綜合試驗環境，并開展典型電子交易等應用，突破百萬行代碼規模可信網絡應用軟件及環境的構建與運行保障。

1.2.2 綜合集成

本重大研究計劃高度重視研究成果的綜合集成工作，部署了“可信軟件理論、方法集成與綜合實驗平臺”集成項目，以此作為關鍵切入點和重要落腳點。該集成項目由南京大學牽頭研究，整合了本重大研究計劃內相關集成、重點支持和培育項目的優勢研究隊伍及前期研究成果，針對可信軟件度量與建模、構造與驗證、演化與控制等科學問題，以綜合集成與創造提升為手段，從基礎理論體系、方法與平臺架構、典型應用示范等三方面對軟件可信性進行了深入研究，取得了系統性與創新性研究成果，有效推動了技術方法的標準固化、學術團隊的互動融合以及研究成果的集成升華。綜合集成工作主要包括如下幾項。

（1）可信軟件理論與方法的元級化綜合集成

從解決可信軟件度量與建模、構造與驗證、演化與控制等科學問題出發，將這三個科學問題解讀為可信度量、可信評估、可信提升，從可信軟件理論的角度，形成一套集成化可信軟件理論與方法的元級化綜合集成框架Meta-T，包括軟件可信性基本內涵、基本特征和基本機理。

從傳統封閉、靜態環節下發展起來的以正確性為核心的軟件基本理論、方法、技術和機制，已經不足以評價開放、動態、網絡化、多變環境中的軟件的可信性。事實上，可信軟件的主體是人，客體是軟件系統和軟件系統的行為與結果，而軟件可信性的基本內涵就是主體與客體之間的信任關系，這種信任關系的建立是一個動態演變的過程。在特定場景下，主體在采用某種手段收集到的關于客體及相關過程的主/客觀證據的基礎上，加深對客體的認識與理解，通過一定的判定機理，給出主/客觀合理判斷。基于上述認識，軟件可信性具有典型的相對性、過程性、約束性、演化性等基本特征。相對性是指可信判斷不是簡單回答是/不是，而是根據上下文價值觀，基于證據與判定機理進行合理判斷；過程性是指可信程度的提高是一個增量式過程，它取決于對客體及相關過程的關鍵環節進行識別、檢測與控制；約束性是指可信保障是一種投入產出的平衡與優化的過程，可信度提升需要多方面的資源投入與固化；演化性是指可信過程是一個隨生存時間積累與應用空間擴大而不斷解決核心問題的過程。

本重大研究計劃定義了軟件可信性的基本機理，包括駕馭機理、核控機理、加框機理、評判機理和演化機理。可信軟件的駕馭機理是從正確性理論看Meta-T，將正確性框架中固化的可信性要素提煉出來，發現其背后的基本原理與機理，應用到應用場景計算機中，體現主體對客體的全面駕馭、互相融合的過程；核控機理是未來可信演化的基本出發點，從與場景互動的角度，圍繞掌控軟件系統本身的核心部分以及應用場景價值觀下的核心關注點等兩個關鍵部分，對客體模型實現可信的評估；加框機理是在客體模型上找出當前軟件不可信的問題所在，以便采取相應的解決問題的手段；評判機理是根據評估過程中主體對客體通過各種手段收集的主客觀可信證據，依據可信需求的滿足程序、證據的完備程度以及相應的投入成本，進行合理判斷；演化機理明確了可信評估是相對的、交互的，軟件的可信性是隨著軟件的不斷演化、環境的不斷變化、用戶可信需求的不斷變化而變化的。

在此基礎上形成的軟件可信性的綜合集成框架Meta-T，從主體和客體兩個方面開展可信性分析和評估。從主體方面，依據期望的可信目標和可信投入，基于可信機理，通過“選點→加框→證據→判定→評估→演化”的過程，完成可信評估；從客體方面，基于應用場景分析，在客體模型上分析可信問題，決定采取的措施，根據獲得的證據實現軟件演化過程中的可信提升判定，可信保障過程就演變為“場景分析+客體建模+問題標識+可信加框+證據收集+可信度量+可信評估+可信提升”的循環迭代過程。

結合綜合集成框架Meta-T在具體領域的應用，可以根據主體的可信需求、客體及其應用場景，分為形式化模式、經驗化模式、工程化模式、混合式模式等多種實施方式。可從多維度建立層次關系，根據可信的分級需求及可投入的資源，為客體局部可信提升提供指導，同時建立可信提升所需資源的投入與穩定時段實施情況的評估度量。綜合集成框架Meta-T在應用領域的探索主要包括：在模式化架構中進行探索，主要是可信軟件過程體系的建立；在具體企業架構中進行探索，包括航天嵌入式系統、網絡化稅務軟件、網絡化交易系統、列車控制系統、操作系統等。

（2）代碼級可信保障工具綜合集成

以代碼可信為切入點，針對嵌入式系統的源代碼，研究代碼級可信保障工具基準測試套件與集成方法。具體內容包括以下幾點。

①基于基準測試的代碼級可信保障工具評價方法。提出了一種基于基準測試的評價方法，初步構造了一個基準測試集數據庫，實現了一個基本的靜態分析工具基準測試套件，并對四個靜態分析工具進行了測評試驗。針對并發程序分析工具的評價和嵌入式程序數值性質分析工具的評價，對測試套件進行了擴充，并進行了評價試驗。從SAMATE和SV-COMP等網站收集整理了86個具有代表性的并發程序測試用例，豐富了構建的基準測試集數據庫。并且，對兩個并發程序分析工具Thread和ESBMC進行了測試評價，包括開發它們的輸出結果標準化工具（用于在測試套件中對這兩個工具進行自動測試），并且對上述工具的能力、優缺點進行了歸納總結。針對嵌入式程序數值性質分析工具進行評價，也對測試套件進行了擴充，并進行了評價試驗。首先從韓國首爾大學實時研究組的SNU-RT測試程序中集中選取了17個典型的嵌入式程序，加入基準測試集，然后基于這些測試用例，對三個程序數值性質分析工具（PolySpace、Frama-C和CAI）進行測試評價，并給出了工具分析能力的對比結果。

②代碼級可信保障技術的可配置集成方法。提出了一種抽象解釋技術與SMT技術的集成方法，可以提高程序全局分析的精度。首先，根據塊劃分策略，把整個程序劃分為一個個程序塊；然后，程序塊的遷移語義采用SMT公式來精確編碼，塊間信息的傳遞使用抽象域表示；在出程序塊時，把SMT公式抽象為抽象域表示；在循環頭，采用抽象域上的加寬操作，保證分析的終止性。本重大研究計劃在軟件驗證基準測試程序集SV-COMP上開展了實驗，單個程序最大代碼規模超過千行。通過實驗驗證了塊級抽象解釋分析方法的有效性：對于所選基準測試集，采用這種集成方法能比語句抽象解釋方法多證明一倍以上的性質。本成果發表在VMCAI 2017國際學術會議上。

③基于輸出整合的代碼級可信保障工具集成框架。針對多個代碼級可信保障工具的集成問題，開發了一個軟件安全性分析平臺（software security analysis platform, SSAP），其中集成了一些程序分析工具，支持對軟件編程規范、運行時錯誤（如數組越界、內存泄漏、空指針解引用、除零等）的檢查。該平臺采用B/S系統架構，各程序分析工具的輸出數據被集成到數據庫中，用戶通過客戶端提交分析請求和查看綜合的分析結果。該平臺已經得到實際應用。

1.2.3 學科交叉情況

本重大研究計劃在學科布局和研究內容方法等方面都很好地體現了多學科的交叉、融合與集成。

（1）學科布局的學科交叉

在學科布局方面，本重大研究計劃的內容涵蓋了信息科學、數學物理科學、管理科學等學科領域。在項目立項部署方面，有交叉背景的項目獲得了鼓勵和支持。在107個獲得支持的項目中，有8個項目為信息科學與其他科學交叉項目（5個信息科學與管理科學交叉項目，3個信息科學與數學物理科學交叉項目）。

（2）研究內容和方法的學科交叉

在研究方面，誤差可控的軟件與算法設計體現了在可信軟件構造與驗證中信息科學與數學物理科學的交叉。“高性能科學計算應用軟件的可信構造方法及基礎算法研究”項目基于JASMIN框架2.0版及新研制的可信軟件模塊，集成可信的基礎數值并行算法，發展了激光聚變二維輻射流體力學總體LARED-H程序。運用該程序實現了美國國家點火裝置基準靶的全過程數值模擬。通過與美國模擬結果的對比，驗證了該程序具有一定的可信度。

重點支持項目“基于計算機代數的嵌入式軟件分析與驗證方法及工具”是信息科學與數學物理科學交叉的突出代表。該項目探索了程序驗證的第三種途徑——符號計算新途徑。它應用計算機代數方法和工具，進一步加深了對程序驗證的不變量生成、程序終止性分析以及實時和混成系統驗證方面的理論研究，取得了一些重要進展和階段性成果：研究了如何將嵌入式軟件分析和驗證中的問題歸結成數學問題，并應用計算機代數方法求解這些問題，建立了若干新的嵌入式軟件分析驗證方法；開發了一個工具原型，能調用DISCOVERER做基于半代數系統求解的驗證工作，也能調用基于邏輯的證明器Isabelle。該項目一個突出特點是它所基于的數學工具和形式化工具是由中國學者原創的。重點支持項目“面向C4KISR重大應用領域軟件可信性需求分析方法與攻擊性實驗驗證環境研究”提出了一個基于因素空間理論的C4KISR系統軟件可信性結構模型，建立了C4KISR系統軟件可信性因素空間理論。

信息科學與管理科學交叉對軟件可信性度量與建模體系的建立、可信軟件過程管理發揮了重要的作用。“可信軟件過程管理及風險控制模型和方法研究”項目研究了可信過程的基本屬性和度量體系，建立了支持可信屬性實現和風險模型，提出了可信軟件過程域和支持可信過程能力評價的軟件過程可信度模型，形成了風險驅動的可信軟件過程模型框架。主要成果包括：①建立了覆蓋軟件生命周期的過程數據模型，采集了軟件過程中影響可信性的過程和產品數據；②根據軟件過程可信度模型，建立了合理的、符合軟件組織商業目標和領域產品特征的可信軟件過程；③提出了基于過程的證據模型和基于證據的可信性評估方法；④提出了缺陷報告和代碼變更之間缺失關聯關系的自動化修復方法以及基于模糊關聯規則挖掘降低系統性偏差的缺陷修復時間預測方法；⑤支持軟件組織在項目環境下動態拼裝和組建貫穿軟件生命周期的、風險度可信的、有數據支持的可信軟件過程管理及風險管理模型，提出了證據驅動的可信軟件過程管理方法；⑥能夠評估軟件組織的軟件過程可信能力。

在許多項目的研究方法和途徑上，運用網絡科學、人工智能（機器學習）方法和手段開展研究，這也體現了不同學科方法間的交叉。復雜網絡在軟件可信性的研究中展示了其生命力。例如，基于函數調用應用程序編程接口（application programming interface, API）的軟件網絡方法，發現基于調用API的軟件網絡滿足無尺度網路的特性，其節點和邊的屬性可以表征軟件特征，有助于劃定計算機病毒與正常軟件的分割線。