《嵌入式軟體可組合信息流安全驗證機制研究》是依託西安電子科技大學，由孫聰擔任項目負責人的青年科學基金項目。
基本介紹
- 中文名：嵌入式軟體可組合信息流安全驗證機制研究
- 項目類別：青年科學基金項目
- 項目負責人：孫聰
- 依託單位：西安電子科技大學
中文摘要,結題摘要,
中文摘要
信息流安全是嵌入式軟體安全性研究需要考慮的重要問題。本項目針對嵌入式軟體組件化設計過程所引入的信息流安全問題，以驗證機制的精確性、可擴展性、可靠性為側重點，研究異構組件化嵌入式軟體的可組合信息流安全屬性的形式化定義和精確驗證。在具體組件模型框架下，通過運用模型抽象與變換技術、自動程式驗證技術和基於契約的推理技術，實現分層低耦合的信息流安全屬性驗證機制，並說明該驗證機制的精確性、可靠性和可組合性，最終提供一種高精確性、高可靠性、可擴展性良好的信息流安全驗證框架。項目將對複雜嵌入式軟體安全性驗證理論和技術的發展提供重要的推動和支持。
結題摘要
本項目針對嵌入式軟體組件化設計過程所引入的信息流安全問題，研究異構組件化嵌入式軟體的可組合信息流安全屬性的形式化定義和精確驗證。項目主要貢獻如下： 1、提出新的信息流安全屬性（Relaxed Release with Reference Points, R3P），提出“條件持久性”這一新的謹慎性原則，使用下推系統可達性分析驗證程式的R3P屬性，並通過“存儲-匹配”模式的模型變換提高驗證效率。 2、提出將可組合的信息流安全驗證套用於模型驅動的嵌入式軟體開發過程中，對SysML建模語言的IBD圖進行自動抽象，轉化為安全相關的接口自動機，在此基礎上給出了組件安全屬性定義、組合系統安全條件，並實現了相應的判定算法。 3、提出廣義安全接口結構，並在廣義安全結構上定義了支持任意有限格模型的基於安全多執行的無干擾屬性，針對單個組件的安全屬性驗證給出了判定過程算法，針對組合系統的安全，給出了可組合定理證明及其判定算法，並將可組合驗證套用於控制系統安全協定等場景。 4、給出了BIP組件模型的可組合信息流安全驗證方法，將BIP模型抽象為廣義安全接口結構，用於嵌入式組件化系統（以雙余度飛行控制系統為例）的信息流安全驗證。 5、針對服務雲環境下的信息流安全控制問題，提出相應的信息流安全模型和組合驗證算法，並提出了針對智慧型感測器網路中信息流安全驗證的分散式驗證算法。 本項目對組件化軟體模型可組合信息流安全驗證機制的研究成果和工具成果，可用於保證領域特定的嵌入式軟體數據訪問、數據傳遞的機密性，彌補目前航空、工業控制等領域嵌入式軟體安全性驗證中缺乏信息流安全屬性形式化驗證理論、技術和工具的不足，對複雜嵌入式軟體安全性驗證理論和技術的發展提供推動和支持。
