基于Petri网的保密性策略建模与验证

Petri net-based modeling and verification of confidentiality policy

为了对实施了具体保密性策略的系统、进程或工作流的保密性进行严格有效的分析与验证,提出了一种基于Petri网的保密性策略建模与验证方法.首先给出保密性策略基于Petri网的形式化描述,为系统建立Petri网模型;然后在此模型下利用保密性策略基于Petri网的形式化描述以及覆盖图对系统的保密性进行分析与验证,以判断系统是否符合保密性策略的要求.由于给定的系统Petri网模型覆盖图可以自动生成,因此可以利用其对系统的保密性进行自动分析与验证.通过一个进程实例阐述了该方法的原理和实施过程.

For analyzing and verifying the confidentiality of system,process or workflow implemented a specific confidentiality policy,this paper proposed a Petri net-based approach to model and verify the confidentiality policy.Confidentiality policy was formally described via Petri net.In Petri net model of system,formal description of confidentiality policy and coverability graph were used to determine whether the system model is match the requirement of the policy.For a given Petri net model of system,the coverability graph could be automatically generated,thus it could be utilized to automatically analyze and verify the confidentiality of system.The theoretical feature and the implementation of the approach are addressed through a sample process.