《基於標號Petri網的行為安全互模擬研究》是依託同濟大學，由劉關俊擔任項目負責人的面上項目。
基本介紹
- 中文名：基於標號Petri網的行為安全互模擬研究
- 項目類別：面上項目
- 項目負責人：劉關俊
- 依託單位：同濟大學
中文摘要,結題摘要,
中文摘要
安全性是網路環境下的系統（如網上銀行交易系統）所關注的重要問題之一，行為安全性策略為預防網路環境下的欺詐等不法行為提供保障。不同的行為安全性策略可致使具有相同功能的兩個系統具有不同的安全性，從而導致它們的行為並不等價，這也是行為安全性策略能夠預防不法行為的原因所在。如何形式化刻畫具有不同行為安全性策略但完成相同功能的兩個系統的（不）等價性以及如何形式化比較兩個不等價系統的安全性強弱是支撐這些系統開發的理論所關心的兩個核心問題。我們發現經典的互模擬理論與語言等價理論不適用於所有的面向安全的系統的需要，不能回答上述問題。本項目發展經典的互模擬理論，提出基於標號Petri網的行為安全互模擬，研究面向安全的行為等價理論以及行為安全性層級體系。據我們所知，目前還沒有相關工作從形式化角度去研究這些問題。因此，本項目的研究成果是對形式化方法與互模擬理論的一個有益擴充，為面向安全的系統的設計提供理論支撐。
結題摘要
本成果圍繞互動式並發系統的行為安全性與行為正確性，基於Petri網，從控制流、數據流、時間、認知四個維度為系統建模，重點分析驗證系統隱私安全性、行為健壯性、行為確定性等。主要創新成果如下：1. 創新性提出了安全互模擬的概念，在考慮系統的不同安全策略的情況下，定性評價系統安全性是否等價等價，對安全行為定性的分層，為系統安全性設計提供了理論依據。2. 創新性提出帶有知識的Petri網（KPN），既描述系統執行邏輯的進展又能描述每個互動主體知識的進展與獲得的知識。利用關於知識的計算樹邏輯CTLK描述系統關注的隱私安全的設計需求，定義了KPN的相似可達圖，基於此要給出了驗證CTLK的算法，為隱私安全驗證提供的新的有效途徑。3. 創新性提出了Petri網的元展這一分析技術，給出了基於元展的判定系統健壯性的充要條件；更為一般的，給出了基於元展的檢測CTL的算法，開發了相關工具，有效緩解狀態爆炸問題。4. 創新性提出了實時互動式系統的時間健壯性，利用互模擬理論證明了一個系統是時間健壯的，則它不存在不確定性行為，而不確定性的行為嚴重影響了實時系統的安全可靠性能。5. 創新性利用Petri網的展開分析由真並發導致的數據不一致性問題，避免交錯語義下可達圖技術不能反映真並發的缺陷。我們也開發了相關的工具，實驗展示了我們方法的有效性。
