安全策略模型规范及其形式分析技术研究

Research on formal security policy model specification and its formal analysis

形式化是开发高安全等级计算机系统的核心技术之一,但目前形式开发方法无法直接借助于机器证明获得较之手工证明更加严格的安全策略模型正确性保证,以及安全策略模型和安全功能规范之间的精确对应。通过把安全功能规范开发技术应用于安全策略模型的开发中,提出了一种新颖的安全策略模型形式规范构造方法及其证明机理,从而有效解决了上述问题。还以Bell-LaPadula多级安全策略为实例,具体说明了规范的形式开发和形式分析过程。

Formal method is one of the kernel technologies of developing high security level computer system. But by current formal development method, assurance of security policy model correctness cannot be provided directly using machine proof which is stricter than manual proof, correspondence between security policy model and security functional specification is also hard to achieve. To solve these problems, a new and effective method was proposed for specification constructing and proving by extending the specification technique of security functional specification into the specification of security policy model. Also, BLP model was specified and analyzed as an example.