資源感知的程式邏輯理論及資源安全性推理

《資源感知的程式邏輯理論及資源安全性推理》是依託深圳大學，由秦勝潮擔任項目負責人的面上項目。

基本介紹

• 中文名：資源感知的程式邏輯理論及資源安全性推理
• 項目類別：面上項目
• 項目負責人：秦勝潮
• 依託單位：深圳大學

項目摘要

電腦程式的運行離不開系統資源，如記憶體，CPU時間，能源供給等。合理、正確地使用這些系統資源是程式安全性和正確性的一個重要方面。錯誤或不合理的資源使用行為可能導致軟體出錯、系統崩潰，甚至可能危及人們的生命財產安全。因此，程式的資源安全性和正確性是軟體安全可靠性的一個非常重要的方面。本項目的研究目標是構建對程式資源使用行為的自動分析與驗證的基礎理論以及資源安全性的推理技術。著重研究操作動態創建數據結構的程式的資源安全性和正確性，重點關注這類程式對系統資源使用和消耗的各種重要特性，並研究其理論模型和分析驗證技術。本項目研究重點集中如下幾個方面：在分離邏輯的基礎上構建資源感知的規範描述語言；定義程式語言的資源感知語義； 搭建資源感知的程式驗證邏輯框架和相應的推理機制；以及設計針對程式資源使用行為的靜態分析算法。

結題摘要

隨著計算機技術的高速發展，電腦程式及設備已經大量套用於人們生活的方方面面。資源使用是程式行為的一個重要方面。人們通常更多的關注程式的功能正確性而忽略了資源使用的安全性和正確性。鑒於此，對各類系統資源（如記憶體，CPU，能量，時間）的合理使用是程式設計、分析與驗證的一個重要需求。尤其是在開發運行於安全攸關係統和資源受限系統之上的軟體程式時，如何確保程式對資源合理有效的使用是構建安全可信軟體的一個重要而迫切的前沿課題。 本項目研究用於程式資源使用行為的形式化分析與驗證的理論與技術。為了解決程式資源使用行為和資源需求的規範描述以及資源安全性等的驗證問題，本項目設計了面向各種資源的規範描述子語言，包括面向記憶體資源的規範描述子語言，面向時間資源的規範描述子語言，面向（由資源使用造成的）能量消耗的規範描述子語言，以及引入結構規範。同時，本項目定義了面向各種特定資源的程式語義，包括面向記憶體資源的語義，面向時間資源的語義，面向能源（資源使用）的語義和面向組合抽象域的規範的雙向推演抽象語義。在基於上述子語言及其語義的定義，本項目建立了程式驗證機制，包括面向記憶體資源的基於分離邏輯的程式驗證框架，面向時間資源的基於代數的邏輯推理系統，支持結構規範的程式驗證系統，面向作業系統的自動驗證系統，以及面向網路協定的驗證系統。最後，本項目提出了基於抽象解釋的方法來分析程式對系統資源操作和使用的行為，包括面向資源使用的靜態分析方法，基於測試、學習和驗證的抽象算法，帶非區域的時態自動機的包含算法，基於GPU加速和並行化的提速算法，以及面向不同場景的資源分析與最佳化算法。項目的研究內容不僅有望為軟體在系統資源使用行為方面的檢測和評估提供一套行之有效的形式化方法和理論框架，而且還實現一套有望進一步最佳化並套用到安全攸關係統軟體和資源受限系統軟體的開發之中的原型工具集。