Synthesising verified access control systems through model checking
Synthesising verified access control systems through model checking
复制标题
通过模型检查合成经过验证的访问控制系统
DOI：
--
复制
发表时间：
2008
期刊：
影响因子：
--
通讯作者：
Dimitar P. Guelev
中科院分区：
文献类型：
--
作者：
Nan Zhang;M. Ryan;Dimitar P. Guelev
我们提出了一个评估和生成访问控制策略的框架。该框架包含一个建模的形式主义称为RW，这是由模型检查工具支持。RW是为访问控制策略建模和验证其属性而设计的。RW语言非常有表现力，允许我们对复杂的访问条件进行建模，这些条件可能取决于数据值、其他权限和代理角色。
一个属性表达了一个代理联盟实现一个目标的能力，其中可能包括阅读和读取某些信息。给定基于策略和属性构建的模型，模型检查算法决定由属性定义的目标是否可由策略提供的权限内的联盟实现。在目标可实现的情况下，算法输出可由联盟使用以实现目标的策略。
合法目标的不可验证性可能表明策略没有为用户提供足够的权限来执行其操作。恶意目标的可验证性可能会揭示策略中的某些安全漏洞。当恶意目标是可实现的，由此产生的策略有助于提供线索，修改政策。该工具实现了算法，从而执行RW模型检查。它还可以将用RW语言编写的策略转换为XACML格式的策略文件。然后可以在转换后的策略文件上构建访问控制系统。
We present a framework for evaluating and generating access control policies. The framework contains a modelling formalism called RW, which is supported by a model checking tool. RW is designed for modelling access control policies, and verifying their properties. The RW language is very expressive, allowing us to model complex access conditions which can depend on data values, other permissions, and agent roles.
A property expresses the capability of a coalition of agents to achieve a goal, which may include reading and overwriting certain information. Given a model built based on a policy and a property, the model-checking algorithm decides whether the goal defined by the property is achievable by the coalition within the permissions the policy provides. In the case that the goal is achievable, the algorithm outputs strategies which may be used by the coalition to achieve the goal.
The unachievability of legitimate goals may suggest that the policy does not provide the users enough permissions to carry out their actions. The achievability of malicious goals may reveal certain security holes in the policy. When malicious goals are achievable, the resulting strategies help to provide clues on amending the policy. The tool implements the algorithm and thus performs the RW model-checking. It can also convert a policy written in the RW language into a policy file in XACML. An access control system can then be built on the converted policy file.