Formal models for verifying multi-threaded recursive programs

点击翻译按钮获取中文摘要

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.