History-Based Access Control with Local Policies
History-Based Access Control with Local Policies
复制标题
具有本地策略的基于历史的访问控制
DOI：
--
复制
发表时间：
2005
期刊：
影响因子：
--
通讯作者：
G. Ferrari
中科院分区：
文献类型：
--
作者：
Massimo Bartoletti;P. Degano;G. Ferrari
提出了λ演算的一种扩展，用于研究基于历史的访问控制。它允许具有可能嵌套的局部作用域的安全策略。我们定义了一个类型和效应系统，对于给定的程序，该系统提取一个历史表达式，即对运行时可获得的历史集合的一种正确近似。历史表达式的有效性是非正则的，因为策略的作用域可以嵌套。然而，提出了一种历史表达式的转换，使得通过标准的模型检查技术进行验证成为可能。如果一个程序在编译时提取的历史表达式是有效的，那么它在运行时永远不会失败。
An extension of the λ-calculus is proposed, to study history-based access control. It allows for security policies with a possibly nested, local scope. We define a type and effect system that, given a program, extracts a history expression, i.e. a correct approximation to the set of histories obtainable at run-time. Validity of history expressions is non-regular, because the scope of policies can be nested. Nevertheless, a transformation of history expressions is presented, that makes verification possible through standard model checking techniques. A program will never fail at run-time if its history expression, extracted at compile-time, is valid.