《基於安全屬性建模的協定安全性測試理論與方法研究》是依託西安電子科技大學，由楊超擔任項目負責人的青年科學基金項目。
基本介紹
- 中文名：基於安全屬性建模的協定安全性測試理論與方法研究
- 項目類別：青年科學基金項目
- 項目負責人：楊超
- 依託單位：西安電子科技大學
中文摘要,結題摘要,
中文摘要
本項目主要研究協定的安全性測試理論與方法。首先，重點關注協定安全屬性的形式化方法，研究基於狀態機理論模型的安全屬性擴展建模機制；借鑑搜尋領域的語義研究成果，研究協定行為的語義建模方法，並將兩者有機結合，進一步研究安全屬性擴展下的協定狀態時序與行為語義的混合建模理論與方法；其次，在該混合建模理論的指導下，結合模型檢測技術，建立適應於安全性測試需求動態變化的邏輯約束公式和檢測規則，研究動態安全性測試例生成算法；最後，研究測試結果的抽象化方法，及其與安全威脅等級的關聯方法，設計統一、定量的測試結果評價標準和安全態勢評估方法，實現測試結果的可度量性和可控性，增強安全性測試結果對協定系統安全防護的指導功能。我們希望在協定的安全性測試理論和方法上有一定的突破，為高效、準確和可靠的協定安全性測試與評估探索和開拓系統的理論基礎和指導方法。
結題摘要
作為網路和分散式系統的基石，協定的正確性決定了整個計算機網路及系統的穩固與安全。但協定實現因其固有的複雜性，必然會引入實現的不一致、漏洞或錯誤，這迫切需要能適應安全需求動態變化的測試方法來進一步驗證協定。因此，本項目主要研究協定的安全性測試理論與方法。項目取得的主要成果包括： 1、提出了一種密碼學可證明安全的且高效的數據所有權證明協定與測試方案，實現了對安全協定的安全屬性進行了形式化建模，並實現了對模型化後的安全協定測試，結果表明效果良好。該成果發表在SCI檢索源期刊上。 2、提出了一個新的基於客戶端加密檔案的去重複刪除安全協定與測試方案，該方案基於擴展邏輯規則系統，建立新協定的動態安全需求和檢查規則，支持多客戶端加密檔案的去重複刪除場景。成果發表在SCI檢索源期刊上，並申請了國家發明專利。 3、提出了一種新的基於語義的安全協定測試方法，並進行了實際系統測試將安全協定的語義進行形式化並與邏輯規則結合，並利用該方法發現了2個國內著名網際網路公司新浪公司的“新浪微博APP”和“騰訊移動QQ”APP的線上認證協定的漏洞，也是首次將理論成果結合實際的安全協定測試獲得的成果。該成果發表在國內最好的學術期刊之一《計算機學報》上，並申請了國家發明專利。 4、提出了協定認證性安全屬性測試方法，設計了一種形式化安全屬性的有限狀態機擴展模型SPG-EFSM，精確定義了協定認證安全屬性，實現了協定認證性攻擊算法，結果表明：發現了廣泛存在於Woo-lam協定及其各種更新版本當中的漏洞，以及μTESLA協定的認證漂移問題，並指出了它們潛在的安全性問題。該成果在安全協定的屬性建模與安全性測試取得了實質性的突破，並將相關成果發表在了國內最好的學術期刊之一《電子學報》上，並正在申請國家發明專利。 本項目在協定的安全性測試理論和方法上有一定的突破，為高效、準確和可靠的協定安全性測試與評估探索和開拓系統的理論基礎和指導方法。
