《基於模擬執行的軟體功能規約的安全性驗證》是依託上海交通大學，由陳雨亭擔任項目負責人的青年科學基金項目。
基本介紹
- 中文名：基於模擬執行的軟體功能規約的安全性驗證
- 項目類別：青年科學基金項目
- 項目負責人：陳雨亭
- 依託單位：上海交通大學
項目摘要,結題摘要,
項目摘要
軟體安全是指軟體需要避免由風險因素或條件所導致的事故或損失，它是軟體可信的一個重要參考指標。在軟體需求分析階段為軟體制定功能與安全方面的需求規約，並驗證軟體功能符合安全需求則有助於安全關鍵軟體的開發。然而，形式化的功能規約的安全性驗證方法（如證明等）在實際工程中不容易被使用，靜態分析功能規約的安全性又常常缺乏嚴格性和準確性。本課題將研究模擬執行軟體形式化規約以進行安全性驗證的方法。為此，課題將在SOFL形式化規約語言基礎上研究軟體安全的定義、描述、驗證機制，並建立集成軟體功能及安全約束的需求規約；研究如何模擬執行軟體的形式化規約，並靈活、嚴格地驗證軟體功能的安全性。對軟體的形式化規約進行模擬執行並進行安全性驗證在國內外屬創新工作，我們力求從理論上有所突破，並期望研究成果被推廣套用到實際項目中，從而使軟體產業能更好地套用安全驗證方法，使用戶獲得符合安全需求的軟體。
結題摘要
軟體安全（Software Safety）是軟體可信的一個重要參考指標，它是指軟體需要避免由於風險（Hazard）因素或者條件而導致的事故或損失，即軟體不僅需要完成它所應該完成的任務，也需要避免在各種風險下可能存在的錯誤的、危險的行為。特別是在開發安全關鍵軟體（Safety-Critical Software）過程中，工程人員在需要制定軟體的功能需求規約，也常常需要分析軟體的風險、可能的事故、安全性缺陷、對功能的安全約束等等。實踐表明，制定軟體安全方面的需求，並驗證軟體及其功能規約的安全性（即檢查軟體功能、行為是否滿足安全需求），有助於安全關鍵軟體的開發。課題主要研究軟體及其功能規約中的安全性驗證方法。主要研究內容包括：研究軟體動態行為方面的安全性需求；研究如何利用形式化工程SOFL（Structured Object-Oriented Formal Language）語言為軟體動態行為建模，並制定安全性約束，從而使軟體需求規約既具有可讀性、可理解性，也可以精確地描述系統行為及其安全需求；研究基於SOFL對軟體功能規約進行安全性驗證，即動態執行軟體功能規約，發現規約中存在的安全性缺陷並予以修正；研究對具體軟體進行安全性分析的技術和方法，包括程式指向分析、軟體崩潰預測方法、自動化的程式調試斷點生成方法等。課題主要取得如下研究成果：（1）我們提出一種混成的方法來檢驗SOFL規約的內部一致性。內部一致性是SOFL規約的一種重要屬性。研究的主要思想如下：通過具體或抽象的值來檢查一個規約中Process的可滿足性，以及通過符號執行和推導技術來檢查集成規約的內部一致性，即通過輸入驅動規約執行，並使執行中所有過程的前置條件和後置條件均為真，產生並檢查輸出；（2）我們研究通過方面（Aspect）以描述及集成軟體安全性質、適應軟體演進的架構語言AspectBreeze。特別是，AspectBreeze利用圖文法，保證編織安全方面前後軟體架構在演進過程中的一致性；（3）我們提出通過挖掘軟體功能場景以預測軟體安全缺陷的方法。研究中，我們通過使用k中心點算法聚類函式、生成功能場景，使用C4.5模型預測場景中的軟體安全缺陷；（4）我們提出對軟體進行安全性分析的方法與技術，包括程式執行路徑執行頻率的分析技術、軟體崩潰預測方法、自動化的程式調試斷點生成方法等。
