基于标号Petri网的行为安全互模拟研究

Security has been one of the most important topics focused on by networked systems such as internet-bank trading system. Behavioral security policies can prevent illegal behaviors such as internet frauds. Different behavioral security policies result in different securities for two systems with the same functions and thus lead to the non-equivalence of their behaviors, which is the reason why they can prevent illegal behaviors. Therefore, the following two questions are the basis for the theory supporting the development of these systems: 1) how to utilize the formal method to define the (non-)equivalence of two systems with the same functions but different secure policies? and 2) how to compare the securities of two nonequivalent systems by using the formal method? We find that bisimulation theory and language-equivalence theory cannot fit all security-oriented systems or cannot answer the above questions. This project proposes secure bisimulation of behavior based on labeled Petri nets. On the basis of secure bisimulation, we will study two theoretical systems: security-oriented behavior equivalence and behavioral security level. With the best of our knowledge, there has not been the related work on these questions. Therefore, our research results will develop the formal method and bisimulation theory, and thus theoretically support the design of these systems.

安全性是网络环境下的系统（如网上银行交易系统）所关注的重要问题之一，行为安全性策略为预防网络环境下的欺诈等不法行为提供保障。不同的行为安全性策略可致使具有相同功能的两个系统具有不同的安全性，从而导致它们的行为并不等价，这也是行为安全性策略能够预防不法行为的原因所在。如何形式化刻画具有不同行为安全性策略但完成相同功能的两个系统的（不）等价性以及如何形式化比较两个不等价系统的安全性强弱是支撑这些系统开发的理论所关心的两个核心问题。我们发现经典的互模拟理论与语言等价理论不适用于所有的面向安全的系统的需要，不能回答上述问题。本项目发展经典的互模拟理论，提出基于标号Petri网的行为安全互模拟，研究面向安全的行为等价理论以及行为安全性层级体系。据我们所知，目前还没有相关工作从形式化角度去研究这些问题。因此，本项目的研究成果是对形式化方法与互模拟理论的一个有益扩充，为面向安全的系统的设计提供理论支撑。

本成果围绕交互式并发系统的行为安全性与行为正确性，基于Petri网，从控制流、数据流、时间、认知四个维度为系统建模，重点分析验证系统隐私安全性、行为健壮性、行为确定性等。主要创新成果如下：.1. 创新性提出了安全互模拟的概念，在考虑系统的不同安全策略的情况下，定性评价系统安全性是否等价等价，对安全行为定性的分层，为系统安全性设计提供了理论依据。.2. 创新性提出带有知识的Petri网（KPN），既描述系统执行逻辑的进展又能描述每个交互主体知识的进展与获得的知识。利用关于知识的计算树逻辑CTLK描述系统关注的隐私安全的设计需求，定义了KPN的相似可达图，基于此要给出了验证CTLK的算法，为隐私安全验证提供的新的有效途径。.3. 创新性提出了Petri网的元展这一分析技术，给出了基于元展的判定系统健壮性的充要条件；更为一般的，给出了基于元展的检测CTL的算法，开发了相关工具，有效缓解状态爆炸问题。.4. 创新性提出了实时交互式系统的时间健壮性，利用互模拟理论证明了一个系统是时间健壮的，则它不存在不确定性行为，而不确定性的行为严重影响了实时系统的安全可靠性能。.5. 创新性利用Petri网的展开分析由真并发导致的数据不一致性问题，避免交错语义下可达图技术不能反映真并发的缺陷。我们也开发了相关的工具，实验展示了我们方法的有效性。