基于Petri网的信息流安全属性的分析与验证*

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

Petri net-based analysis and verification of information flow security properties

The definition of information flow security properties are based on different semantic model, which is difficult to make comparison between them. This paper used Petri net as unified model to describe the security system, defined four security properties on Petri net and analyzed the logic relationship between them. The traditional algorithmic verification method for information flow was known as unwinding method, which was not sufficient and could be just used in deterministic system. The second work of this paper was giving a sufficient algorithmic verification method for the security properties had been defined and programming to implement the method. Finally, it shows the application of this method in covert channel.