摘要
信息流安全属性的定义均基于不同的语义模型,很难作出比较,以Petri网作为描述安全系统的统一模型,在Petri网上定义四种常见的安全属性,并分析它们之间的逻辑关系。在信息流安全属性验证方面,传统的方法称为展开方法,该方法适用于确定型系统,而对于非确定型系统,该方法是可靠的,但不完备。进一步对Pe-tri网上已经定义的四种属性给出可靠完备的验证算法,并开发出相应的验证工具。最后通过实例说明了验证方法在搜索隐通道方面的应用。
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.
出处
《计算机应用研究》
CSCD
北大核心
2010年第12期4638-4642,共5页
Application Research of Computers
基金
国家自然科学基金资助项目(60773049)
江苏大学高级人才科研启动基金资助项目(07JDG014)
江苏省高校自然科学基金资助项目(08KJD520015)
国家教育部博士点基金资助项目(20093227110005)
关键词
PETRI网
无干扰属性
广义无干扰属性
广义非推断属性
可分离属性
Petri net
noninterference property
generalized noninterference property
generalized noninference property
separability property
