Formal models for verifying multi-threaded recursive programs

在这项研究中，我们提出了一种根据给定的安全规范在给定的递归程序中自动插入用于访问控制的检查语句的方法。基于历史的访问控制(HBAC)被认为是访问控制模型。从信息流的角度给出了系统的安全规范。当我们将S中的每个安全类视为一个类型时，我们说一个程序P满足一个规格说明S，如果P是类型安全的。我们首先将问题定义为在给定的程序P中插入检查语句以获得对给定的规格说明S是类型安全的程序P‘的问题。这个类型系统是健全的，如果程序P对规格说明S是类型安全的，则P对S具有非干涉性。其次，证明了该问题是co-NP-Hard的，并提出了一个解决该问题的定点计算算法。基于我们实现的系统的实验结果表明，该方法可以在合理的时间内工作。

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.