基于Petri网的强制访问控制模型及其安全分析

摘要：

强制访问控制模型(MAC)是一种重要的安全模型.在多级安全的格模型和Bell-LaPadula安全模型的基础上,对MAC安全模型进行了形式化描述,并给出了与其等价的着色Petri网模型.在Petri网状态可达图的基础上,对MAC模型的有关安全属性,如主体访问客体的时序关系,主体访问的可达性,因主体的动态安全级访问而存在的安全隐患以及因主体对客体的间接访问而导致敏感信息的可推测性等进行了较为详细地分析.通过对一个安全模型的范例分析,结果表明:基于Petri网的安全模型的分析方法可以充分利用现有的可达图的分析方法来对系统安全模型的有关性质进行分析和验证,能够在安全模型的设计和实现阶段有效地改善系统的总体安全策略.

关键词：格、Petri网、可达性、安全分析、强制访问控制模型

所属期刊栏目：17

分类号：TP301(计算技术、计算机技术)

资助基金：国家重点基础研究发展计划（973计划）;国家自然科学基金;香港研究资助局项目

在线出版日期：2005-12-08（万方平台首次上网日期，不代表论文的发表时间）

页数：共6页

页码：82-87