安全管理员的访问分析框架

可在www.sciencedirect.com在线获取理论计算机科学电子笔记312（2015）89-105www.elsevier.com/locate/entcs一种基于应急管理的访问分析框架桑德拉阿尔维斯1部葡萄牙波尔图大学计算机科学系MaribelFern'andez2，3部伦敦大学国王摘要我们定义了一个访问控制策略分析框架，旨在简化安全管理员的指定和验证任务。我们考虑基于类别的访问控制模型中的策略，该模型已被证明是许多最知名的访问控制模型（例如，MAC地址，DAC、RBAC）。使用基于类别的策略的图形表示，我们展示了如何回答通常的管理员查询可以自动计算，可以检查访问控制策略的属性。 我们展示了在紧急情况下的应用程序，在那里我们的框架可以使用分析访问控制和应急管理之间的相互作用关键词：安全策略，访问控制，操作语义，重写，基于图的分析。1介绍访问控制系统用于保护资源免受未经授权的使用。在最基本的形式中，访问控制策略指定每个用户可以对每个资源执行的操作。一个资源和一个操作的组合称为权限。目前正在使用各种访问控制模型和访问控制策略规范语言最流行的一种是ANSI（分层）基于角色的访问控制（H-RBAC）模型[2]，其中用户被分配给角色，每个角色被分配一组权限（使用时间和位置约束的RBAC[19]）。更灵活的型号，如1电子邮件地址：sandra@dcc.fc.up.pt2电子邮件：maribel. kcl.ac.uk3部分由欧洲航空航天研究和发展组织（EOARD-AFOSR）资助。http://dx.doi.org/10.1016/j.entcs.2015.04.0061571-0661/© 2015作者。出版社：Elsevier B.V.这是CC BY许可下的开放获取文章（http://creativecommons.org/licenses/by/4.0/）。90S. 阿尔维斯湾Fernández/Electronic Notes in Theoretical Computer Science 312（2015）89基于事件的访问控制（DEBAC）模型[12]和动作状态访问控制模型[7]，指定了依赖于动态条件的权限，这些动态条件是根据系统中发生的事件在[5]中提出了一个访问控制的元模型，它可以专门用于特定领域的应用程序。它确定了访问控制的核心原则集，抽象了特定访问控制模型中的许多复杂性，以简化策略编写和策略分析的任务。元模型的一个关键方面是将注意力集中在类别的概念上。一个范畴是一类共享某些属性的实体。访问控制中使用的经典分组类型，如角色、安全许可、信任的离散度量等， 是更一般的范畴概念的特殊例子。 在基于类别的访问控制策略中，权限被分配给用户类别（我们称之为主体），而不是分配给单个用户。 类别可以定义为基于例如， 用户属性、地理约束、资源属性。例如，用户可以根据他们的年龄被分配到不同的类别，并且策略可以给予执行动作的许可（例如，下载）在资源上（例如，afilm），但不包括“儿童”类别。以这种方式，许可以动态和自主的方式改变（例如，当注册用户有生日时），不像，例如，基于角色的访问控制模型，需要安全管理员的干预鉴于访问控制策略定义的复杂性和范围，分析和推理访问控制策略的正式方法是必不可少的。这在处理紧急情况下的访问控制的系统中尤其重要，在这种情况下，用户的权利可能需要改变以应对特定的紧急情况。访问控制模型和策略的形式化规范（参见，例如，[16，30]）使用了定理证明器，专用逻辑，以及最近的功能和基于重写的方法（参见，例如，[29，12]）。在[14]中描述了基于类别的元模型的基于重写的操作语义使用标准的重写工具，可以验证基于重写的安全策略，以确保每个访问请求都有唯一的答案，如[15]所示。在本文中，我们定义了一个访问控制策略分析框架，旨在简化安全管理员的规范和验证任务。我们考虑基于类别的策略，因为基于类别的模型包含了最知名的访问控制模型[14]，从而使我们能够获得一个通用的框架。使用图形表示的政策，我们展示了如何回答通常的管理员查询可以自动计算，和属性的访问控制策略（如，每个访问请求接收一个唯一的答案）可以检查。我们展示了该框架在分布式环境中的政策分析中的应用，特别是包括紧急情况下权利管理的政策。例如，在医院环境中，访问控制策略可以指定每个医生可以访问他/她自己的患者的患者记录然而，如果病人p心脏骤停，那么病房里的任何医生S. 阿尔维斯湾Fernández/Electronic Notes in Theoretical Computer Science 312（2015）8991应该能接触到P我们将表明，这种政策可以很容易地在我们的框架中指定，在一个视觉和正式的方式，和属性，如事实上，该政策确保了不应允许用户在同一资源上执行两个冲突动作），可以使用基于图的算法和重写技术来容易地证明。文件概述论文的其余部分组织如下。 在第2节中，我们回顾了基于类别的访问控制模型。第3节讨论紧急政策。第4节介绍了一个基于图的框架来表示和分析基于类别的策略，第5节描述了它的实现（用于策略可视化和分析的Ruby应用程序）。在第6节中，我们讨论了相关的工作，并在第7节中，得出结论，并建议进一步的工作2分类：基于类别的元模型我们假设熟悉一阶逻辑和项重写系统的基本概念[3]。下面我们简要描述基于类别的访问控制元模型的关键概念;详细描述请参见[5]。非正式地，类别是实体可以被分配到的几个不同的类或组中的任何一个。实体在许多分类的话语域中由常数表示，包括：可数的类别集合C，表示为c0，c1，.。一个可数的主体集合P，记为p0，p1，. （我们假设请求访问资源的主体被预先认证）;命名动作的可数集合A，表示为a0，a1，. 资源标识符的可数集合R，表示为r0，r1，. ;访问请求的可能答案的有限集合（例如，{grant，deny，undetermined}）和一个可数的情境标识符集合S来表示环境信息。更一般地，实体由术语（例如， 委托人代表 通过数据结构主体（pi，attributeList）），但是常量对于本文中的大多数示例将是足够的。元模型包括以下关系：• 主范畴分配：PCA <$P × C，使得（p，c）∈ PCA i <$a principalp ∈ P被分配给范畴c ∈ C。• 权限类别分配：ARCA <$A×R×C，使得（a，r，c）∈ ARCA i，a ∈ A对资源r ∈R的操作可以由分配的主体执行到 范畴c ∈ C。• 授权：PARP ×A × R，使得（p，a，r）∈ PARi a principalp∈ P可以在资源r∈ R上执行动作a∈ A。定义2.1[公理]关系PAR满足下面的核心公理，其中我们假设范畴之间存在一个关系n;这可以简单地是相等，集合包含（分配给c∈ C的主体集合是分配给cJ∈ C的主体集合的子集），或者可以使用特定关系92S. 阿尔维斯湾Fernández/Electronic Notes in Theoretical Computer Science 312（2015）89∈（a1）np∈ P，na∈ A，nr∈ R，（a，r，cJ）∈ ARCA）惠（p，a，r）∈ PAR定义2.2[基于类别的策略]基于类别的策略是一个元组其中E=（P，C，A，R，S），使得公理（a1）得到满足。在操作上，公理（a1）可以通过一组函数来实现，如[14]所示。我们回想一下下面函数par（P，A，R）的定义;它依赖于函数pca和arca，前者返回分配给主体的类别列表，后者返回分配给类别的权限列表定义2.3定义2.1中公理（a1）的重写式的具体化由重写规则给出：（a2）par（P，A，R）→如果（A，R）∈arca（contain（pca（P）thengrantelsedeny正如函数名称所示，contain计算包含列表pca（P）中给定的任何类别的类别集。该函数是列表上的成员操作符，grant和deny是答案，arca将函数arca泛化为考虑类别列表：arca（nil）→nilarca（cons（C，L））→append（arca（C），arca（L））然后，主体p对资源r执行动作a的访问请求可以简单地通过将术语par（p，a，r）重写为范式来评估。公理（a1）及其代数版本（a2）指出，只有当p属于类别c时，主体p对资源r执行动作a的请求才被授权，使得对于低于c的某个类别（例如，c本身）行动a被授权r，否则拒绝请求。还有其他替代方案，例如，如果没有足够的信息来批准请求，则将不确定视为答案在[ 11 ]中提出了分布式基于类别的访问控制的公理化，以指定联邦策略，作为单个访问控制策略的组合获得。在联邦中，每个成员都有自己的访问控制策略，并有助于定义全局访问控制策略。我们将在下一节中使用分布式访问控制的概念来定义紧急策略。我们回顾下面的主要公理。假设情境标识符的集合S包括用于站点的标识符，即，s∈ S标识联邦的一个组成部分。PCAs、ARCAs和PARs表示由站点标识符索引的关系族直观地说，PAR表示在站点中有效的授权。定义全局授权策略的关系PAR通过组合由关系PAR定义的本地策略来获得，如下所示集合P、C、A、R分别包括系统的任何站点中的主体、类别、动作和资源，它们被假设为在联盟中是全局已知的（或者，我们可以为每个站点定义集合Ps、Cs、As、RsS. 阿尔维斯湾Fernández/Electronic Notes in Theoretical Computer Science 312（2015）8993定义2.4[分布式公理]分布式的基于范畴的元模型由以下核心公理定义（b1）n∈ P，n∈ A，n∈ R，n∈ S，（c，cJ∈ C，（p，c）∈ PCAs（a，r，cJ）∈ ARCAs）惠（p，a，r）∈PARs（f1）n∈ P，n∈ A，n∈ R，（p，a，r）∈ OPpar（{PARs|s∈S}）惠（p，a，r）∈PAR访问请求的结果可能因评估请求的站点而异公理（f1）描述了全局授权关系，它是通过使用运算符OPpar从每个站点定义的授权关系中获得的。虽然大多数现有的政策语言（例如，XACML）有一组固定的操作符来组合策略，元模型可以容纳大量的组合操作符。定义2.5A 分布式 基于类别 政策 是 已定义 通过 元组{PCAi}i∈S，{ARCAi}i∈S，{PARi}i∈S，OPpark，使得公理（b1）和（f1）满足.分布式模型的操作语义通过扩展定义2.3中提出的函数，使用分布式术语重写系统（DTRS），这是一种术语重写系统，其中规则被划分为模块，每个模块与一个唯一的标识符相关联，函数符号用这样的标识符进行注释（有关DTRS的更多细节，我们参考[12]）。换句话说，在特定站点中定义的特定函数由站点标识符索引;没有站点注释的函数被假定为在本地定义定义2.6在分布式环境中，Def.2.4由重写规则给出（ b2）pars （P ，A，R）→如果（A，R）∈arcars（包含（pcas （P）则grantelsedeny其中函数∈是列表上的成员关系运算符，grant和deny是答案，而r cas是定义类别特权分配的函数，如前一节所述。公理（f1）可以通过以下重写规则来实现，该规则通过使用pars来实现OPpar，其中函数fauth根据运算符op将结果组合成最终答案：（f 2）授权（p，a，r，s1，.， s n）→ fauth（op，pars1（p，a，r），.，parsn（p，a，r））。公理（f1）可以用几种方式实现。在上面的定义中选择的版本对应于一个非常通用的重写规则，该规则可以用于评估单个中心站点中的访问请求（如果n = 1并且运算符op 是身份），以及用于评估答案的组合（具有合适的94S. 阿尔维斯湾Fernández/Electronic Notes in Theoretical Computer Science 312（2015）89操作者OP）。可以使用诸如返回主体p注册的站点的psite（p）或返回资源r所在的站点的rsite（r）之类的函数通过这种方式，访问请求可以在预定义的中心站点进行评估，或者可以优先考虑本地评估，或者可以实现更详细的访问答案组合我们参考[13，10]的例子。3应急政策在本文中，我们考虑一种特殊的策略组合，其中访问控制策略与紧急策略相结合，该紧急策略指定各种紧急情况如何影响用户访问资源的权限。在这种方法中，事件是基本或复合动作[22]，我们使用事件（ei，p，a，o，t，l）形式的术语表示，遵循[14]。这里，event是一个数据构造函数，ei是一个事件标识符，p是与事件相关联的主体，a是一个动作，o是它的对象，t是事件发生的时间，l是一个参数列表（取决于事件类型，可能不需要某些参数）。 紧急政策将与特定事件相关。为了简化，我们只考虑原子事件，并假设系统中发生的所有事件的历史都是可用的（例如，通过日志）。我们遵循[18]中给出的紧急情况的定义如果事件E发生在比T早的时间Ts，并且导致紧急情况的启动，并且由于以下任一种结果，该紧急情况在T之前尚未结束，则紧急情况发生在时间T：（i）限幅，即， 在Ts和T之间的时间T J发生的事件E j，导致紧急情况终止，或（ii）该紧急情况的超时δ到期。例如，在医院环境中，访问控制策略可以指定每个医生可以访问他/她自己的患者的患者记录。然而，如果病人p发生了心脏骤停，那么病房里的任何医生都应该在心脏急症期间有权接触p分布式元模型和上面定义的事件概念可以用来指定紧急情况下的访问控制。我们考虑两个站点π1和π2，使得π1包含标准策略，π2包含紧急策略。在前面的例子中，让patient是一个由所有患者（给定医院）组成的类别，doctor是一个由所有医生（给定医院）组成的类别假设医生（X）是由患者X的所有医生组成的（参数化的）类别，使得对于所有X，医生（X）是医生，即，类别医生（X）从类别医生继承所有权限。假设关系PCA和ARCA满足以下公理，其中，如果已经检测到针对P发起心脏紧急情况的事件，并且没有记录结束紧急情况的事件，则emerg（bcrd，P）为真<$P，（P，patient）∈ PCA <$（read，record（P），doctor（P））∈ ARCAπ1P，（P，patient）∈PCAS. 阿尔维斯湾Fernández/Electronic Notes in Theoretical Computer Science 312（2015）8995在操作上，我们在标准（π1）和紧急（π2）站点中为arca指定重写规则，并使用具有优先级的联合操作符来组合策略arcaπ1（医生（P））→[（读取，记录（P））]arcaπ2（医生）→[（读取，记录（P））|P ∈ patientList_emerg（bcrd，P）]）其中patientList返回患者列表，即P，使得patient∈pca（P）。我们将在下面的章节中讨论证明此类策略的属性的技术以表明任何医生都可以访问心脏病急诊患者的记录4基于类别的策略4.1策略的图形表示我们首先定义如何通过图形来表示策略。数据结构和算法的图形或视觉表示与文本表示相比具有许多既定的显著优势。特别是，它们往往比相应的文本表示更容易理解和分析。此外，作为一个很好的研究领域，图论的算法和性质可以用来分析政策的性质定义4.1[策略图]我们定义一个策略图，或者简称为图，作为元组G=（V，E，lv，le），其中V是一组节点，E是一组无向边，这是一个子集的{{v1，v2} |v1，v2∈ V <$v1v2}，lv是一个内射标号函数将节点映射到基于类别的元模型中的实体lv：V →P <$C <$A <$R，le是边的标号函数。我们假设一个节点的度的通常概念，作为连接到该节点的边的数量定义4.2G中两个节点v0，vn之间的长度为n的路是一个序列v0，v1，. v n，使得{v i−1，v i} ∈ E，对所有1 ≤ i≤ n。由于我们有不同类型的节点，我们定义一个函数类型：V →{P，C，A，R}，它将每个节点与其标签的类型相更准确地说，如果lv（v）=p∈ P，则type（v）=P（即，P是表示主体的节点的类型），类似地，C是表示类别、A动作和R资源的节点的类型此外，我们考虑边的类型由该边所连接的节点的类型决定，即我们考虑函数类型：E→ {P，C，A，R} × {P，C，A，R}。一个边类型将是一个对（T1，T2），为了简单起见，我们将其表示为T1T2。例如，AC是连接类型A的节点与类型C的节点的边的类型。注意，由于我们的边是无向的，所以我们不区分类型T1T2和T2T1。我们将使用类型来限制表示策略的图的边，如下所示。96S. 阿尔维斯湾Fernández/Electronic Notes in Theoretical Computer Science 312（2015）89PC一R定义4.3[良好类型的策略图]如果策略图只包含以下类型的边，则(a) {v1，v2} ∈ E使得type（v1）=P <$type（v2）=C，它们将主体与范畴联系起来。这对应于PC类型的边缘。(b) {v1，v2} ∈ E使得type（v1）=Ctype（v2）=A，它们将范畴与动作联系起来。这对应于CA类型的边。(c) {v1，v2} ∈ E使得type（v1）=A，type（v2）=R，它们将动作连接到资源。这对应于AR类型的边。定义4.4[与G相关的关系]设G是一个良好类型的策略图，PC、CA和AR分别是PC、CA和AR类型的所有边的集合。然后我们定义与G相关的以下关系：• 关系PCA G由集合{（lv（v1），lv（v2））定义|type（v1）= P <${v1，v2} ∈PC}.它也可以定义为从类型P的节点开始的大小为1的路径的集合。• 关系ARCA G由集合{（lv（v1），lv（v2），lv（v3））给出|类型（v1）=A<${v1，v2} ∈AR<${v3，v2} ∈ CR}. 它也可以被定义为一组路径大小为2，从类型C的节点开始，在类型R的节点上结束（反之亦然）。• 关系PAR G由集合{（lv（v1），lv（v3），lv（v4））给出|Bagrav2s.t. {v1，v2}∈ PC <${v2，v3} ∈ CA <${v3，v4} ∈ AR}。它也可以定义为一组大小为3的路径，从P类型的节点开始，到R类型的节点结束（反之亦然）。命题4.5策略图中任何大小为3并且以类型R的节点结束，必须具有以下形状：证据对边类型施加限制的直接结果。 请注意，所有长度为1的路径从类型P的节点开始，到类型C的节点结束。 从类型C的节点开始的长度为1的路径终止于类型A的节点或节点并且从类型A的节点开始的长度为1的路径在节点A上结束C型节点或R型节点。因此，从类型P的节点开始并在类型R的节点结束的唯一大小为3的路径是遍历类型C的节点的路径和类型A的节点。Q因此，从所有从P型节点开始到R型节点结束的大小为3的路径，可以有效地计算PAR关系（目前我们不考虑类别之间的PAR关系）。此外，很容易看出，任何类型良好的策略图都表示访问控制策略。命题4.6每个类型良好的策略图G定义了一个唯一的基于类别的访问控制策略：PACE，PCA G，ARCA G，PAR G.证据 根据Def. 2.2，我们需要证明PCAG，ARCAG和PARGS. 阿尔维斯湾Fernández/Electronic Notes in Theoretical Computer Science 312（2015）8997满足公理（a1），它由定义4.4得出（因为现在我们考虑范畴之间的关系是相等关系，但我们将在后面处理一般情况）。Q然而，对于给定的策略，可能有多个图生成策略;例如，采取在未分配的权限上进行划分的任何图（即，在动作和资源之间的边缘上进行划分，使得没有边缘将动作连接到任何类别）。然而，存在对应于策略的唯一最小图。定义4.7 [路径类型]设v0，v1，.， v n是一条长度为n的路，使得type（v i）=Ti，其中0 ≤i≤n。路径的类型是由沿着路径的边的类型给出的序列，即T0T1，T1T2，...，T n−1T n.关系PCAG、ARCAG和PARG现在可以用某种类型的类型化路径来定义。举例来说PAR G={（lv（v1），lv（v3），lv（v4））|v1，v2，v3，v4是类型为PC，CA，AR的路径。还请注意，可以将最小唯一图定义为类型为CA和CA、AR类型的路径集合。这种将基于类别的元模型形式化为图的做法没有考虑分布式策略。这可以通过考虑对于每个站点，图中有一个特殊的附加节点，类型为S，标记为站点标识符，并且该站点的所有主体都连接到该节点来定义4.8[分布式策略图]设G=（V，E，lv，le）是表示策略的良类型策略图，设s∈S是分布式系统中的位置标识符。则站点s的策略图Gs由（V {vs}，E{vs}}）定义。{{v s，v}|v∈ V ∈type（v）= P}，lvJ，leJ），其中lvJ和leJ以自然的方式扩展lv和le，即通过将v s映射到s。分布式策略图是图的元组（Gs1，.，其中Gsi=（Vi，Ei，lvij，leji）是si的多项式，1 ≤i≤n. 如果每个位置s∈S，则关系PCAs、ARCAs和PARs被定义为（作为G s上的路径），如在非分布场景中一样。使用图表来正式化全球授权政策PAR并不那么直截了当。定义PAR的一种可能性是简单地通过工会，但还有更复杂的方法来组合政策。现在，我们将采取不同政策的联合定义4.9 [并图]设（Gs1，.，Gsn）是具有n个站点s1，...，s n，其中每个Gsi=（Vi，E i，lv i，le i）。 它们的关联并图定义为G=（V，E，lv，le），其中V是一个节点集，使得对于每个vi∈ Vi，其中lvi（vi）=x，存在唯一的节点v∈ V，使得lv（v）=x，E是一个边集，使得如果{v1，v2} ∈Ei，则存在边{v1，v2} ∈E，其中lvi（v1）=lv（v1），lvi（v2）=lv（v2），lei（{v1，v2}）=le（{v1，v2}）。98S. 阿尔维斯湾Fernández/Electronic Notes in Theoretical Computer Science 312（2015）89由于多条边可以连接同一对节点，这对应于多重图。注意，元模型的实体（主体、类别、操作和资源）可以被不同的站点所知。这意味着在全局策略的图形表示中，必须能够区分节点/边是否属于特定站点。为此，我们定义了两个函数visibleV：V →2S和visibleE：E→ S，使得对于每个节点v，visibleV（v）将返回具有与v具有相同标签的节点的站点集合，即v已知的站点集合，并且类似地对于每个边e，visibleE（e）将返回e定义4.10并图G中两个节点v0，v n之间的一条长度为n的路是序列v0，v1，.，v n，使得{v i−1，v i} ∈E，对于所有1 ≤i≤n，且所有边e1，.，路径中的e n在同一站点中可见。命题4.11联合图G定义了一个分布式的基于类别的策略，其中OP par是一个具有优先级的联合算子。证据根据定义2.5，我们需要证明公理（b1）和（f1）是满足的。公理（b1）由每个Gsi得出，对于公理（f1），如果存在PC，CA，AR类型的路径（可见E对于路径中的所有边总是相同的），则该路径也存在于某些Gsj中，这意味着par（p，a，r）∈ PARsj，因此它将属于OPpar{PARs|s∈ S}，如果OPpar是具有优先级的联合运算符。Q可以将同一实体的副本视为不同的节点，这些节点可以链接，然后在可视化显示图形时折叠成单个节点。我们稍后将讨论有效显示策略的不同选项。上面定义的可见V、可见E在图形表示方面，可以定义其他更复杂的策略组合，例如，考虑到冲突信息，但我们将在未来处理到目前为止，我们在元模型的图形形式化中还没有考虑到类别之间的关系。如前所述，这可以通过定义一个包含C类型节点的函数来实现。然而，这将不再允许我们仅仅基于路径来定义某些属性或者，我们形式化的CC型的边缘方面的关系。也就是说，我们允许边的集合包含形式为{c1，c2}的边，使得type（c1）=type（c2）=C。 请注意，边是无向的，但是，c1c2但不是c2c1。 因此，当定义涉及CC类型的边的路径时，需要知道这些边可以在哪个方向上被横穿。我们在边上定义一个函数target，使得如果vi∈target（{v1，v2}），则vi可以是该边的目的节点（注意，如果边可以在两个方向上被遍历，则v1，v2都可以是该边的目的节点考虑到目标函数，我们需要一个更有约束的路径概念，因此我们将对定义4.10进行改进：定义4.12G=（V，E，lv，le）中长度为n的约束路是一个序列v0，v1，. v n，使得对于所有1 ≤ i ≤ n，{v i−1，v i} ∈ E <$v i∈ target（{v i−1，vi}）。S. 阿尔维斯湾Fernández/Electronic Notes in Theoretical Computer Science 312（2015）8999C≥定义4.13设c1，c2是中的两个范畴，则c1c2，如果在c 1和c 2标记的节点之间有一条（CC）类型为C_4的约束路径。在本文中，我们只考虑类别之间的关系，但对于其他实体（例如资源或动作）也可以考虑相同定义4.14[动态策略图]动态策略图是一个良好类型的图G=（V，E，lv，le）以及V上的函数ld，使得ld（v）=R，对于满足以下条件的某个收敛重写系统R• 如果type（v）=P，则ld（v）定义一个函数pca，它返回（对于每个p）一个类别列表;• 如果type（v）=C，则ld（v）定义一个函数arca，它（对于每个c）返回一个权限列表（形式为（action，resource）的对）。模型中实体之间的关系可以以自主的方式改变（例如，由于系统中发生的事件），在某些类别中添加或删除主体/权限。在这个意义上，策略图可以被看作是系统在特定时间的照片。从图中可以提取在特定时刻的关系PCA、ARCA和PAR，但不知道如何得到下一张照片这就是ld函数的目的。定义4.15动态策略图在以下情况下被称为正确（在特定时刻）：• 对于类 型 P 的 每个节点v，Id（v）=[c1，...， c n] i中 存在边{v，v i}，对于i = 1，...，n，使得lv（v i）= c i;• 对于类型C的每个节点v，ld（v）= [（a1，r1），.，（a n，r n）] i ∈ {vai，vr i}和{v，va i}，i = 1，.，n，使得lv（va i）= ai，lv（vr i）= ri并且lv（v）= c;动态策略图表示动态的基于类别的策略。如果相关的动态图是正确的，则每个请求都有唯一的答案4.2基于图对于一个给定的策略，我们感兴趣的是检查某些属性，如原则、类别、资源和权限。我们首先考虑一个非分布式系统。作为静态属性的例子，人们可能有兴趣检查，我们考虑以下几点：（一）所有的主体是否与至少一个类别相关联？(ii)是否存在与所有类别关联的权限？(iii)所有的资源都有效使用了吗（根据主体和权限）？(iv)对于给定的类别，谁是相关的主体？（五）特定主犯属于哪类(vi)对于给定的类别，关联的权限是什么？(vii)对于给定的主体，关联的权限是什么？[4]我们考虑通常的 符号a，a，. a，n0。v˛n¸100S. 阿尔维斯湾Fernández/Electronic Notes in Theoretical Computer Science 312（2015）89对于由良好类型图G=（V，E，lv，le）表示的给定策略，上述属性可以以以下方式形式化：(i) 如果类型P的每个节点的度为正，则所有主体与至少一个类别相关联（在所有主体连接到站点节点的分布式场景中，则通过确保所有主体连接到类型C的节点来保证该属性）;(ii) 对于类型C的每个节点，存在类型为（CC）的路径，CA，AR。(iii) 对于类型R的每个节点，存在类型PC、（CC）N、CA、AR的路径。(iv) 对于一个给定的C型节点，找到所有P型的邻居。(v) 对于一个给定的P型节点，找到所有C型的邻居。(vi) 对于一个给定的C类型的节点，找到所有类型为（CC）的路径，CA，AR。每个路径的最后两个节点将定义与该类别关联的权限。(vii) 对于一个给定的P型节点，找出所有PC、（CC）、CA、AR型路径。最后两个节点将定义与该主体关联的权限命题4.16上面所有的检查都可以在多项式时间内计算，|V|+的|E|.注意，上述属性在分布式场景中仍然有效，或者通过考虑各个图Gs1，.Gsn，或上面定义的并图中的路径概念。可以使用基础图上的属性检查其他静态属性特别是对于分布式场景。 例如，检测是否存在冲突的权限。 如果资源r中的动作a1与r中的动作a2相冲突，则对于每个主体p， 是并图中连接p和r的一条PC，（CC）-R，CA，AR对于给定的并集图，我们也可以问，对应于策略的最小唯一图是什么。 这可以通过从类型S的节点开始并考虑生成树中的边来计算，仅考虑以类型P、C和R的节点结束的分支。通过这种方式，可以消除类型A和R的节点之间不与任何类别相关联的边，以及类型C和R的节点之间不与任何资源相关联还有更复杂和相关的问题可以用这种形式主义来处理。举例来说• 对于给定的策略图G，以及给定的主体集合{p1，...，p n}和许可{（a1，r1），.，（an，rn）}，确保给定主体集合共同具有给定权限所需的最小更改次数（在PCA和ARCA虽然这是一个复杂的问题，但通过固定主体或权限的数量，我们可以获得问题的可管理实例。• 对于给定的策略图G，以及给定的主体集合{p1，...，p n}和许可{（a1，r1），.，（an，rn）}，保证这些用户可以获得这些权限S. 阿尔维斯湾Fernández/Electronic Notes in Theoretical Computer Science 312（2015）89101人们可能对保证一组特定的权限分配感兴趣，但是以受控的方式，特别是在紧急情况下。对于单个对（p，（a，r）），这相当于找到图中的最短路径，将主体连接到权限。4.3应用：应急管理我们的主要动机是提供一个分析框架来处理策略更新，允许安全管理员检测在涉及紧急情况的场景中引入策略的更改如第3节所述，可以使用额外的应急站点对应急策略进行建模。通过将正常策略的图与紧急策略的图相结合（采用适当的合成算子），给出了紧急情况下策略的图表示。例如，当使用具有优先级的union操作符组合两个策略时，上面定义的union-graph将出现。然后，在处理紧急情况时，可以使用上一节中描述的分析来指定属性。 例如，可以保证，在任何医生都可以通过显示对于医生类别中的每个主要P，-在与紧急策略相关联的图中的形式为p、c+、access、recordi 的类型为PC、（CC）n、CA、AR正常策略和紧急策略的图可以用来分析其他性质。例如，人们可能希望确定哪些权限被紧急事件撤销;哪些权限被紧急事件创建;每个主体是否具有特定的权限。 许可 期间 紧急情况; 是否 或者在紧急情况下不禁止某个动作，等等。所有这些属性都可以很容易地使用我们的图形形式化建立。“职责分离”约束也对应于路径约束。 例如，如果策略图中的类型PC、（CC）报警、CA、AR的路径集合不包括以激活、报警结束的路径和以删除、记录并在类型P的相同节点中开始的路径，则约束5分析政策的工具在本节中，我们将描述一个使用图形形式化来分析策略的工具。5.1策略的可视化表示如前所述，在基于类别的元模型中使用图来形式化地表示策略在算法和来自图论的良好建立的属性方面具有许多优点，所述图论可以用于分析这些策略的属性，以及用于以有效的方式显示图的工具。回想一 下 ，我们将分布式系统定 义 为一个元组（G1，...， Gn），以及102S. 阿尔维斯湾Fernández/Electronic Notes in Theoretical Computer Science 312（2015）89联合图G作为组合来自各个策略Gi的所有信息的多重图。还记得，每个Gi包含一个S类型的特殊节点，每个主体都连接到该节点由于P C A R中的实体对于所有站点都是全局的，因此系统的适当可视显示应清楚地显示每个实体所在的站点。理想情况下，人们希望在3维空间中表示系统，其中每个站点将处于不同的水平面，其中几个站点的共同身份可以选择不同的水平平面并将其合并以组合策略。考虑到操作/显示此类图形的复杂程度，我们考虑替代选项：• 所有不同的Gi都在同一平面上表示，但不同的颜色用于识别不同的站点（如果一个节点在几个站点中是已知的，那么它被它所属的每个站点的不同颜色环• 通过选择一个节点站点（S类型的节点），其他站点的所有颜色都变为灰色，从而突出显示所选站点。• 因为我们表示的是一个多重图，所以在相同的节点之间可以有多条边。他们应该使用与他们的网站相关的颜色来表示。• 为了进一步突出显示选择，可以增加所涉及的节点的大小（或者可以减少未涉及的节点）。请注意，未连接的实体不能与任何站点相关联，在这种情况下，函数visibleV可以用于确定节点的颜色。当表示并集图时，函数visibleE也用于确定边缘的颜色。可以考虑其他可能性，例如表示对应于其出现的不同位置的相同实体的不同副本，以及使用特殊边缘来连接不同副本。然后，每个策略可以单独显示，与其他策略的连接由附加边给出。该替代方案将给出每个单独策略的清晰可视化（特别是如果可以省略附加边缘），但不会提供 对一般政策的适当概述5.2Ruby原型一个名为Policy Manager[28]的应用程序被实现，为安全管理员提供了一个易于使用的图形工具，允许构建和管理多个策略。该应用程序是用Ruby [21]实现的：一种解释型、面向对象、多范式的编程语言。在策略数据的图形显示方面，策略管理器提供了用户友好的可视化表示，便于识别策略对象的任务该应用程序以树的形式为用户提供了策略的完整视图，允许用户放大树中过于拥挤的部分。它还允许选择特定的实体，突出显示与该实体相关联的节点和边。例如，通过单击主体名称，树将以所选对象为中心，从而可以更清楚地查看与该主体关联的类别和权限。此外，用户能够通过拖动来重新定位元素，如S. 阿尔维斯湾Fernández/Electronic Notes in Theoretical Computer Science 312（2015）89103并从视图中删除不相关的元素该应用程序还包括一个文本视图，允许有关政策的简单查询。该项目的一个关键方面是实现类别的动态与RBAC中的角色不同，类别可以根据事件或系统状态的变化动态变化（紧急情况可以被视为特定类型的事件）。为了表示动态图（参见定义4.14），该工具允许用户保存描述数据库中事件的Ruby代码然而，这需要用户具备Ruby语言的知识，同时也会带来安全问题。更理想的解决方案是定义一种用户友好的领域特定语言，允许用户指定类别和权限，例如使用重写规则。然后可以将这种语言编译成代码，插入到策略数据库中（就像当前用于指定类别的Ruby代码一样6相关工作在文献中已经使用了几种形式语言来建模和分析访问控制问题。Koch等人[26]使用图来形式化RBAC，特别是通过图转换规则来建模角色管理操作。最近，[6，29，12]使用术语重写规则来建模特定的访问控制模型并表达访问控制策略。我们的方法结合了使用图的形式主义来表示系统的具体状态，并使用重写规则来模拟这个系统的动态。广义TRBAC模型[25]和ASL [23]旨在为政策定义提供一个通用框架，但它们主要关注用户，群体和角色的概念（被解释为与工作职能的概念同义）。Li等人'的RT系列角色信任模型[27]提供了一个通用框架，专门用于定义特定的策略要求（在凭证方面）。通过重写系统来指定策略不仅可以利用广泛的重写理论来建立安全属性，如[29，17，10]中所示，还可以利用基于重写的框架（如CiME，MAUDE或TOM）来推理策略属