（计算机应用技术专业论文）基于模型检测的空间访问控制系统规则验证.pdf

江苏大学硕士学位论文 摘要 随着空间数据库、地理信息系统、基于用户位置服务和移动应用 的普及和广泛应用，空间数据库管理系统的安全问题得到越来越多的 关注。带有空间特性的角色访问控制模型s p a t i a l r b a c 规定系统达 到必要的安全要求须满足一定的空间约束，即空间区域约束、空间角 色激活基数约束和空间职责分离约束。验证空间访问控制系统是否满 足以上三种约束，对保证访问控制系统的安全性至关重要。 本文采用模型检测的方法来验证空间访问控制系统规则是否满 足相应的约束。模型检测技术是一种被广泛应用的验证有限状态系统 满足规范的自动化分析方法，其基本思想是先建立待测系统的有限状 态模型，然后通过穷尽搜索模型中的状态，判断其是否满足待测属 性。本文主要内容如下： ( 1 ) 提出了一种基于谓词逻辑的空间访问控制系统的描述方法。在 这个方法中，系统由谓词及规则共同组成，其中谓词表示各空间类中对 象之间的关系，规则反映了系统授权给用户的谓词读写权限。空间信息 经映射函数处理后作为系统授权的条件之一，保证了系统描述的规范和 简洁。 ( 2 ) 提出了待验证属性的表示方法及检测算法。将s p a t i a l r b a c 规 定的空问约束属性表示成统一的检测目标的形式，并针对这种统一形 式设计了规则验证的模型检测算法。该算法利用用户对系统的认知来表 示系统状态，将用户对系统变量是否具有读写权限作为状态的变迁条 江苏大学硕士学位论文 件，从目标状态开始由后往前遍历系统状态空间，找出完成e l 标需要的 操作序列，若搜索成功则表示系统中存在空间约束不满足的情况。 ( 3 ) 改进了模型检测工具a c p e g 。在对a c p e g 源代码分析的基础 上，加入了空间位置信息的处理能力并修改了源代码中检测算法的实现 部分，使其满足空间访问控制系统规则检测的需要。最后通过一个空间 访问控制系统规则检测分析的实例，验证了本文提出的检测方法的正 确性及有效性。 关键词：访问控制，s p a t i a l r b a c ，空间约束，模型检测 江苏大学硕士学位论文 a b s t r a c t i no r d e rt oa c h i e v et h en e c e s s a r ys a f e t yr e q u i r e m e n t s ，t h er o l e b a s e da c c e s s c o n t r o lm o d e ls p a t i a l r b a c ，谢t ht h es p a t i a lc h a r a c t e r i s t i c s ，m u s tm e e tt h et h r e e c o n s t r a i n t s ：t h ec o n s t r a i n to ns p a t i a lr e g i o n ，t h es p a t i a ls e p a r a t i o no fd u t yc o n s t r a i n t a n dt h ec o n s t r a i n to nc a r d i n a l i t yo fs p a t i a lr o l ea c t i v a t i o n i ti sv e r yc r u c i a lt oe n s u r e t h es e c u r i t yo ft h ea c c e s sc o n t r o ls y s t e mt h a tv e r i f y i n gw h e t h e rt h ea c c e s sc o n t r o l s y s t e mm e e tt h et h r e ec o n s t r a i n t s i nt h i sp a p e r ，t h em o d e lc h e c k i n gm e t h o dw a su s e dt ov e r i f yw h e t h e rt h er u l e so f s p a t i a la c c e s sc o n t r o ls y s t e mm e e tt h ec o r r e s p o n d i n gc o n s t r a i n t s m o d e lc h e c k i n g t e c h n o l o g yi saw i d e l yu s e da u t o m a t e da n a l y s i sm e t h o di nv e r i f y i n gf i n i t e s t a t e s y s t e m s ，a n dt h eb a s i ci d e ai st oe s t a b l i s ham o d e lo ff i n i t e s t a t es y s t e m ，a n dt h e n v e r i f yw h e t h e rt h es y s t e mm e e tt h ep r o p e r t i e sb ys e a r c h i n gt h es t a t e si nt h em o d e l t h em a i nc o n t e n t so ft h i sp a p e ra sf o l l o w s ： ( 1 ) am e t h o do fr e p r e s e n t i n gs p a t i a la c c e s sc o n t r o ls y s t e m ，w h i c hi sb a s e do n p r e d i c a t el o g i cw a sp r o p o s e d i nt h i sm e t h o d ，t h es y s t e mc o n s i s t so fp r e d i c a t e sa n d r u l e s ，i nw h i c ht h ep r e d i c a t ei n d i c a t e st h er e l a t i o n s h i po ft h es p a t i a lc l a s so b j e c t ，t h e r u l e sr e f l e c tt h ea u t h o r i t i e so fr e a d i n ga n dw r i t i n gt h ep r e d i c a t e s s p a t i a li n f o r m a t i o n p r o c e s s e db yt h em a p p i n gf u n c t i o ni so n eo ft h ec o n d i t i o n sa u t h o r i z e da sas y s t e mt o e n s u r et h a tt h es y s t e md e s c r i b e di nt h es p e c i f i c a t i o na n dc o n c i s e ( 2 ) t h er e p r e s e n t i n gm e t h o da n dd e t e c t i n ga l g o r i t h mo fp r o p e r t i e st ob ev e r i f i e d w e r eg i v e n t h er e p r e s e n t a t i o no fc o n s t r a i n ta t t r i b u t e si nt h es p a t i a l r b a cw e r e g i v e ni nau n i f i e df o r m ，a n dan e wa l g o r i t h md e t e c t i n gt h er u l e so fs p a t i a la c c e s s c o n t r o ls y s t e mw a sp r o p o s e di nt h eb a s eo fe x i s t i n gm o d e lc h e c k i n gm e t h o d t h e a l g o r i t h mu s e st h eu s e r sk n o w l e d g eo ft h es y s t e mt oi n d i c a t es y s t e ms t a t u s ，a n dp u t s t h er e a d i n ga n dw r i t i n ga u t h o r i t ya sac o n d i t i o no fs t a t ec h a n g e ，s t a r t i n gf r o mt h e t a r g e ts t a t ea f t e rt h ef o r w a r dt r a v e r s a lf r o mt h es y s t e ms t a t es p a c et oi d e n t i f yt h e o p e r a t i o nn e e d e dt oa c h i e v et a r g e t ss e q u e n c e ，i ft h es e a r c hi ss u c c e s s f u l ，i tm e a n st h a t s o m es p a c ec o n s t r a i n t sa r en o ts a t i s f i e di nt h es y s t e m ( 3 ) t h ef u n c t i o no fm o d e lc h e c k i n gt o o la c p e gw a si m p r o v e d b ya d d i n gt h e i i l 江苏大学硕士学位论文 s p a t i a li n f o r m a t i o np r o c e s s i n gc a p a c i t ya n dm o d i f y i n gt h es o u r c ec o d et oa c h i e v et h e d e t e c t i o na l g o r i t h m ，t h et o o lc o u l dm e e tt h en e e do fd e t e c t i n gs p a t i a la c c e s sc o n t r o l s y s t e mr u l e s f i n a l l y , a ne x a m p l eo fa c c e s sc o n t r o ls y s t e mw a sa n a l y z e da n dt h er e s u l t s h o w st h a tt h ep r o p o s e dd e t e c t i o nm e t h o di sc o r r e c ta n de f f e c t i v e k e yw o r d s ：a c c e s sc o n t r o l ，s p a t i a l - r b a c ，s p a t i a lc o n s t r a i n t s ，m o d e lc h e c k i n g i v 学位论文版权使用授权书 本学位论文作者完全了解学校有关保留、使用学位论文的规定， 同意学校保留并向国家有关部门或机构送交论文的复印件和电子版， 允许论文被查阅和借阅。本人授权江苏大学可以将本学位论文的全部 内容或部分内容编入有关数据库进行检索，可以采用影印、缩印或扫 描等复制手段保存和汇编本学位论文。 本学位论文属于 保密口，在年解密后适用本授权书。 不保密 学位论文储繇雾眈移 扣p 年易月昌e t 艚刻磴轹翔 加f 刁年6 月7 e l 时免 独创性申明 本人郑重声明：所呈交的学位论文，是本人在导师的指导下，独 立进行研究工作所取得的成果。除文中已经注明引用的内容以外，本 论文不包含任何其他个人或集体已经发表或撰写过的作品成果。对本 文的研究做出重要贡献的个人和集体，均已在文中以明确方式标明。 本人完全意识到本声明的法律结果由本人承担。 学位论文作者躲如瓣 狮年6 月日 江苏大学硕士学位论文 1 1 研究背景及意义 第一章绪论 在计算机联系尤其紧密的互联世界中，访问控制的重要性在迅速增长。访问 控制规则就是访问控制系统建立的授权策略。要使一个访问控制系统变得合法有 效，重要的是确保访问控制规则的正确定义。一个访问控制系统的规则必须要满 足系统将要提供的服务。系统定义的访问控制规则是否合适主要体现在两个方 面：第一，该规则必须提供用户足够的权限去执行他们的动作以达到他们合法的 目的。第二，该规则也应该禁止恶意目标的完成。 随着现代通信技术日新月异，用户利用移动终端可以在任何时间、任何地点 使用网络信息和服务，而无线定位技术的发展为这种需求提供了可能性，尤其是 全球定位系统g p s 的出现使得定位精度得到了大幅度的提高，由此导致对基于 用户位置服务l lj 和移动应用的需求也相应的增加，为了满足上述需求，越来越多 的人开始研究基于位置的服务。基于位置的服务是i t 服务中的重要内容，它根 据用户当前的位置信息及用户的权限范围向用户提供经过搜集、整理、过滤过的 信息。它提供服务时必须依据用户当前所处的位置、信息或数据存储的位置等因 素，做出是否向该用户提供信息服务的决策，并进行相应的后续操作。在基于用 户位置的信息服务系统中，用户对信息的处理权限往往是和用户发出信息处理请 求时的位置有关，是动态变化的，而不仅仅和用户的职责有关。因此，必须研究 基于移动用户位置的访问控制模型。 在空间环境下，角色所具有权限的施用受到角色作用域的制约。只有当用户 当前所处的空间位置在其所扮演角色的空间作用域范围内才能被授予对客体的 操作权限。系统在进行访问控制决策时必须根据客体和用户的空间位置来授予或 取消权限。将现有的基于角色访问控制模型应用到空间数据的访问控制时，必须 对其进行改进，增加对空间数据安全特性的支持【2 ，3 一，以适应空间数据库中用户 权限与其所处空间位置之间的映射关系。 研究带有空间特性访问控制系统规则可以防止由于用户位置改变而带来的 可能产生漏洞的危险授权。以一个康复医疗机构中职员和病人的移动应用为例， 授予这些人个基于地理位置的终端，他们可以使用这些终端获得由应用服务器 江苏大学硕士学位论文 提供的信息服务，由具有不同功能的角色个体构成，比如护士、医生和病人等。 可以发现，根据角色功能的不同，用户所获得的服务是不同的。如：为护士所提 供的服务可能就和给医生的不同，这个不是简译的因为个人偏好而主要是结构和 功能所决定的。我们规定护士权限只能在规定科室内获得，以防止病人信息的泄 露，如果在权限授予过程中，护士的地理位置移动没有被考虑，那么内科的护士 就可能读取外科病人的资料，这样就产生了信息的不安全泄露。为了保证系统的 安全性，需要研究在规则提供权限下恶意目标是否可以完成，如果可以完成，则 说明系统违反了相应的约束，无法满足一定的安全要求。 在以往的研究注重空间访问控制系统规则的定义及建模，这有助于空间访问 控制系统建立初期错误的避免，但是即使建立了正确的模型，在实际的应用中也 难免出现错误，这给空间访问控制系统的安全带来了很大的隐患，这就需要有一 个合适的方法针对具体的空间访问控制系统规则进行检测，排除实际应用中的规 则错误。由于访问控制系统规则集的复杂性，无法使用手动方法进行规则检测， 寻求自动工具的检测方法已成为必然需求。目前，对自动工具的研究方法已受到 研究者的广泛关注，虽然已提出一些设想，比如使用p e t r i 网的方法、使用模型 检测的方法等等，但这方面的研究还处于初始阶段，没有成熟的研究成果。模型 检测具有强大的时态逻辑推理能力，模型检测方法是目前流行的一种系统验证方 法，通过对系统状态的搜索，可验证表示属性的逻辑表达式在系统运行中是否成 立。目前模型检测主要应用在计算机硬件、安全认证协议、访问控制系统等方面 的分析与验证中。因此本文决定采用模型检测的方法对空间访问控制系统规则的 验证做一些探索工作，增加系统的安全性能。 1 2 国内外发展现状 国际上对数据库安全研究起步较早，也积累了丰富的理论经验。早期b e l l 和l a p a d u l a 对信息安全进行大量的基础性研究，提出多种系统安全模型【5 j ，并在 多个系统中得以实现。美国国防部于1 9 8 5 年公布了世界上第一个计算机系统安 全评估标准t c s e c l 6 ( n - - 信计算机安全评估标准) ，之后又公布了t d i ( 可信数据库 管理系统解释) ，这也是目前国际上比较通用的标准。我国于1 9 9 9 年制定了计 算机信息系统安全保护等级准则( g b1 7 8 5 9 1 9 9 9 ) ，目前我国数据库安全的研 究均参照了这些标准进行研制。国内为了解决使用广泛的c 级数据库管理系统 的安全问题，一些数据库安全研究人员通过开发成本低、见效快的的应用程序方 江苏大学硕士学位论文 法实施对数据库的访问控制【_ 7 1 ，这具有一定的可行性。 当前对数据库安全技术的研究主要是围绕关系数据库系统中的访问控制模 型【8 】展开的，主要集中在自主访问控制( d a c ) 、强制访问控制( m a c ) 及基于角色 访问控制( r b a c ) 三个方面。 基于角色的访问控n ( m 3 a c ) 是一种经典的访问控制模型，对r b a c 的研究成 果9 ，1 0 , 1 1 , 1 2 】也比较多。它模拟了现实生活中权限与岗位相关联的实际情况，通过 一定的角色分配规则给用户分配或取消角色来完成对用户权限的授予或回收。安 全管理人员可以根据需要在系统中定义多个角色，并为这些角色设置合适的访问 权限，而用户根据其职责再被指派为不同的角色，从而实现了用户与访问权限的 逻辑分离( 见图1 1 ) ，提高了安全管理的效率。 图1 1r b a c 的授权方式 由于访问控制系统的复杂性使得手动进行规则检测变得几乎不可能，现在研 究者总是倾向于借助工具来进行系统规则的检测。 f i s l e r 和k r i s h n a m u r t h i 等人建立了一个用来分析访问控制规则的软件 m a r g r a v e l l5 1 。m a r g r a v e 并没有执行模型检测，它仅仅是简单的遍历了描述规则的 m t b d d ，使用输入的查询中提供的信息并观察得到的结果，并以此证明一个规 则是否满足某种属性。m a r g r a v e 仅仅是针对单个规则进行检测，而现实系统中往 往是授权规则集合共同起作用。 s c h a a d 和m o f f e t t 使模型a l l o y 明确说明了r b a c 系统模型【1 7 1 ，a r b a c 9 7 系统扩充和责任分离特性【l 踟。然而由于a l l o y 无法进行时态逻辑推理，如果使用 a l l o y ，就需要硬编码系统状态，这会使得检测工作变得非常复杂。 s h a a d 和l ix i a o o u 提出了使用p e t r in e t 的方法检测e c a ( e v e n tc o n d i t i o n 江苏大学硕士学位论文 a c t i o n ) 主动规则【1 9 】，并建立了一个用来分析规则的工具c c p n ( c o n d i t i o nc o l o r e d p e t r in e t ) 1 2 m ，这个工具仅仅是应用在主动规则上面，并不适应所有空间访问控 制系统规则的检测。 z h a n gn a n 和r y a nm a r k l 2 h 提出了基于模型检测的访问控制系统规则检测方 法，开发了一个规则检测工具a c p e g l 2 2 1 ，a c p e g 使用r w 语言描述系统规则 以及待验证的属性，解决了先前工作所忽视的规则间相互作用，用户间的合作及 多步执行带来的安全漏洞问题。但这些工作都没有涉及带有空问特性的访问控制 系统规则的验证。由于a c p e g 的源代码在网上已经给出，可通过加入合适的空 间信息判断接口，使其适应空间访问控制系统规则验证的要求。 1 3 本文的主要工作 s p a t i a l r b a c l 2 3 1 模型是一个增强的带有空间特性的r b a c 模型，这个模型 给出了空间访问控制系统为了保证一定的安全特性需要满足的一些空间约束，包 括空间区域约束，空间角色激活基数约束和空间职责分离约束。通过对空间访问 控制系统授权规则的验证，可以判断这个系统是否满足s p a t i a l r b a c 模型给定 的的约束条件。本文主要解决以下几个问题： ( 1 ) 空间访问控制系统规则的表示方法。由于空间访问控制系统的发展，其 规则也日益复杂。如何对其正确规范地描述是设计验证方法的基础。由于系统的 空间特性带来了空间信息处理的难题，需要给出相应的映射方法将空间信息进行 转化，这对整个系统的正确描述也带来了一定困难。 ( 2 ) s p a t i a l r b a c 模型中空间区域约束、空间角色激活基数约束以及空间职责 分离约束属性需要转化为模型检测范畴的检测目标，这样才能确定算法的输出结 果。通过对约束属性的描述，建立空间访问控制系统的状态空间，设计相应的模 型检测算法，找出违反约束的相应目标需要执行的操作序列，从而设计出完整的 空间访问控制系统规则的验证方法。因为所选课题与实际应用有关，还需要给出 对验证方法正确性和有效性的必要的证明和分析。 ( 3 ) 为了实现空间访问控制系统规则验证方法的实现，需要设计相应的验证 工具。本文考虑在原有的模型检测工具a c p e g 的基础上加入空间区域信息处理 机制，使其满足空间访问控制系统规则验证的需要。 江苏大学硕士学位论文 1 4 本文的组织结构 本文主要分为六章，其主要内容安排如下： 第一章主要介绍课题的研究背景和意义、空问数据库以及访问控制系统规则 验证方面的国内外研究现状，并对其加以分析和比较，最后阐述本文的主要研究 工作。 第二章介绍访问控制系统的相关背景知识。主要包括访问控制系统的模型及 带有空问特性的角色访问控制系统s p a t i a l r b a c 模型，最后对目前已有的访问 控制系统规则验证的方法进行分析，阐述了本文选择模型检测的依据。 第三章提出基于谓词逻辑的空间访问控制系统的描述方法。在这个方法中， 系统由谓词及规则共同组成，空间类中对象的性质及关系表示成谓词的形式，系 统根据谓词逻辑运算的结果为用户分配相应权限，将空间信息作为系统授权的参 数之一，简化了空间访问控制系统的规则表示。最后对这种表示方法进行分析， 阐述其优势。 第四章给出s p a t i a l r b a c 模型中三种空间约束属性的统一表示形式，并提 出针对前一章中描述的系统进行验证的模型检测算法，通过算法的执行，查询给 定系统违反上述三种空间约束属性的恶意目标是否可以完成。 第五章在已有的模型检测工具a c p e g 的基础上加入空问区域信息处理机 制，修改检测算法对应的源代码，并通过一个实例进行分析研究，验证规则验证 方法正确性及有效性，并给出算法在不同规模系统中运行的时空消耗。 第六章总结全文工作，指出本文工作的不足并对下一步工作进行展望。 江苏大学硕士学位论文 第二章空间访问控制系统与模型检测技术分析 2 1 访问控制系统的模型 访问控制技术是信息安全的重要保障措施之一，已经经历了二十多年的发 展。目前主要的访问控制模型【2 4 】包括：自主访问控制、强制访问控制和基于角色 的访问控制。 ( 1 ) 自主访问控制 自主访问控带l j ( d i s c r e t i o n a r ya c c e s sc o n t r o l ，d a c ) 是最常用的一种访问控制 机制。它是根据自主访问控制策略建立的一种模型，允许合法用户以用户或用户 组的身份访问策略规定的客体，同时阻止非授权用户访问客体，某些用户还可以 自主地把自己所拥有的客体的访问权限授予其他用户。自主访问控制在实现上， 首先要对用户的身份进行鉴别，然后才可以按照访问控制列表所赋予用户的权 限，允许和限制用户使用客体的资源。主体控制权限的修改通常由特权用户( 管 理员) 或是特权用户组实现。d a c 采用访问控制列表( a c l ) 方式，客体访问控制 信息存取自由、灵活，广泛应用于商业和工业环境中，但是由于用户可以任意传 递权限，没有访问文件( f i l e l ) 权限的用户a 能够从有访问权限的用户b 那里得到 访问权限或是直接获得文件，d a c 模型提供的安全防护还是相对比较低的，不 能给系统提供充分的数据保护。 ( 2 ) 强制访问控制 强制访问控$ 1 j ( m a n d a t o r y a c c e s sc o n t r o l ，m a c ) 是指将系统中的每个主体和 客体赋予相应的安全级别，当主体访问客体时调用强制访问控制机制，根据主体 的安全级别和访问方式，比较主体的安全级别和客体的安全级别，从而确定是否 允许主体对客体的访问。强制访问控制提供了基于标识的高级安全认证，可以避 免和防止大多数有意无意的对数据库的侵害，主要用于多级安全级别的军事应用 中。但是强制访问控制太严格，以至在某些应用环境下不能用，而且主、客体安 全级别的划分与现实要求无法保持一致，在同级别间缺乏控制机制。 ( 3 ) 基于角色的访问控制 基于角色的访问控f l ；l j ( r o l e b a s e da c c e s sc o n r t o l ，r b a c ) 将角色的概念引入 访问控制，大大简化了授权管理的方法，也大大提高了管理的效率，它支持最小 江苏大学硕士学位论文 特权、责任分离以及数据抽象三个基本的安全原则。r b a c 始于2 0 世纪7 0 年代， 到了9 0 年代开始兴起。由于计算机系统已发展到以多应用和服务于多用户为特 征，并己普及应用到各行各业中，与应用领域有关的安全需求大量涌现，访问控 制要求立足于单位或部门的网络来设计和实施，甚至还要考虑其丌放性，以便于 协作单位间的系统互连。传统的访问控制技术已不能满足需要，基于角色的访问 控制技术得到推崇，成为当前比较流行的访问控制技术。 r b a c 是目前公认的解决大型企业统一资源访问控制的有效方法【2 ”。虽然 r b a c 有诸多优点，对其研究也相当广泛和深入，但仍有一些应用是现有r b a c 模型所不能描述的，比如某些应用中需要用空间约束来限制资源的使用。在目前 的空间数据库应用中，将r b a c 和空间信息相结合的空间访问控制系统的应用 也越来越多。f r o d e 等人基于无线通讯网开发了一个带有空问特性的角色访问控 制系统模型1 3 l ，但仅简单地提出了带有空间特性的职责分离约束，并没有对授权 约束、会话状态变化规律以及带有空问特性的角色继承机制进行深入研究。e l i s a b e r t i n o 等人提出了著名的g e o r b a c l m 】模型，它扩展了传统的r b a c 模型以用 于处理空间和基于地理位置的数据信息的访问控制，采用空间实体来表示客体、 用户的地理位置，以及受地理位置约束的角色。用户所具有的角色是否被激活取 决于用户所在的地理位置。同时，为了使模型具有灵活性和可重用性，在 g e o r b a c 模型中引入了角色模式( r o l es c h e m a ) 的概念，它包括角色名字、角色 空间有效作用域的类型、逻辑位置的粒度等，但对于角色的空间约束规则并没有 进行充分的研究。 2 2 带空间特性角色访问控制系统模型 由于无线网络的快速发展加上位置定位设备精确度的不断提高，带有空间特 性的计算机应用逐步展开。空间感知的访问控制系统可用于以下一些情况：( 1 ) 用户只希望某些人在办公室内使用一些设备，如打印机等；( 2 ) 一些公司基于安 全的考虑只希望用户在特定的办公室内获得一定的资源；( 3 ) 一些重要的信息不 能同时由一个用户获得等。为了使空间访问控制系统能够满足上述要求，需要提 出一个支持空间能力的访问控制系统。在位置感知的应用程序中，用户经常被分 为不同类别，因此，在r b a c 基础上进行空间特性的扩充是个合理的选择。虽 然目前已经出现了许多支持空间和基于位置的访问控制技术或限制上下文感知 的访问控制模型，但不能完全满足目前实际应用中的安全需要。 江苏大学硕士学位论文 在将现有的r b a c 模型应用到对空间数据的访问控制时，需要对现有的基 于角色的访问控制模型进行改进，增加对空间数据的安全特性支持，以适应空间 数据库中用户权限与其所处空间位置之间的映射关系。例如，在某些环境下，用 户对信息的访问请求会随用户位置变化而变化，这是因为由于用户所处空间位置 的不同，导致他所扮演的角色不同，就拥有不同的访问权限。确切的说，在空间 数据处理系统中，权限授予给角色，而且角色所具有的权限的施用受到角色作用 域的制约。用户属于空间数据处理系统预先定义好的范畴，只有当用户所处的当 前所处空间位置在其所扮演角色的空间作用域范围内才能被授予对客体的操作 权限。系统在进行访问控制决策时必须根据客体和用户的空间位置来授予或取消 权限。例如，在一个银行客户访问控制系统中，客户扮演一个角色，该角色具有 打开用户保险柜的权限。事实上，用户必须在保险柜附近，同时必须是银行上班 时间才能打开这个保险柜。这种情况下，激活这个角色的约束条件就是“银行上 班时间”和“用户在这个保险柜附近”。 本文对空间访问控制系统的规则进行检测，检测的目的是使系统规则满足一 定的约束，从而使系统达到预定的安全要求。因此，选定一个合理、有效的空间 访问控制系统模型对安全方面的研究十分必要，该模型必须可以提供完整的约束 集保证现实应用中的安全需求【3 5 1 。 2 2 1s p a t i a l - r b a c 模型 带有空间特性的角色访问控制系统s p a t i a l r b a c i ：2 3 】模型是本课题组之前的 研究成果。随着r b a c 应用的进一步深入，相当多的领域提出了空间特性的要求。 在有些环境下，用户访问请求会随用户位置变化而变化，通常由于用户所处位置 的不同，他所扮演的角色也有可能不同，而且也可能拥有不同的访问权限【 4 0 , 4 1 1 。 基于这个要求提出的s p a t i a l r b a c 模型通过引入空间对象、空间位置等元素，使 一个角色在不同空间位置上具有不同权限。 设u = u l ，u 2 ，a m ) 是所有用户的集合；r - - r i ，r 2 ，r n ) 是所有角色的集合； o b = o b l ! , o b 2 ，, o b k 是所有空间对象的集合；o p = o p l ! , o p 2 ，o p t 是所有操作的集 合；s = s i ，s 2 ，s p 是所有会话的集合；c = c i ，c 2 ，c t ) 是所有约束规则的集合； p _ - 2 0 p 0 b 是所有权限的集合；l o c = l o c l ，l o c 2 , ，l o e , p ) 是空间对象所处空间位置 的集合，l o c 表示由平面坐标系中的所有坐标数据序偶 构成的点集。 u a ( u x l o c x r ) c 从用户集到角色集的多对多映射，表示用户u 在特定的 江苏大学硕士学位论文 空间位置l o c 被分配角色r ，且满足约束规则c ； p a ( p l o c r ) c从权限集到角色集的多对多映射，表示角色r 在特定的 空m 位置l o c 被授予权限p ，且满足约束规则c ； s = 会话s 是指用户与系统进行的一次 交互。会话用7 元组来描述，其中u 、r 、u a 和p a 分别表示该会话所允许的用户、 角色、用户角色的映射关系和角色权限映射关系，c 表示该会话在运行时必须满 足的约束规则，c h a n g e p o s i t i o n 表示会话状态发生变化时的空间位置，t a s k 表示 会话需完成的一系列操作，操作是指系统根据用户的任务要求所执行的一条指 令。 o p c - r x s = a s s i g n _ u ( u ，r , l o c ) u n a s s i g n _ u ( u ，r , l o c ) 操作，分配取消用户u 在空间位置l o c 的角色r ； a u t h o r i z e _ r ( r ，p ，l o c ) u n a u t h o r i z e r ( r ，p ，l o c ) 操作，授予收回角色r 在空间位置 l o c 的权限p ； e n a b l e r ( r ，l o c ) d i s a b l e _ r ( r , l o c ) 操作，使角色在空间位置l o c 有效无效； a c t i v a t e r ( u ，r ，l o c ) d e a c t i v a t e r ( u ，r ，l o c ) 操作，用户u 在空间位置l o c 激活 不激活角色r ； ) 2 2 2s p a t i a l r b a c 空间约束 在带有空间约束的系统中，导致冲突的原因主要有两个：( 1 ) 角色的语义；( 2 ) 角色获得的授权超出了角色发挥作用的空间范围。 在s p a t i a l 。r b a c 模型中，针对一个空间对象区域特征，约束被分为三大类： 空间区域约束、空间角色激活基数约束以及空间职责分离约束。这三种类型的约 束较全面地反映了一个角色在区域特征维度上的访问控制规则的安全要求。 ( 1 ) 空间区域约束 二维区域的形状是多种多样的，可以是规则的几何形状，也可以是不规则的 任意图形，考虑到r 树中叶结点的边界框是包含叶结点中的所有空间对象的最小 外包矩形，s p a t i a l r b a c 模型使用最小外包矩形来表示这个区域。 定义2 1 空间区域约束记为( l s ，s ) ，用来表示在指定空间区域范围l s 内，能 否给用户分配角色，或给角色授予权限，或改变角色状态，即进行一次会话s 。 江苏大学硕士学位论文 ( 2 ) 空间角色激活基数约束 s p a t i a l r b a c 模型中引入了角色状态的概念。角色可以拥有以下四种状态之 一：有效( e n a b l e d ) 、无效( d i s a b l e d ) 、激活( a c t i v a t e d ) 、去除激活( d e a c t i v a t e d ) 。角 色处于无效状态表明该角色不可以在任何用户的会话中使用，即用户无法获得与 该角色相关联的权限。一个处于无效状态的角色可以在某些情况下转为有效。角 色处于有效状态表明该角色可被那些扮演该角色且其空间位置在本角色作用域 的用户激活，从而行使相应权限。若有一个用户激活了某个角色，那么该角色的 状态就变为激活状态。一个角色处于激活状态意味着至少有一个用户激活了这个 角色。当某一角色处于激活状态，并发生了去除激活事件，这时如果仅有一个会 话使用到该角色，那么该角色转为无效状态，否则，该角色仍然保持激活状态。 处于有效或者激活状态的角色，可在无效事件的影响下，转为无效状态。 另外，出于安全考虑，在s p a t i a l r b a c d p ，系统管理员一旦发现有不法用户 在恶意破坏系统，即使该用户扮演的角色集合处在有效或激活状态，管理员仍可 以执行无效事件，强行使分配给该用户的角色无效来阻止破坏，保证安全性。 定义2 2 角色激活基数约束( r a a r e a ) 记为o ( l s ，m a x r , s ( a c t i v a t e r ( r ，l s ) ) ) ，其 中，l s = 表示空间区域，a c t i v a t er ( r ，l s ) 表示在该空间区域内角色r 被激活， m a x r 为角色最大数目约束。其形式化表示为：v r i e r ，v l s j e l s ，j m a x r n 01 ( l s j ，s ( a c t i v a t e _ r ( r i ，l s j ) ) ) 弋 m a x r ) 定义2 3 用户角色激活基数约束( u r a - a r e a ) 记为0 ( l s ，m a x u r , s ( a c t i v a t er ( u ，r ，l s ) ) ) ，其中，l s = l i ，l p ，a c t i v a t e _ r ( u ，r ，l s ) 表示在该空间区域内用户u 激活 角色r ，m a x u r 为用户危色最大数目约束。其形式化表示为：v r i e r ，v u k e u ， 3l s j l s ，jm a x re n 0 2 ( l s j ，s ( a c t i v a t e r ( u k ，r i ，l s j ) ) ) 弋 m a x u r 角色最大数目约束( m a x r ) 限制在一个特定空间区域内，一个角色激活基数 的最大上限，不管用户是否是在不同会话或是由不同用户激活角色r 。用户角色 最大数目约束( m a x u r ) 限制在一个特定空间区域内，一个角色被一个特定用户激 活基数的最大上限。同一角色在一个特定的空间区域内总的激活基数的最大上限 是确定的。同一个角色在一个特定的空间区域内被不同用户激活基数的最大上限 不同，但是其总和应该等于此特定的空间区域内总的激活基数的最大上限，即： m a x r = m a x u i r ，( i = 1 , - - - - , n ) 其中，n 是这个区域内激活该角色，的用户数。 江苏大学硕士学位论文 约束m a 殄约l 束5 m a x u r l 3 厂7f ，、 l 2 l 6 l l 0 x ix 2x 3 x 4x 5 x 6x 图2 1 空间角色激活基数约束 在图2 1 中，在区域 和 内，角色r 是有效状态，在特定的空间区域 用户建立一个会话，与这 个会话相关的角色最大数目约束( m a x r ) 被触发，约束在 区 域内有效，而在这个区域内的非阴影部分角色，- 是无效状态。这个约束说明在 区域两个阴影部分内，总的用户激活角色，的基数不能超过 m a x r ，同一个用户激活角色，的基数不能超过m a x u r 。 角色最大数目约束的作用是将某一特定空间区域内激活角色的总次数限定 在某个阈值之内。当一个或多个用户用完了指定的角色激活次数后，此角色将不 能再被激活，即使该角色仍处于有效状态。值得注意的是，角色最大数目约束有 可能跨越角色有效的几个不同的空间区域。图2 1 中， 和 就是角色有效的两个不同区域。控制一个角色被激活基数 对保证系统安全有着至关重要的作用。例如，假设规定在某一个特定的空间位置 角色r 被激活的最大基数为5 ，而在这个位置有7 个会话要求激活角色r ，不管是由 一个用户或是多个用户发出，其中2 个会话要被阻塞。 ( 3 ) 空问职责分离约束 传统的r b a c 模型中引入职责分离( s o d ) 规则是为了防止授权冲突，主要是 因为在实际的应用场合中通常需要由不同的人来行使不同的职责，达到相互牵制 的目的。例如，在企业中，某个职工报销差旅费时，必须先由主管领导签字，然 后再由出纳支付。显然职责分离对保护信息安全至关重要，s p a t i a l r b a c 模型对 描述和执行这样的策略非常方便。角色互斥约束是根据用户角色分配集或者以在 用户会话中激活的角色集判断的，s o d 规则可以被定义为静态的职责分离约束 ( s s o d ) 和动态的职责分离( d s o d ) 规则。 y w ” 江苏大学硕士学位论文 s p a c i a l r b a c 模型将传统r b a c 模型中的s o d 进行了扩展，分为空间静态 职责分离约束( s s s o d ) 和空间动态职责分离约束( s d s o d ) 。例如，考虑两个角色， 医生和护士，他们定义在医院这个范围中。不失一般性，假定同一个人不能够在 两个不同的地方( 例如不同的医院里) 被分配具有医生的角色；同样地，一个人不 能在一个医院内同时担任医生和护士两个角色。在后一种情况中，一个人能否扮 演医生或护士的角色受到其所处的空间位置的制约，只有当其所处的位置和其所 扮演的角色的作用域时候满足包含关系的时候才能够行使所扮演的角色的权限。 s p a c i a l r b a c 模型对空间约束的精确定义可大大提高空间访问控制系统的 安全性。满足上述三类要求的系统我们就认为是相对安全的。因此，在为空间访 问控制系统设计规则时，必须确保设计的系统满足这些约束属性的要求，这就需 要对规则进行检测，保证设计的可靠性。 2 3 访问控制系统的安全需求 在信息技术高速发展的今天，访问控制技术在信息安全中的作用也显得越来 越重要，要确保一个访问控制系统安全有效还必须保证该访问控制系统规则的可 靠。长期以来，大量的研究工作都忽略了对规则之间相互作用的考虑，这很有可 能导致在用户合作或多步操作的过程中产生安全漏洞。因此需要采取必要的检测 方法来确保规则的正确定义。访问控制规则间的正确合理性主要体现在两个方 面：第一，规则必须提供用户足够的权限去执行合法动作；第二，规则之间还要 确保不能执行恶意操作。由于访问控制系统规则集的复杂性，无法使用手动方法 进行规则检测，目前主要还是偏向于使用工具的方法来检测访问控制系统规则的 合理性和安全性【2 6 1 。 2 4 访问控制系统规则检测方法 近几年来，访问控制系统规则的自动检测技术【2 7 1 引起了许多学者的广泛关 注。主要的检测方法可以分为以下几种： ( 1 ) 基于测试的