Security Verification of Software with Dynamic Access Control

访问控制策略是一种规则，描述了指定主体何时以及在何种条件下可以（或不能或必须）对指定目标执行指定操作。其行为由策略控制的程序被称为策略控制系统（PCS）。在这项研究中，我们首先定义了一个简单的策略规范语言。该语言具有足够的结构来描述积极/消极的授权和义务。基于该语言形式化地定义了PCS的操作语义，并将PCS的安全性验证问题定义为对给定的PCS S和目标（称为安全性）φ，判定P的每个可达状态是否满足φ的问题。我们已经实现了一个验证工具的PCS，其工作原理如下。首先，下推系统（PDS）是从PCS抽象和非确定有限自动机（NFA），它接受的PDS的所有可达状态的集合被构造。对一个1.7K行的复杂责任策略的PCS进行验证的计算时间约为几分钟，这表明所提出的验证方法对真实的世界程序是可行的。通过将PDS扩展到树结构，定义了广义生长TRS（GG-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.