访问控制策略和自动验证技术对计算机科学的影响

理论计算机科学电子笔记185（2007）107-120www.elsevier.com/locate/entcs访问控制策略E. Kleiner1牛津大学计算实验室Oxford，OX1 3QD，UKT. 纽科姆2牛津大学计算实验室Oxford，OX1 3QD，UK摘要访问控制系统根据特定的策略管理用户访问资源的权限。此策略中的规则可能以通过人工检查不明显的方式进行交互;因此，需要自动验证技术，可以检查策略是否确实实现了某些所需的安全要求。30年前，访问控制的形式化提出了一个模型和一个安全规范，其中满意度是不可判定的。随后的研究，旨在找到限制版本，获得这个问题的可判定性，产生的模型没有令人满意的表达能力的实际系统。我们没有限制模型，而是重新检查安全规范。我们开发了一个新的逻辑，可以表达各种各样的安全属性的访问控制系统，并表明模型检查是可判定的一个有用的片段，这个逻辑。保留字：访问控制，模型检测，时态逻辑，CSP。1引言动机 访 问 控制系统是一种管理一组用户访问（例如读取或写入）某些资源（例如机密文件）的权限的机制。这是根据访问控制策略完成的，访问控制策略是一组规则，指示在哪些情况下特定用户可以获得对特定资源的特定权限。这些策略可以是大型的和动态的，例如，它们可以在每次创建或删除用户或资源时更新。由于这些原因，通常1电子邮件：eldar. comlab.ox.ac.uk2电子邮件：tom. comlab.ox.ac.uk1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2007.05.032108E. Kleiner，T.Newcomb/Electronic Notes in Theoretical Computer Science 185（2007）107不清楚策略在任何给定时间允许哪些行为，以及策略是否实际上实现了某些所需的安全规范。例如，系统管理员希望确保策略规则不会以任何方式交互，从而允许不受限制的用户访问受限资源。因此，需要自动化工具来帮助管理员评估访问控制策略对其系统安全性的影响问题所在在Harrison，Ruzzo和Ullman的开创性论文中，提出了一种正式的访问控制模型，称为HRU。HRU系统的状态由一组对象表示，其中一些对象是主体，并且保护矩阵给出主体和对象对之间的当前访问权限。策略是一组命令，每个命令都由对象参数化，并指定访问矩阵上的某些可能的转换。他们的语言能够自然地表达现实世界的访问控制系统（例如UNIX）的行为。他们考虑了以下安全问题：给定一组策略规则，一个通用访问权限a和一个初始矩阵，是否有可能达到一个状态，其中a被授予任何主体。然后，他们证明了这个问题是不可判定的使用编码的图灵机磁带到矩阵。尝试的解决方案。从那时起，研究集中在寻找受限制的模型，对于这些模型，这个问题是可以以最小的表达能力减少来判定的例如，坚持每个命令都是单操作的[7]（只能执行一个动作，例如，它可以创建一个对象，或授予访问权限，但不能在同一个原子步骤中完成这两个动作）或单条件[6]（每个命令的启用条件是访问矩阵的单个单元格在[18]中，Sandhu和Suri引入了非单调变换模型，该模型包含在[13]的允许创建对象但禁止创建新主体的条件中。Koch等人 [9]分析了他们基于图的访问控制框架的类似限制。我们的观察。虽然所有这些模型都获得了HRU安全问题的可判定性，但不幸的是，它们都不足以完全表达许多实际系统。这是因为它们通过限制可以考虑的政策类型。我们重新审视了[7]中的原始问题。不可判定性的一个来源是安全问题是访问控制策略加上初始矩阵的属性。它提出的问题总是以“从给定的初始状态，它是否可能”开始。. .“我们认为，在评估政策的安全性时，初始状态并不那么重要。管理员对访问控制系统更常见的问题是和换句话说，他们倾向于含蓄地假设系统已经启动并运行。此外，回答这些问题可以被视为回答整个初始状态范围内例如，如果我们证明任何用户E. Kleiner，T.Newcomb/Electronic Notes in Theoretical Computer Science 185（2007）107109没有权限A就不能获得权限B，并且如果我们知道我们的访问控制系统的初始状态不具有授予任何用户的权限A，则我们知道系统不允许用户获得权限B。本文提 出 了一种类似于HRU的访问控制保护矩阵模型。策略规则表示为参数化命令，如果某些特定权限满足某些前提条件，则这些命令可以创建/销毁对象，授予/获取权限。然后，我们引入了一个一阶线性时序逻辑，该逻辑在访问控制系统的有限次运行上进行解释。该逻辑可以量化所有当前存在的对象，并拥有时态运算符“总是”。原子命题可以对量化变量的特定权限状态或变量之间的相等关系进行断言我们称之为逻辑安全访问时态逻辑（SATL），因为它可以表示各种安全属性超过门禁系统整个逻辑的模型检查问题是不可判定的，因为它可以表达HRU安全问题[7]。然而，我们表明，这个问题是可判定的一个片段的逻辑，我们称之为通用SATL。在这个片段中的公式只有quantifiers，它们只能出现在最外层。我们有一个用于证明可判定性的有限抽象模型的原型实现。它是用CSP [15]编写的，用于模型检查器FDR [4]。最后给出了一个例子来说明该方法的有效性捐款. 我们描述了一个访问控制模型，它比[7]中给出的模型更有表现力，因为我们允许测试权限的缺失，但在技术上更简单，因为我们将原子命令序列分组为单个操作。我们引入了一个时间逻辑，能够表达广泛的安全性这些模型的属性。整个逻辑的模型检查问题是不可判定的，但我们相信这提供了一个框架，调查什么样的有用的安全问题，可以决定访问控制策略。本文是这一研究的一个重要开端。我们提出了这种逻辑的一个片段，它能够提出关于访问控制策略的实际问题， 我们表明，存在一个算法的模型检查问题在这个片段，并建立了一个概念验证的实现。如上所述，该结果还提供了检查某些初始状态集合的HRU安全问题的程序。这可以变成一个不完整的（但健全的）程序，用于检查原始HRU安全问题（即，对于单个指定的初始状态），方法是试图找到一组初始状态，其中包含在通用SATL中可表达的指定状态，并且检查成功。组织。在第2节中，我们提出了访问控制的形式化模型。在第三节中，我们介绍了我们的时序逻辑SATL，并证明了不可判定性110E. Kleiner，T.Newcomb/Electronic Notes in Theoretical Computer Science 185（2007）107整个逻辑的模型检测问题。 这个问题被证明是可判定的片段通用SATL在第4节。在第5节中，我们简要描述了我们的实现。结论、相关工作和未来工作见第6节。2一种访问控制我们假设对象的无限域和访问权限的有限集合A。一个状态是一个对（O，M），其中O是A的有限子集，表示当前存在的对象的集合，M是O×O×A的子集，表示当前授予的权限。例如，权限（Frank，passwd，x）表示对象Frank是否具有对象passwd的访问权限x，并且可以对名为Frank的用户是否能够执行更改其密码的程序进行访问控制 策略P 是一组有限的命令， 其中 命令c（x1，.，xn）是有限集合的6元组：（con，co take，ccreate，cgrant，ctake，cdestroy）直观地说，前两个组件表示命令的先决条件（必须为on和o的权限），最后四个组件表示命令的原子操作（要创建的对象，授予和获取的权限以及要销毁的对象）。更正式地说，con、co n、cgrant、ctake中的每一个都是F×F×A的子集，ccreate、cdestroy是F的子集。这里，F是形式参数{x1，.，xn}，即表示通过其参数化命令的对象的符号。命令的实例命令，并使用与命令不同的3对象我们现在正式指定由访问控制策略P在状态上引起的转移关系如下。（O，M）→（OJ，MJ）i如果策略中存在命令的某个实例c，则以下所有条件都成立：(i) 该命令适用于：• c上的c上的o上的o上的O×O×A。（条件权限属于当前状态的范围。）• ccreate{}.（要创建的对象不存在。）• cgrantctakeOJJ×OJJ×A，其中OJJ=Occreate。（在应用ccreate之后，存在要更改的• c摧毁jj.（要销毁的对象在应用ccreate(ii) 守卫的命令得到满足：• c关于反洗钱。• coM={}.（3）“独特”的限制并不意味着精确的表现力。如果一个人想允许在一个命令中提到的两个参数可以表示同一个对象，那么可以添加一个类似的命令，在其中标识两个形参名称。E. Kleiner，T.Newcomb/Electronic Notes in Theoretical Computer Science 185（2007）107111(iii) 满足下一个状态谓词：• OJ=（Occreate）\cdestroy.• MJ=（（M<$cgrant）\ctake）<$（OJ×OJ×A）.注意，默认情况下，新创建的对象没有与之关联的权限，但该命令可以在cgrant中指定要授予对象的权限。还注意到，我们在迁移系统中不包括任何初始状态。我们认为，一个策略实际上有许多可能的初始状态，我们允许策略设计者在我们的逻辑中指定关于初始状态的约束或假设。我们对HRU访问控制的形式化在某种程度上简化了我们的模型。我们不区分主语和宾语：通过给予应被视为主语的宾语o一个许可（o，o，主语），我们可以产生同样的表达能力。我们还将构成HRU中原子命令的所有顺序原语操作收集在一起最后，由于它不会产生额外的技术开销，我们还允许通过权限启用命令既可以是O也可以是On。例2.1我们复制[22]中给出的一个例子，叫做雇员信息系统。它的特点是一家公司的员工，其中一些是经理和/或董事，并可能奖励奖金给其他员工。我们将使用访问权限管理器，主任，和奖金.对奥里创建格兰特采取摧毁c1（x，y）（x，x，主任）（x，y，Bonus）c2（x，y）JJ（x，y，Bonus）c3（x，y）（x，x，经理）（y，y，经理）（y，y，主任）（x，y，Bonus）c4（x，y）JJJJ（x，y，Bonus）c5（x，y）（x，x，主任）（y，y，经理）（y，y，经理）c6（x，y）（x，x，主任）（y，y，经理）（y，y，经理）c7（x，y）（x，x，经理）yc8（x，y）（x，x，经理）（y，y，经理）（y，y，主任）yFig. 1.员工信息系统。公司的政策规定董事可以发放奖金。这在图1中由命令c1（x，y）表示，其中主管x发出信号，表示他命令c2（x，y）显示董事也可以删除他们授予的奖金。类似地，c3（x，y）和c4（x，y）规定，经理可以向任何非经理或董事的员工发放或收取奖金命令c5（x，y）和c6（x，y）表示主管可以从经理降级或晋升为经理。112E. Kleiner，T.Newcomb/Electronic Notes in Theoretical Computer Science 185（2007）107[22]中的原始示例包括员工x指定另一名员工y作为他的辩护人的能力。为了简单起见，我们省略了这一点，但很容易E. Kleiner，T.Newcomb/Electronic Notes in Theoretical Computer Science 185（2007）107113π |= o = oJi o=oJπ |=（o，oJ，a）i <$（o，oJ，a）∈M1π |=<$φi <$notπ| = φπ |= φi π| = φ或π|=π|=<$x.φi <$存在某个o∈O1使得πTo| = φ [o/x] π |=<$x.φi <$对于所有的o∈O1，我们有πTo| = φ [o/x]π|= Q φi 对于所有i = 1，.，n我们有πi|= φ图二. 满意通过设置权限（x，y，Advocate）来建模。在[22]中不允许但在我们的框架中允许的一个特性是允许现有对象集增长和收缩的能力。命令c7（x，y）和c8（x，y）表示管理者可以雇佣和解雇员工。3安全访问时序逻辑安全访问时序逻辑（SATL）的公式是：φ：：= x =y|Xy|（x，y，a）|¬φ |φ ∨ φ |φ ∧ φ |φ ⇒ φ |x.φ |x.φ |Q φ其中x，y是从某个变量集合中提取的，a是访问权限。为了节省我们探索情况的时间，我们考虑x/=y是<$（x=y），φ是<$（<$φ<$），φ是<$φ。我们有时会提到其中变量已经用实际对象名实例化的公式，即公式可能有形式为o=oJ或（o，oJ，a）的原子命题，其中o，oJ∈n。当没有量化器并且所有变量都用对象名实例化时，我们称之为命题公式。请记住，这些不是SATL中的公式对于有限个非空状态序列π =（O1，M1），. ，（On，Mn），我们称π是P的一条路，如果（O1，M1）→ ··· →（On，Mn）.我们写πi（其中i∈ {1，.，n}），即πi=（Oi，Mi），.，（On，Mn）.我们将πTo（其中o∈O1）写为π的最长前缀（可能是所有π），其中对于前缀中的每个状态（Oj，Mj）都有o∈Oj状态序列π和公式之间的满足在图中定义二、符号φ[o/x]表示一个公式φ，其中x的所有自由占位符都被o取代。 这样，当满意度应用于封闭公式时，所有变量在被求值时都已经被实际对象替代，因此满意度在原子命题中找到对象名o，oJ，而不是变量。请注意，量化器的范围仅限于当前存在的对象，其时间范围限于所选对象的生存期。这是必要的，以防止逻辑能够测试不存在的对象的属性114E. Kleiner，T.Newcomb/Electronic Notes in Theoretical Computer Science 185（2007）107但是产生了这种逻辑的一个怪癖：量化器不分布在时间运算符上，例如在一般情况下，时间运算符。Q φ/Q x..我们说公式φ满足策略P，记为P| = φ，当每条路径 P满足φ。SATL的模型检验问题如下：给定来自逻辑的任何公式φ和任何策略P，P是否|= φ？我们还需要符号PTC| = φ，这意味着P的所有路径，使集合C中的所有对象连续存在，都满足φ。整个SATL的模型检测问题是不可判定的。这是因为我们能够将[7]中所示的HRU安全问题表示为图灵机的停机问题。HRU的安全问题是：假设一个固定的初始状态，最终是否可以授予一定的访问权限。我们使用SATL公式来表示这样的问题1，.，xn. （（x1，...，xn）<$（y.y = x1<$··y = xn）你好，我是1000，2000。<$（y1，y2，a））。在这里，X1表示初始状态中x i变量之间的权限的确切状态，而（X2y. . ）子句表示最初没有其他对象。Q子句断言在两个对象之间不应授予权限a。4通用SATL我们将通用SATL定义为SATL的片段，它只包含可能只发生在最外层的量化器，即。形式的公式1，. 其中φ是无量化因子的。在看了一个例子之后，我们将证明我们的框架的一些命题，最终目标是证明通用SATL的模型检查问题是可判定的。例4.1在[22]中考虑的经理合谋情景问题是：“两个经理是否可以合谋，其中一个给另一个奖金？”我们可以用下面的公式来表示这种情况在通用SATL中是不可能的：1996年，（（x，x，Manager）（y，y，Manager）<$（x，y，Bonus）<$（y，x，Bonus）<$Q <$（（x，y，Bonus）<$（y，x，Bonus）.我们的访问控制系统的语义表现出数据独立性[20]（或参数多态性）相对于对象的“类型”。 这是因为我们在这个类型上假设的唯一操作是相等性测试。这导致了对象的对称性，这意味着过渡系统的双相似性命题4.2对于所有的态（O，M）和（OJ，MJ）以及所有的双射σ，我们有（O，M）→（OJ，MJ）i <$σ（O，M）→σ（OJ，MJ）其中σ以显而易见的方式提升到态E. Kleiner，T.Newcomb/Electronic Notes in Theoretical Computer Science 185（2007）107115证据 从定义上看，Q我们现在减少问题，涉及一个通用的SATL公式的一组问题，涉及命题SATL公式。这使我们从此可以把注意力限制在一个命题公式上，这个命题公式涉及来自有限集合C的对象常数，以及对象C连续存在的系统的路径。命题4.3模型检验问题P|= 1x1，. φ等价于有限个形式为PTC的模型检验问题的合取|=，其中是一个命题公式，只涉及有限集合C中的对象。证据取任何n个不同的对象C={o1，.，n}。 我们证明，考虑在这个有限集上的范围内的量子化是足够的，从而将一阶问题减少到命题问题的有限集。我们可以暂时发明记谱与书写P|= 1x1，. ，xn.φiP|=1：C，.，xn：C.证明前进方向是微不足道的。 向后的方向可以证明为如下 取P的任意路径π和任意对象oJ，.，oJ作为x 1的实例，.，xn.1N由命题4.2我们知道，对于每一个双射σ，σπ也是P的一条路，所以我们找到这样一个σ，它映射每个oJ转化为C. 假设右手边，σoJ，.，σoJi知道σπ| = φ [1oJ，.，oJn/x1，...，xn]。对φ应用结构归纳法，π |= φ [1n/x1，...，xn]。最后，请注意，P|=1：C，.，xn：C.φ等价于PTC|= 1×1：C，...，xn：C.φ，因为C. φ只检查其实例对象连续存在的路径。Q为了检验系统上的命题公式，我们采用了一个抽象的转换系统，其中抽象状态只记录对象C的有限集合之间的关系;因此，抽象状态是C×C×A的子集，并且表示包含C中对象之间的确切关系的任何具体状态。准确地说，我们使用一个抽象函数，它接受一个状态（O，M），O=C，并将其映射到α（O，M）= M<$（C × C × A）.注意，这个映射不是完全的--不存在所有对象C的状态没有抽象。我们需要在抽象系统中引入转换的概念。通常的要求是，当存在某种相应的具体转换时，抽象转换恰好存在。作为一种定义，这是不可取的，因为它不是直接可计算的：每个抽象状态代表无限数量的具体状态，我们不能检查它们。相反，我们使用以下观察。因为我们的抽象状态不记录关于C之外的对象的信息，并且因为我们的系统是关于对象的数据独立，所以我们可以认为C之外的所有对象都是同构的。此外，每个命令仅检查和/或更改一个有限元素116E. Kleiner，T.Newcomb/Electronic Notes in Theoretical Computer Science 185（2007）107物体的数量。以类似于[14]的方式，这允许我们将无限对象集“折叠”为有限对象集，其大小取决于任何单个过渡可能需要的此类对象的最大数量。这个想法建议我们计算抽象状态空间上的转换，计算“简化”状态空间（C <$C j）×（C <$C j）× A上的具体转移这里，CJ是大小为m的C\C的子集，其中m是任何一个命令中形式对象参数的最大数量（即，可以“涉及”的最多对象在任何一个过渡中）。为了使其更正式，我们定义了从抽象状态到具体状态的翻译：γ（Q）={（O，M）|OC，O CCJ，MO×O×A，M∈（C × C × A）= Q}。我们定义一个跃迁→存在于两个抽象态Q和QJ之间，恰好当存在从γ（Q）中的任何态到γ（QJ）中的任何态的某种具体跃迁时。这是可计算的，因为它只处理有限结构。这使得我们可以讨论抽象迹Q1→ ··· →Qn。为了联系抽象和具体的系统，我们说每条路径（O1，M1）→···→ P T C的（On，Mn）（即，对于所有i = 1，.，n）蕴含一个具体迹α（O1，M1）→ ··· →α（On，Mn）.我们将证明这两个系统具有等价的迹线。4命题4.4所有具体痕迹都是抽象痕迹证据 我们通过证明（O1，M1）来 → （O2，M2）蕴含α（O1，M1）→α（O2，M2），其结果由归纳法得出.假设生成转换（O1，M1）→（O2，M2）的命令c是用对象CD实例化的，其中D是与C.设σ是从C<$D到C<$Cj的任何保持C的内射。 我们知道这样的注射存在，|D| ≤m =|CJ|.我们将此注入提升到以下状态：σ（0，M）=（{σ（0）|o∈O和o ∈ dom σ}，{（σ（o1），σ（o2），a）|（o1，o2，a）∈ M且o1，o2∈ domσ}）。现在可以得出σ（O1，M1）→σ（O2，M2）使用相同的命令c，除了我们用对象C<$CJ而不是C<$D实例化。这可以从→的定义中通过详细的案例来看出还可以通过更非正式的观察看到，σ只删除命令实例未检查/更新的对象，并统一重命名其他对象。当i= 1，2时，我们也有σ（Oi，Mi）∈γ（α（Oi，Mi））.Q4它们不是双相似的，是过渡系统之间更强的等价性。 例如，一个抽象系统可能有一个无限长的行为，它破坏了无限多的对象;这在任何具体系统中都不会发生。E. Kleiner，T.Newcomb/Electronic Notes in Theoretical Computer Science 185（2007）107117我我我命题4.5所有抽象的痕迹都是具体的 痕迹。证据现在让我们假设我们有一个抽象的转换序列Q1 →..→Qn. 我们知道每一个过渡的存在是因为有一个具体的过渡从某个状态Si∈γ（Qi）到某个状态SJ∈γ（Qi+1）. 我们称之为命令创建此转换ci（CCJ）的实例，以强调它仅使用来自CCJ的对象实例化。我们的目的是证明存在一个具体的迹（O1，M1）→ ··· →（On，Mn），其中对每个i，（Oi，Mi）∈γ（Qi）.与前面的构造相反，我们将CJ中的对象映射回整个Cj中，并且我们希望以这样一种方式实现这一点，即每个新命令实例使用的对象不会与任何其他新命令所使用的对象重叠因此，我们需要对每个命令ci（CCJ）进行不同的注入σi：CJ→C\C（O1，M1）c1（C<$σ1CJ）−→（O2，M2）···cn−1（C<$σn−1C J）−→（On，Mn）.我们需要在跟踪中设置每个状态（Oi，Mi），以使它捕获每个尚未执行的命令ci（CσiCJ）所期望的对象σi（Cj）上的初始条件（我们从状态Si获得这些值）和每个已执行的命令所期望的对象σi（CJ）上的最终条件（我们从状态SJ获得这些值）。这是可以做到的，因为注入σi不重叠，所以建议的状态是：（Oi，Mi）=Qi<$σ1SJ<$$>··<$σi−1SJ<$σiSi<$··<$σn−1Sn−1。1i−1上面，每个注入σj应用于C外部的对象和不仅仅是C之间的权限，因此σjS返回结构5（O，M），O={}，M（C×C×A）={}，以及M<$（C <$σCJ）×（C <$σCJ）× A.操作符将这些结构（使用union）组合起来形成一个状态，使用Qi填充C×C×A部分。读者可能会注意到，在最后的迹线中，矩阵的某些部分总是空白的（例如，σ1CJ×σ2CJ×A）-它们并不直接对应 可以从状态Si和SJ中提取的任何信息。虽然对于这些权限可以具有什么值有一定的自由度，最安全的做法是将所有这些权限都设置为0。这是因为如果这些o∈σiCJ对象中的一个被破坏，我们需要（o，oJ，a）和（oJ，o，a）在所有对象oJ的后续状态中都是o ∈ σ i。相反，如果创建了一个，我们需要这些权限在以前的状态下是无效的。（这与下面讨论的C5 我们不能称这些状态为M = O × O × A，因为我们不一定有M=O×O×A。118E. Kleiner，T.Newcomb/Electronic Notes in Theoretical Computer Science 185（2007）107我从α（Oi，Mi）=Qi的定义中可以很容易地看出。还有待证明的是：Qi<$σ1SJ<$$>···<$σiSJ<$σiSi <$σ iSi+1<$···<$σn−1Sn−11i−1ci（C<$σiC J）Q<$σ SJ<$···<$σ SJ−→J···中国+1 11我 i−1<$σiSi<$σiSi+1n−1n−1由于下划线的项，这可以通过检查→的定义中的情况从Si→SJ推导出来。请注意，o∈C永远不会出现在销毁字段中因为结果状态没有抽象。这一点很重要，因为否则我们将要求该对象的行和列中的所有权限在后续状态中都是不可用的，而我们对（Oi+1，Mi+1）的定义不能否则，证明是直截了当的。Q我们现在要证明抽象系统和具体系统之间的迹等价性意味着检查抽象系统将得到与检查具体系统相同的结果。首先要注意的是，满意度可以应用于迹线和路径。命题4.6抽象系统和具体系统不能用任何只提到C中对象的命题公式φ来区分。证据观察到，在具体状态上检验φ中使用的原子命题返回的真值与在代表性抽象状态上检验它返回的真值相同。这意味着在路径上检查φ返回与在相关轨迹上检查φ相同的真值这个结果是由抽象系统和具体系统的迹等价得出的（命题4.4和4.5）。Q定理4.7通用SATL的模型检验是可判定的，即存在一个过程，给定一个访问控制策略P和一个封闭的通用SATL公式φ，回答P是否|= φ。证据命题4.3意味着我们可以考虑模型检查问题PTC| = φ对于一个命题公式φ只提到有限集合中的对象C.通过命题4.6，我们可以使用线性时态逻辑的传统模型检测算法来检查有限可计算抽象系统[19]，以推断具体系统PTC上φ的真实性。Q5自动化我们可以在进程代数CSP [15]中对定理4.7CSP事件表示由来自CCJ的对象实例化的命令。我们将（C<$CJ）×（C<$CJ）×A中的每个许可建模为一个单独的过程，如果事件满足相关命令的前提条件，并在适当时改变状态。表示C×C×A之外的权限的进程不保留状态，而是根据γ保持永久的不确定状态。 然后，使用CSP并行E. Kleiner，T.Newcomb/Electronic Notes in Theoretical Computer Science 185（2007）10711911操作符，而细化检查器FDR [4]可以用来探索哪些状态是可达的。更多细节见[8]。例5.1我们完成了雇员信息系统的运行示例。我们设置C={ox，oy}来表示规范中提到的两个管理器公式，并且CJ={oJ，oJ}，因为参数的最大数量1 2在任何一个命令是两个。抽象在CSP中编码，并使用细化检查器FDR进行检查。它给出了一个反例<$c6（oJ，ox），c3（oy，ox）<$c。我们把这解释为某个导演oJ降级ox;然后oy可以给对ox的奖励。从系统中删除c6会使我们检查成功。使用我们的定理，这证明了以下关于雇员信息系统：不管雇员的数量，如果董事不能降级经理，那么两个经理就不可能合谋，让其中一个奖励另一个奖金。6结论摘要我们已经介绍了一个一阶时序逻辑的访问控制的保护矩阵模型虽然整个逻辑的模型检查问题是不可判定的，但我们已经确定了一个有用的逻辑片段，问题是可以决定的。这使我们能够检查此类系统的实际需求，而不必限制策略语言。我们描述了如何HRU安全问题可以减少到我们的决策问题在某些情况下。我们还建立了一个原型实现的模型检查过程。Guelev，Ryan和Schobbens [5]提出了基于命题逻辑的RW形式主义，用于表达访问控制策略和查询。本文还提出了一种用Prolog语言实现的计算能力的固定数量的代理人在固定数量的资源存在下实现特定目标。此外，还提供了一个工具，它将RW脚本作为输入，并将策略描述转换为XACML [21]。泛SATL可以与只使用存在量化的RW公式相比较。另一个相关的工作是[2]，其中显示了如何在CSP中表达具有有限数量的主题和资源的访问控制机制。我们使用的CSP模型在某种程度上是相似的。这两个作品的原因只对有界系统。因此，它们只能用于寻找电锯，不能提供一般的安全证明。我们的结果表明，只有存在量化的RW公式可以检查无界系统。在实践中，如果不假设系统永远不会进入某种不一致的状态，通常不可能证明我们所考虑的安全需求。在这种情况下，人们希望“加强”检查通过指定，例如，通用SATL无法表达这些120E. Kleiner，T.Newcomb/Electronic Notes in Theoretical Computer Science 185（2007）107不变量，但我们目前正在准备关于SATL包含公式的较大片段的可判定性结果，如1，.，xn. （（φINV）Q（φINV）），其中INV通过限制使用量化器来表达系统的期望全局不变量。本文中提出的结果是可能的，这要归功于该模型与对象类型无关的事实。这一观察使我们能够使用为具有数组的数据独立系统开发的技术[10，14]，并将其应用于访问控制矩阵。我们相信，还有其他关于阵列系统的结果可以用于分析访问控制策略，特别是关于重置阵列的结果[16，11]。手动编写CSP脚本来分析访问控制策略可能是繁琐且容易出错的。因此，我们打算开发一个编译器，将产生CSP脚本从一个更抽象的描述。我们还对基于角色的访问控制（RBAC）感兴趣，它是图灵完备的[3].我们相信，我们的可判定性结果可以扩展到模型中的一些RBAC策略，系统是有限的，以固定数量的角色，但不受限制，否则。最后，我们希望我们的结果可以为信任管理系统的验证提供更多的启示[1]。我们在这里提出的结果，以及在安全协议领域[17]中获得的知识，可以结合起来，以便对此类系统进行推理，并希望加强现有的可判定性结果[12]。引用[1] 布拉兹，M.，J. Feigenbaum和J. Lacy，分散式信任管理，在：IEEE安全和隐私，1996年，pp. 1081-6011.[2] Bryans，J.，Reasoning about XACML policies using CSP，Technical Report CS-TR-924，University ofNewcastle（2005）.[3] Crampton，J.，“授权和反链”，博士论文，伯克贝克，伦敦大学，伦敦，英国（2002年）。[4] Formal Systems（Europe）Ltd，网址http://www.fsel.com[5] Guelev，D.，M. 瑞安和P。-Y. Schobben s ，模型检查访问控制策略。，in：ISC，2004，pp.219-230.[6] Harrison，M.和W.鲁佐，单调保护系统，在：A。J. R.DeMillo，D.多布金和R. Lipton，编辑，安全计算的基础，学术出版社，1978年，pp。337-363[7] 哈里森，M.，W. Ruzzo和J. Ullman，操作系统中的保护，ACM通信（1976）。[8] Kleiner ， E. 和 T.Newcomb ， Using CSP to decide safety problems for access control policies ，Technical Report RR-06-04 ， Oxford University Computing Laboratory ， Parks Road ， Oxford ，OX1 3QD，UK（2006）。[9] Koch ， M. ， L. Mancini 和 F. Parisi-Presicce ， 基 于 图 的 访 问 控 制 模 型 的 安 全 性 的 可 判 定 性 ， 在 ：ESORICS229-243E. Kleiner，T.Newcomb/Electronic Notes in Theoretical Computer Science 185（2007）107121[10] 拉 兹 奇 河 ，T.新 公 司 和 A 公 司 。Roscoe ， Onmodelchecheckingdata-independentsystemswithitharayswithitoutreset ， Theory and Practice of Logic Programming ： SpecialIssue on VerificationandComputational Logic 4（2004）.[11]拉 兹 奇 河 ，T.新 公 司 和 A 公 司 。Roscoe ， Polymorphicic ics ystem with it harrays ， 2-countermachinesandmultiset rewriting，in：Proceedings of INFINITY，2004，pp. 3-19[12] Li ， N. ， J. Mitchell 和 W. Winsborough ， Beyond Proof-of-Compliance ： Security Analysis in TrustManagement，J. ACM52（2005），pp. 474-514.[13] 利普顿河，巴西-地和L.Snyder，On Synchronization and Security，in：A.J. R.DeMillo，D.多布金和R. Lipton，编辑，安全计算的基础，学术出版社，1978年，pp。367-385[14] Newcomb，T.“Model Checking Data-Independent Systems With Arrays”，Ph.D. 牛津大学计算机实验室（2003）。[15] Roscoe，A.，“The Theory and Practice of Concurrency,” Prentice-Hall,[16] R os coe，A. 和河。 Lazi 'c，你怎么能让我看到你的眼睛呢？第二届验证与计算逻辑国际研讨会（VCL2001）的论文集，技术报告DSSE-TR-2001-3，第5-23页（2001），第10 - 12页。5-23[17] 瑞安，P.，S.施耐德，M。Goldsmith，G. Lowe和A. Roscoe，安全协议（2001）。[18] 桑德胡河，巴西-地和G. Suri，访问权限的非单调变换，在：IEEE安全与隐私研讨会论文集，1992年，pp.148比163[19] Vardi，M. Wolper，An automata-theoretic approach to automatic program veri fication（preliminaryreport），in：Proc. 1st Annual IEEE Symposium on Logic in Computer Science，Washington，DC，1986，pp. 332-344。[20] Wolper，P.和V. Lovinfosse，具有网络不变量的大型过程集的可验证性，在：有限状态系统的自动验证方法，计算机科学讲义407（1989），pp. 68比80[21] Zhang，N.，M. Ryan和D. Guelev，在XACML中综合验证访问控制系统，在：FMSE56-65.[22] Zhang，N.，M. Ryan和D. Guelev，通过模型检查评估访问控制策略。，in：ISC，2005，pp. 446-460