Formal models for verifying multi-threaded recursive programs

在本研究中，我们提出了一种根据给定的安全规范在给定的递归程序中自动插入访问控制检查语句的方法。假设基于历史的访问控制（HBAC）作为访问控制模型。从信息流的角度给出了安全规范。如果一个程序P是类型安全的，当我们把S中的每个安全类看作是一个类型时，我们就说程序P满足规范S。我们首先将该问题定义为在给定程序P中插入检查语句以获得对于给定规范S是类型安全的程序P'的问题。这个类型系统是健全的，因为如果一个程序P对于规范S是类型安全的，那么P对于S具有不干扰性质。接下来，我们证明了该问题是共同np困难的，并提出了一个不定点计算算法来解决该问题。基于所实现系统的实验结果表明，所提出的方法可以在合理的时间内工作。

In this study, we proposed a method for automatically inserting check statements for access control into a given recursive program according to a given security specification. A history-based access control (HBAC) was assumed as the access control model. A security specification is given in terms of information flow. We say that a program P satisfies a specification S if P is type-safe when we consider each security class in S as a type. We first defined the problem as the one to insert check statements into a given program P to obtain a program P' that is type-safe for a given specification S. This type system is sound in the sense that if a program P is type-safe for a specification S, then P has noninterference property for S. Next, the problem was shown to be co-NP-hard and we proposed a fix-point computation algorithm for solving the problem. The experimental results based on our implemented system showed that the proposed method can work within reasonable time.