论文研究 基于Petri网的信息流安全属性的分析与验证.pdf

信息流安全属性的定义均基于不同的语义模型,很难作出比较,以Petri网作为描述安全系统的统一模型,在Petri网上定义四种常见的安全属性,并分析它们之间的逻辑关系。在信息流安全属性验证方面,传统的方法称为展开方法,该方法适用于确定型系统,而对于非确定型系统,该方法是可靠的,但不完备。进一步对Petri网上已经定义的四种属性给出可靠完备的验证算法,并开发出相应的验证工具。最后通过实例说明了验证方法在搜索隐通道方面的应用。