可信軟體構造理論與方法研究

《可信軟體構造理論與方法研究》是依託武漢大學，由何炎祥擔任項目負責人的重大研究計畫。

基本介紹

• 中文名：可信軟體構造理論與方法研究
• 項目類別：重大研究計畫
• 項目負責人：何炎祥
• 依託單位：武漢大學

項目摘要

由於軟體的運行環境越來越開放，規模不斷增大，行為日益複雜，使得軟體的可信性面臨著嚴峻的挑戰，如何構造可信軟體受到了工業界和學術界越來越多的重視和關注。近年來，國內外對可信軟體展開了廣泛研究，但可信軟體的構造仍然缺乏一套系統的成熟的理論和方法。本項目擬採用理論研究和實證研究相結合的方法，研究可信軟體的系統化開發理論、方法與技術，設計並實現可信軟體開發工具和運行支撐平台及環境。主要研究內容包括：1、可信軟體開發過程模型，重點研究開發過程中的可信保障機制；2、面向可信軟體的需求建模及基於行為的需求模型驗證方法；3、可信軟體體系結構設計、構件化實現及基於可信編譯的程式代碼生成方法；4、可信軟體的測試與評估方法；5、可信軟體開發工具的設計與實現以及開發平台的集成方案；6、面向國產家電嵌入式可信軟體典型示範套用。

結題摘要

由於軟體的運行環境越來越開放，規模不斷增大，行為日益複雜，使得軟體的可信性面臨著嚴峻的挑戰，如何構造可信軟體受到了工業界和學術界越來越多的重視和關注。近年來，國內外對可信軟體展開了廣泛研究，但可信軟體的構造仍然缺乏一套系統、成熟理論和方法。本項目採用理論研究和實證研究相結合的方法，研究可信軟體的系統化開發理論、方法與技術，設計並實現可信軟體開發工具和支撐平台。主要研究成果如下： 1、提出了一個基於可信鏈的可信軟體開發過程模型，並提出了一整套可信軟體構造方法和技術，研發了相應的開發工具，形成了較為完整的可信軟體開發技術體系和套用平台。 2、在需求建模與驗證階段，提出了一種基於多視點和軟體行為的需求建模方法和需求模型的檢測方法，從而獲得可信的需求模型。 3、在設計階段，提出了一種體系結構多維可信關注點模型和一種高可信體系結構描述語言(DADL)，實現了從需求到設計模型的平滑過渡和精確跟蹤，並提出了一個異常處理與驗證框架。 4、在實現階段，提出了三次編譯，兩次對比的編譯器驗證方法。該方法結合編譯後代碼可信性加強技術，保障了可信目標代碼的生成。基於該技術自主研發的HRCC可信編譯器得到大規模商業套用，並提出了不同體系結構下低能耗和耗損均衡的編譯最佳化方法，降低快取動態能耗達38%。 5、在測試與評估階段，構建了一個面向雲環境的系統行為採集與保護實驗平台，其核心技術被華為有限公司採用；設計和實現了一個基於漏洞庫的可信性評估工具。 本項目獲授權發明專利5項, 軟體著作權5項，出版專著2部，發表SCI論文11篇，EI論文34篇。以陳國良和周巢塵兩院士為正副組長的鑑定委員會認為該成果創新特色明顯，整體達國際先進水平。本項目成果獲得2014年湖北省科技進步一等獎。