Verification of control flow based security properties
Verification of control flow based security properties
复制标题
基于控制流的安全属性验证
DOI：
--
复制
发表时间：
1999
期刊：
影响因子：
--
通讯作者：
Tommy Thorn
中科院分区：
文献类型：
--
作者：
T. Jensen;D. L. Métayer;Tommy Thorn
基于软件的安全性的一个基本问题是插入到代码中的本地安全检查是否足以实现全局安全属性。我们介绍了一种形式主义的基础上的两级线性时间时序逻辑指定的全球安全属性有关的程序的控制流，并说明其表达能力与一些现有的属性。我们定义了一个最低限度的，安全专用的程序模型，只包含过程调用和运行时的安全检查，并提出了一个自动的方法来验证，使用本地安全检查的实现满足全球的安全属性。对于一个给定的公式的时序逻辑，我们证明了存在一个约束的状态，必须考虑的大小，以确保公式的有效性：这减少了有限状态模型检查的问题。最后，我们将该框架实例化到为Java（JDK 1.2）提出的安全体系结构中。
A fundamental problem in software based security is whether local security checks inserted into the code are sufficient to implement a global security property. We introduce a formalism based on a two-level linear time temporal logic for specifying global security properties pertaining to the control flow of the program, and illustrate its expressive power with a number of existing properties. We define a minimalistic, security dedicated program model that only contains procedure call and run time security checks and propose an automatic method for verifying that an implementation using local security checks satisfies a global security property. For a given formula in the temporal logic, we prove that there exists a bound on the size of the states that have to be considered in order to assure the validity of the formula: this reduces the problem to finite state model checking. Finally, we instantiate the framework to the security architecture proposed for Java (JDK 1.2).