Security Verification of Software with Dynamic Access Control

动态访问控制软件的安全验证

• 批准号: 14580376
• 负责人: SEKI Hiroyuki
• 金额: $ 2.05万
• 依托单位: NARA INSTITUTE OF SCIENCE AND TECHNOLOGY
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Scientific Research (C)
• 财政年份: 2002
• 资助国家: 日本
• 起止时间: 2002 至 2003
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/en/grant/KAKENHI-PROJECT-14580376/
• 关键词: ACESS CONTROL; SECURITY; SAFETY; VERIFICATION; MODEL CHECKING; POLICY

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.

访问控制策略是描述指定主体可以(或不能或必须)在指定目标上执行指定操作的时间和条件的规则。其行为由策略控制的程序称为策略控制系统(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个网页。

项目成果

Hiroyuki Seki, Naoya Nitta, Yoshiaki Takata, Shigeta Kuninobu: "Infinite State Model Checking and Its Application to Software Verification"第2回クリティカルソフトウェアワークショップ予稿集. 20-22 (2003)

Hiroyuki Seki、Naoya Nitta、Yoshiaki Takata、Shigeta Kuninobu：“无限状态模型检查及其在软件验证中的应用”第二届关键软件研讨会论文集 20-22 (2003)。

八木勲, 高田喜朗, 関浩之: "ラベル付き遷移システムに基づくアスペクト指向プログラムのモデル化"電子情報通信学会技術研究報告. SS2003-46. 1-6 (2004)

Isao Yagi、Yoshiro Takada、Hiroyuki Seki：“基于标记转换系统的面向方面的程序建模” IEICE 技术报告 SS2003-46 (2004)。

Y.Takata, T.Nakamura, H.Seki: "Accessibility Verification of WWW Documents by an Automatic Guideline Verification Tool"37^<th> Annual Hawaii Int'l Conference on System Sciences, the Digital Documents and Media Track. (Full Paper : CD-ROM). Abstract:98 (20

Y.Takata、T.Nakamura、H.Seki：“通过自动指南验证工具对 WWW 文档进行可访问性验证”第 37 届夏威夷系统科学、数字文档和媒体领域国际会议。

毛利寿志, 高田喜朗, 関浩之: "システムの内部状態を導入した信用管理モデル"電子情報通信学会2004年総合大会講演論文集. A-7-2 (2004)

Hisashi Mori、Yoshiro Takada、Hiroyuki Seki：“结合系统内部状态的信任管理模型”2004 年电子、信息和通信工程师协会大会记录 A-7-2 (2004)。

Hitoshi Ohsaki, Hiroyuki Seki, Toshinori Takai: "Recognizing Boolean Closed A-Tree Languages with Membership Conditional Rewriting Mechanism"14^<th> Int'l Conference on Rewriting Techniques and Applications. LNCS 2706. 483-498 (2003)

Hitoshi Ohsaki、Hiroyuki Seki、Toshinori Takai：“利用成员条件重写机制识别布尔闭合 A 树语言”第 14 届重写技术与应用国际会议。