Security Verification of Software with Dynamic Access Control

访问控制策略是描述指定主体可以(或不能或必须)在指定目标上执行指定操作的时间和条件的规则。其行为由策略控制的程序称为策略控制系统(PCS)。在本研究中，我们首先定义了一种简单的策略规范语言。该语言的结构足以描述积极/消极的授权和义务。在此基础上，形式化地定义了P的操作语义，并将P的(安全)验证问题定义为对给定的P-P S和一个目标(称为安全性质)φ，P的每个可达状态是否满足φ的问题.我们已经实现了一个针对PCS的验证工具，其工作原理如下。首先，从PCS抽象出一个下推系统(PDS)，并构造一个接受PDS所有可达状态集合的非确定有限自动机(NFA)。对一个1.7k行复杂义务策略的PCS进行验证，验证时间约为几分钟，表明该验证方法在实际程序中是可行的，并对该方法进行了扩展.通过将PDS扩展到树形结构，定义了TRS的一个子类--广义生长TRS(Growth TRS)。我们证明了对于保持可识别性的任意GG-TRS，LTL(线性时态逻辑)模型检测是可判定的。此外，作为验证方法的应用，我们实现了一个工具来验证给定的XML文档是否满足给定的可访问性准则。我们已经使用该工具验证了美国和日本40个主要组织的约3,000个网页。

A policy for access control is a rule describing when and on which condition a specified subject can (or cannot or must) perform a specified action on a specified target. A program of which behavior is controlled by a policy is called a policy controlled system (PCS). In this research, we first define a simple policy specification language. The language has a structure sufficient for describing positive/negative authorization and obligation. We formally define the operational semantics of PCS based on the language.Next, we define the (safety) verification problem for PCS as the problem to decide for a given PCS S and a goal (called safety property) φ, whether every reachable state of P satisfies φ. We have implemented a verification tool for PCS, which works as follows. First, a pushdown system (PDS) is abstracted from a PCS and a nondeterministic finite automaton (NFA) which accepts the set of all reachable states of the PDS is constructed. The computation time is about a few minutes for verifying a PCS of 1.7K lines with complex obligation policy, which shows that the proposed verification method is feasible for real world programs.We extend the proposed method for verifying the property of term rewrite system (TRS). A subclass of TRS called generalized growing TRS (GG-TRS) is defined by extending PDS to tree structure. We show that for an arbitrary GG-TRS which preserves recognizability, an LTL (linear temporal logic) model checking is decidable. Also, as an application of the verification method, we have implemented a tool which verifies whether a given XML document satisfies a given accessibility guideline. We have verified about 3,000 web pages of forty major organizations in the U.S.A.and Japan using the tool.