《基於最小信任基的可信系統構建與驗證方法研究》是依託中國科學技術大學，由黃文超擔任項目負責人的面上項目。
基本介紹
- 中文名：基於最小信任基的可信系統構建與驗證方法研究
- 項目類別：面上項目
- 項目負責人：黃文超
- 依託單位：中國科學技術大學
中文摘要,結題摘要,
中文摘要
現如今，我們的國防、能源、金融、醫療正遭受著嚴重的計算機系統和網路安全威脅與攻擊。其中，我們面臨三個重要系統安全問題：系統平台易被篡改、軟體設計易出漏洞、遠程結點難以信任。本課題擬研究基於最小信任基的可信系統構建與驗證技術：研究基於動態可信根的系統數據完整性度量與保護技術，防止敵方惡意篡改或竊取數據，縮小信任基體積以減少設計漏洞的可能，同時儘可能提供豐富上層接口以降低套用軟體的設計難度；研究基於Event-B的數據安全形式化建模、精化與證明技術，更細粒度地確保底層系統及套用軟體不存在設計漏洞；研究基於TPM2.0的遠程身份及平台可信性證明技術，提高遠程證明的可信性及高效性；研究基於Pi演算的可信認證協定形式化驗證技術，確保遠程協定的設計安全，並減少協定的驗證難度及工作量。本課題的目的就是提供一種最小信任基系統，解決平台完整性、設計可靠性、遠程可證明性問題，為推進系統安全研究發展作出貢獻。
結題摘要
計算機系統與網路安全面臨三個研究難題：平台完整性、設計可靠性、遠程可信性問題。最小信任基技術已成為解決上述問題的熱門研究方法。然而，這些研究存在諸多不完善的地方，以致於其技術仍未商用及廣泛運用。其中，最重要的兩個研究挑戰在於：(1)如何權衡可信基的系統體積與安全風險，使用兩者均達到令人滿意的程度；(2)如何設計有效的形式化驗證方法，以方便地證明每一個最小信任基以及整個系統的安全。為此，本課題研究上述三個難題、兩個挑戰，為推進系統安全研究發展作出貢獻。我們的項目主要貢獻如下：(1) 提出一套安全協定通用全自動形式化驗證平台我們提出一套安全協定通用全自動形式化驗證平台SmartVerif。我們採取深度學習與形式化驗證技術相結合的方法，研究基於動態策略的安全協定形式化自動驗證技術，以突破並解決傳統形式化自動驗證中的狀態空間爆炸問題，並實現對主流網路安全協定的自動化證明。SmartVerif可以挖掘給定目標的安全協定與軟體的所有安全漏洞，確保網路安全協定不會被攻擊者攻破。該成果已被信息安全領域國際頂級學術會議USENIX Security 2020接收。(2) 提出一套保護系統狀態連續性形式化建模與驗證框架我們針對保護系統狀態連續性解決方案提出了一個形式化建模與驗證框架，該框架使用精化策略將抽象動作具體化為某個具體狀態連續性解決方案的防護行為。我們在Coq證明工具中實現了該框架，並證明了一個稱為Memior的狀態連續性解決方案保證了受保護模組的狀態連續性。(3) 提出一套禁止系統形式化建模與驗證的通用框架我們提出了一個禁止系統形式化建模與驗證的通用框架，該框架支持分析基於不同技術的禁止系統，通過逐步精化減少了對新禁止系統的形式驗證的複雜性。我們在Coq驗證工具中實現了該框架，並在發現了在使用禁止系統時的潛在安全威脅。在項目執行階段，發表26篇論文，其中包括CCF A類論文6篇（期刊論文2篇，會議論文4篇），以及獲得14項國內專利，完成預期研究計畫。
