图变换的访问控制策略的规范化和演变：统一且精确的框架

网址：http://www.elsevier.nl/locate/entcs/volume51.html11页访问控制策略Manuel Koch1、Luigi V. Mancini2和Francesco Parisi-Presicce2;31PSI AG，柏林，德国2Univ. di Roma La Sapienza，罗马， 意大利3乔治梅森大学关闭TN，USA摘要图变换为访问控制策略的规范提供了一个统一而精确的框架。状态由图表示，状态转换由图变换表示。策略由四个部分形式化：类型图、正约束和负约束以及一组规则。这种形式主义允许不同的政策模型的详细比较和政策的演变和政策的整合关键词：安全，访问控制，规则库规范，进化。1引言访问控制（AC）保护计算机系统免受未经授权的访问或修改信息，无论是在存储，处理或trans-sit。在这方面，AC关注的是确定计算系统用户的合法活动[San94]。已经提出了几种模型来解决计算应用的AC要求。传统的AC模型被广泛地分类为自主访问控制（DAC）[San94]和强制访问控制（MAC）[San93]模型。在DAC模型中，访问授权规则是为计算系统中的每一对（主体，对象）指定的。 主体可以是用户、组或代表其他主体的进程。如果一个主体是对象O的所有者，则该主体被授权自行决定授予或撤销对O的访问权限给其他主体。DAC模型具有固有的灵活性1 电子邮件地址：mkoch@psi.de2 电子邮件：lv. dsi.uniroma1.it3 电子邮件地址：fparisi@ise.gmu.educ 2002年由Elsevier Science B出版。V.CC BY-NC-ND许可下的开放访问。2并且最广泛地用于商业系统，例如Unix操作系统。然而，这些模型并不提供高的安全性保证和抵御特洛伊木马Hoarse攻击。例如，如果授权用户访问执行包含特洛伊木马骗局的程序的对象O，则O可能被恶意地复制到具有较低授权的另一个对象中，这导致允许对原始O没有访问权的用户访问O的副本。发援会的大多数现有实施都遵循人权股模式[人权股]。该模型基于访问控制矩阵，其中每个元素指定特定主体访问系统中特定对象的访问权限一般来说，HRU的安全性是不可判定的。基本的安全问题是确定是否存在可达状态，在该状态下，给定的主体拥有它先前不拥有的给定授权MAC模型看起来更加严格，所有主体和对象都基于授权决策期间使用的预定安全级别进行分类。MAC模型关注的是控制和执行信息流的问题，而DAC模型没有解决这个问题。在MAC中，访问控制策略由系统强制执行，并且不能被用户或受损的应用程序覆盖。例如，为了确保军事应用中的信息保密性，MAC模型使用不采用读和写规则的多级安全限制来实现。这些规则旨在确保信息不会从较高的安全级别流向较低的安全级别，即使在较高安全级别的受损应用程序包含恶意特洛伊木马Hoarse。尽管有这些有吸引力的包容性，MAC模型还没有被用于分类信息处理领域之外。具有MAC功能的系统不再支持标准应用程序或管理工具，并且它们的管理和使用比基于DAC的系统复杂得多。此外，MAC系统实现了一种过于强大和限制性的遏制形式，即标准应用程序通常无法再正常运行。新的模型，如基于角色的访问控制（RBAC）[San98，SFK00]已被提出，以解决更广泛的应用程序的安全要求。特别是，RBAC模型引入了新的角色概念来组织用户和访问权限，其中角色表示信息系统用户的组织责任。RBAC模型提供了几个公认的优点。它们已被证明是“策略中性”的，这意味着使用RBAC功能可以表达广泛的安全模型，包括传统的DAC和MAC。使用角色还可以简化安全管理。 例如，如果为用户分配了组织内的新任务时，用户将从旧角色撤销并分配给新角色，而在其他模型中，用户的旧权限必须单独删除，新权限必须授予。考虑到文献中定义的各种不同的AC模型，3一个重要的问题是如何评估和比较所有这些模型的表达能力和实现的复杂性方面的功能。因此，似乎有必要制定一个正式的框架，以指定和比较不同的AC模型的功能特别地，本文使用图变换的形式化框架讨论了任何AC模型的演化、转换和集成的AC模型的演化包括改变现有模型的AC规则和约束。在约束不被修改的功能性违反的意义上，改变必须保持一致性。从一个AC策略到新的AC策略的转换也会出现类似的问题。除了AC模型的演化和过渡之外，现有AC政策的整合形成了产生新政策的第三种机制。只要不同策略允许的访问没有冲突，策略的集成就相对简单。如果存在冲突，如果在统一的正式框架内描述不同的策略，则可以更容易地研究和协调冲突。我们正在进行的工作的主要目标是系统地描述不同AC政策的演变，不同AC政策的整合以及从一个政策到另一个政策的过渡。提出了一个独特的正式框架来解决这两个问题。本文使用图转换来指定一个RBAC模型。我们知道最近有两篇关于整合AC政策的文章（[BDS 00，BCFP01]）第一种是用标准的表达式语言来定义模型代数，它的语义是基于主语、宾语、权限三元组以及规则是Horn子句的事实。相反，我们专注于图形规则和正式的工具，以协助发展和整合政策的过程中，以保证一个连贯的模型。2安全政策框架本节介绍基于图转换的AC策略规范的框架。该框架被称为安全策略框架，由四个组件组成：第一个组件是一个类型图，提供AC策略的类型信息[CELP 96]。第二个组件是一组图形规则，指定生成表示AC策略所接受的系统状态的图形的策略规则。对于某些AC策略，限制由图规则构造的系统图的集合是有意义的，因为并非所有系统图都表示有效状态。因此，安全策略框架还包含两组约束，这两组约束指定不应包含在任何系统图中的图（负约束）和必须被显式地构造为系统图的部分的图（正约束）。 在AC策略的实际实现中，约束是多余的，因为唯一可接受的状态是由实现的规则显式构建的状态。但是，当开发一个4RAC策略通过连续的执行步骤，或者当比较不同的策略时，或者当试图预测通过集成两个不同的策略而获得的策略的行为时，具有由约束提供的附加信息是有用的。此外，从“建设性”规则中提取消极信息通常是困难的。正约束和负约束可以被认为是规则的初始需求和开发过程的正式文档。其次，我们构造了一个类型图TG，并假定所有的图和图态射都是TG中的类型图。图规则p：（L！R; A（p））由规则名p、部分图态射r和一组负应用条件（NAC）A（p）= f L！ Ni：i2Ig包含具有源L的全图态射[HW 95]. 对于通过图形规则导出图形，选择单推出方法是因为其（在AC策略领域）自动删除悬挂边的期望属性。正约束和负约束都由态射形式化地指定只有它们的语义才能区分它们。定义2.1 [负约束和正约束]一个约束（正或负）由一个全图态射c：X给出！ Y.一个图G满足一个正（负）约束c，如果对每个全内射图态射p：X！G存在（不存在）全内射图态射中澳q：Y！ G这样X！ Y！ G = X！ G.定义2.2[安全策略框架]一个安全策略框架，或者只是框架，是一个元组SP =（TG;（P; r P）;P os;N eg），其中TG是一个类型图，对（P; r P）由一组规则名称和一个总映射rP：P！j规则（T G）j 4，P os是一组正约束，N eg是一组负约束。示 例2.3[基于角色的访问控制]该示例展示了基于角色的访问控制（RBAC）模型[San98，OSM00]的变体的安全策略框架。此模型考虑多个用户角色（或仅角色）和负责用户角色分配的多个管理员角色。角色和管理角色都在由偏序给出的层次结构中排序。在图1中，示出了管理角色层次结构（在左手侧）和角色层次结构（在右手侧）的示例，其中层次结构由图形给出角色和管理角色分别由r和ar类型的节点给出，角色之间的边表示继承关系。通常，在层次结构中比部门主管角色更高的部门主管角色继承与部门主管相关联的所有权限。4范畴规则（TG）具有所有对（r; A）作为对象，其中r：L！ R是一个部分图态射，A是一个具有源L的全图态射集。5RarRRarRRarRRarRuS部门分配给“部门主管”角色的用户Smith被授予与该角色关联的所有权限。Fig. 1. 管理员角色层次结构（左）和角色层次结构（右）。图二.RBAC模型的类型图。图概括了偏序的概念，通过定义特定的规则，可以将图结构限制为任何角色层次结构。此外，图1示出了管理角色和用户角色之间的边缘，表示管理角色修改用户角色的授权。 这些边从管理角色可到达的角色集是管理角色的范围。例如，上层管理员角色的范围由上层ve角色给出，而下层管理员仅具有最低角色的授权。管理员可以为用户分配角色或撤消其角色。如果用户被直接分配给某个角色，则该用户是该角色的成员。她/他如果某个角色是从该用户分配到的角色继承的，则为该角色授权。用户可以建立会话，在该会话期间，用户激活她/他被授权的角色考虑到该RBAC模型，SPF的类型图（参见图2）包括管理员角色的节点类型ar、角色的节点类型r、用户的节点类型u和用户会话的节点类型s。ar和r节点的循环分别用于指定层次结构。从节点u到节点r的边称为分配边，它将用户分配给角色，节点u处的循环指定不存在分配边。节点s和节点u之间的边将会话分配给用户。本文没有考虑角色的创建和删除，因此RBAC模型的基本操作是添加用户、删除用户、添加分配、删除分配、添加会话、删除会话、激活角色和停用角色。所有这些操作都由图1中的图转换规则建模3.第三章。添加用户规则向系统引入新用户新创建的规则remove user也会删除用户及其所有会话，以确保6uRu添加到角RararuRar从角色中uRarSSuR*r激活角色uSSR*ruR停用角色uRSS添加用uu删除用户Su新会话u删除会话S图三. 集中式RBAC模型的图形规则。不存在已删除用户的活动会话。 这由rule remove user左侧的双圈会话节点表示。解释是连接到用户的所有会话都将被删除。角色是一组角色的缩写，这些角色组成了每个可能会话数量的规则否定应用条件可以确保当且仅当出现的会话节点的数量与规则所指定的会话节点的数量相同时，规则是可应用的。创建和删除会话的规则是新建会话和删除会话。会话节点s通过边直接连接到正在使用s的用户。可以随时删除会话，而不管会话的活动角色是否存在。添加到角色规则通过分配边连接用户和角色，将用户分配给角色。这个想法是每个用户最多有一个分配，即一个用户最多可以在一个角色。成员资格由用户节点u处不存在循环来指示。添加到角色规则需要循环，并在规则设置分配时删除循环。规则remove fromrole删除分配边缘并停用用户的所有会话。所有会话都可以被停用，因为会话的所有激活角色都由一个分配边缘授权。不能激活未被此分配授权的角色。用户节点再次配备有环路。 用户可以激活她/他被授权的任何角色r。如果存在以分配边开始并以r结束的路径，则用户被授权使用r。对应的图形规则是激活角色。 此边由会话的用户创建。 星 在角色之间的边缘表明通过角色层次结构的（可能为空）路径。空路径表示用户还可以激活其直接分配的角色。角色r只能在r还不是会话的成员时加入会话，如会话节点和角色节点之间NAC的虚线所示。从会话中取消激活角色是通过删除7TG TG会话和角色节点之间的边缘。图4中给出了负约束和正约束的示例。负约束要求用户节点u处的循环不能与分配边同时发生（上约束），并且用户不能处于两个或更多个角色（下约束）。这样可以确保一个用户最多分配一个角色。正约束要求每当为角色激活用户会话时，会话的用户都被授权使用该会话。负约束：正约束：见图4。 RBAC模型的约束。可以由框架的规则构造的图表示策略模型中可能的系统状态。这些图在下文中称为系统图。安全策略框架是一致的，如果所有的系统图满足框架中的正约束和负一个安全策略框架态射f：SP1！SP2，或者仅仅是框架态射，通过全图态射f TG：TG1 将 安 全 策 略 框 架 联 系 起 来！ 型图与映射fP： P1 之 间 的 T G2！ 规则名称集之间的P2。映射fP必须保持规则的行为，因为只有当fP（x）在重命名的类型上做了x做的一切，甚至可能更多时，规则名x才能映射到规则名fP（x）SP2中的正约束的集合除了Pos1之外还可以包含新的正约束和SP1扩展的正约束w.r.t. 新类型。SP2中的负约束集可以包含对新类型的附加负约束，但不能对旧类型施加新的负约束。定 义 2.4[ 框 架 态 射 ] 安 全 策 略 框 架 工 作 SPi= （ TGi;（Pi;rPi）; Posi; Negi）（i=1;2）之间的框架态射是一对f=（fTG;fP）：SP1！ SP2 ， 其 中fTG ： TG1！ TG2 是 一个全图 态射， 且 fP ：P1！P2是一个全映射，使得VfTG（rP2（fP（p）=rP1（p）对所有p2P1，Pos1Vf （Pos2）和Vf（Neg2）Neg1. 5安全策略框架的范畴，由SP表示，具有作为对象的所有安全策略框架和作为态射的所有框架态射。5fTG 是由f诱导的遗忘函子TG等uuR*SRSRuRRuRV8对于每个框架SP，idSP=（idTG; idP）是身份，并且组成是按组件定义的。范畴SP是nitely cocomplete[KMPP01b]。3不断演变的政策正如在实际的任何开发活动中一样，安全策略的规范是一个渐进的过程：随着对需求的更好理解，对想要的（积极约束）和不想要的（消极约束）状态的初始描述必须不断发展。修改AC策略的过程可以处理局部变化（策略通过添加/移除个体约束和规则而演变）、模块化变化（两个策略被组合以形成较大的策略，其中原始策略是子组件）以及全局变化（一个策略被另一个策略替换）。当必须修改策略以考虑对安全需求的更好理解或安全需求的变化安全策略框架SP=（TG;（P; rP）; P os; N eg）可以通过修改其组件来改变，即，类型图的扩展或缩减、向P添加图规则/从P移除图规则、向Pos添加正约束/从P os移除正约束以及向N eg添加负约束/从N eg移除负约束。 一个框架态射f：SP1！SP2描述了框架SP1的变化 到框架SP2，也可以从SP2到SP1。我们把进化定义为范畴SP中的一系列框架态射，它们可以在两个方向上运动定义3.1[演化]框架SP到框架的演化SP0 是框架的序列e=（ SP SP：SP SP），使得 SP=0 1n 1n0SP， SPn= SP，并且对于每个 i= 0;：;n1、存在框架态射0m f：SP！ SP或m b：SP ！ SP.ii i+1ii+1i安全策略框架的演变产生了反映所需变化的新的安全策略框架。然而，这些变化并不能确保新的安全政策框架总体上是连贯一致的。从语义的角度来看，这个问题可以通过考虑SP的仅包含一致的安全策略框架的完整子类别SPc来解决。进化只有在这个子类别中才是可能的。从操作的角度来看，我们可以通过使用最初在[HW 95]中介绍的机械结构来解决这个问题。该构造通过添加应用条件来操纵框架的规则，以确保规则不会创建不满足约束的图。 [KMPP00，KMPP01a]中介绍了生成一致性安全策略框架的方法。当两家公司合并时，可能会发生模块化更改，同时保留其权利和行为的主要部分，因此两家公司的安全信息也必须合并。合并发生在与安全策略框架的语法级别上，并在语义级别上与表示公司状态的系统图进行合并9合并语义层面上的合并是演化与集成的区别：演化在语法上只考虑安全策略框架，集成也包括语义变化。两个AC策略在语法级别上的集成通过类别SP中的安全策略框架的推出产生新的安全策略框架。两个安全策略框架SP1和SP2通过辅助框架SP 0相关联，该辅助框架SP0标识两个框架中的公共部分（类型和规则）;实际的集成由框架态射f1表示：SP0！SP1和f2：SP0！SP2. F1的推出 和f2 在SP中，将框架SP1和SP2集成到一个新的安全策略框架SP中，称为集成框架。请注意，由于SP中存在（nite）共极限，本文的集成概念可以很容易地推广到几个框架的集成。一个重要的集成方面是保持一致性：如果框架SP1和SP2是一致的，那么SP是否是一致的？一致性w.r.t.负约束总是通过推出[KMPP01b]保留。一致性w.r.t.外推构造通常不保持正约束。不连贯的原因w.r.t.然而，正约束可以被简化为涉及公共类型的正约束的部分。引用仅在SP1或仅在SP2中出现的类型的正约束的一致性被保留。集成两个策略的另一个重要问题是规则的重叠。如果两个相似的规则可以在给定时刻应用，并且，比如说，它们不是平行独立的（即，一个的应用可能阻止另一个的应用），必须做出（外部）决定来确定“策略”。不同的策略是可能的，从一个策略的优先级到规则的优先级。在第一种情况下，选择两个策略中的一个，并且另一个策略的规则被完全丢弃（激进的解决方案）或配备NAC以消除冲突;在第二种情况下，分析每对规则，并且其中一个（不总是来自相同的策略）优选修改另一个（静态）或在运行时（动态）选择应用哪个规则。当AC政策被认为不适合特定公司，希望用新政策取代当前政策，并且新政策是今后唯一使用的政策时，就会发生政策的全球变化从策略A到策略B的转换可以看作是一个两步进化过程，第一步是在采用策略A优先的策略后，将A嵌入到A+B中，然后再将A的逆态射嵌入到B中。4总结发言我们已经提出了一个形式主义，以指定AC政策。状态由图表示，它们的演化由图变换表示。策略由四个部分形式化：类型图、正约束和负约束（10描述什么是想要的和什么是禁止的声明性方式）和一组规则（描述可以构造什么的操作性方式策略随时间的变化可以用框架态射的序列来描述，对应于规则和约束的逐步添加/删除我们还讨论了在策略框架和框架态射范畴中使用推出来集成两个策略的效果在调查中的剩余问题是，不仅比较不同的访问控制模型（DAC，MAC，RBAC）的表达能力，但它们的相对复杂性。 这可以通过在不同的模型中表达图形规则来实现，这些模型是使用表达式[GRPPS00]构建的，这些表达式来自于在普通安全系统中容易实现的少量基本操作。引用[Bal90] R.W.鲍德温在大型数据库中进行安全管理的特权。1990年IEEESymposium on Research in Security and Privacy，pp. 116{132. IEEE计算机协会出版社，1990年5月。[BCFP01] E.贝尔蒂诺湾Catania，E.Ferrari和P.佩拉斯卡访问控制模型推理的逻辑框架 在proc 第六届ACM研讨会 访问控制模型和技术41{52. ACMPress 2001.P. Bonatti，S.D. C. di Vimercati，和P.萨马拉蒂一种组成访问控制策略的模块化方法在S.Jajodia和P.Samarati编辑的ACM计算机和通信安全会议的论文集，第164页{173. ACM，2000年11月[CELP 96]A. Corradini，H. Ehrig，M. Lo we和J. Padberg. 图文法的范畴及其与导子范畴的附属。在第五届国际图形语法及其在计算机科学中的应用研讨会上，LNCS第1073号，第56页。Springer，1996年。M. Gro e-Rhode，F. Parisi-Presicce和M.西梅奥尼通过规则表达式实现图变换系统。In H. Ehrig，G.恩格斯，H. J. Kreowski和G. Rozenberg，编辑，Proc. ofTAGT'98，编号1764，LNCS，第368页{382.斯普林格，2000年。[HRU]哈里森，MH，Ruzzo，W. L.，和Ullman，J.D.，操作系统中的保护，ACM通讯，19，8，pp。461-471，10月一九七六年[HW 95] Reiko Heckel和Annika Wagner。确保条件图文法的一致性-一种建设性方法。 在Proc.的SEGRAGRA'95图重写和计算，编号2。 TCS电子笔记，1995年。http://www.elsevier.nl/locate/entcs/volume2.html的网站。[KMPP00] M. Koch、L.V. Mancini和F.巴黎普雷西切。基于图变换的角色访问控制形式化模型。在第六届会议上，11欧洲计算机安全研究研讨会（ESORICS 2000）编号1895，LNCS，第122页。Springer，2000年[KMPP01a] M.科赫湖V.Mancini和F.巴黎普雷西切。访问控制策略的规范和发展。第六届ACM Symp.访问控制模型和技术第121页{130. ACM Press2001.[KMPP01b] M. Koch、L.V. Mancini和F.巴黎普雷西切。基于图的访问控制策略规范方法的基础。在Proc. FoSSaCS 2001，编号2030，LNCS中，第287页{302.Springer，2001年[OSM00] S.奥斯本河Sandhu和Q.穆纳沃配置基于角色的访问控制以实施强制性和 描 述 性 访 问 控 制 策 略 。 ACM Transactions on Information and SystemSecurity，3（2），May 2000.[Roz97] Grzegorz Rozenberg，editor. 图文法与图变换计算手册。 第一卷：基础。 World Scienti c，1997.[San93] R. S. Sandhu基于网格的访问控制模型。IEEE 计算机，26（11）：9{19，1993.[San94] R. Sandu和P. Samarati。访问控制：原理与实践。IEEE通信杂志，第40页，1994年。[San98] Ravi S. Sandhu基于角色的访问控制。《计算机进展》第46卷中国科学技术出版社，1998年.[SFK00] R. Sandhu，D. Ferraiolo和R.库恩NIST基于角色的访问控制模型：走向统一标准. 第五届ACM基于角色的访问控制研讨会。ACM，2000年7月