（计算机科学与技术专业论文）基于角色访问控制系统的安全授权分析与验证.pdf

删 a n a l y s i sa n dv e r i f i c a t i o no fs e c u r i t ya u t h o r i z a t i o nf o rr o l eb a s e d a c c e s sc o n t r o ls y s t e m b y z h a n gh a o b e ( x i n y a n gn o r m a lu n i v e r s i t y ) 2 0 0 8 at h e s i ss u b m i t t e di np a r t i a ls a t i s f a c t i o no ft h e r e q u i r e m e n t sf o rt h ed e g r e eo f m a s t e ro f e n g i n e e r i n g c o m p u t e rs c i e n c ea n dt e c h n o l o g y i nt h e g r a d u a t es c h o o l o f h u n a nu n i v e r s i t y s u p e r v i s o r a s s o c i a t ep r o f e s s o rs u nj i a n h u a m a y , 2 0 1 1 湖南大学 学位论文原创性声明 本人郑重声明：所呈交的论文是本人在导师的指导下独立进行研究所取 得的研究成果。除了文中特别加以标注引用的内容外，本论文不包含任何 其他个人或集体已经发表或撰写的成果作品。对本文的研究做出重要贡献 的个人和集体，均已在文中以明确方式标明。本人完全意识到本声明的法 律后果由本人承担。 作者签名：弓艮炙 b 期：泸f 年乡具弓1 日 学位论文版权使用授权书 本学位论文作者完全了解学校有关保留、使用学位论文的规定，同意学 校保留并向国家有关部门或机构送交论文的复印件和电子版，允许论文被 查阅和借阅。本人授权湖南大学可以将本学位论文的全部或部分内容编入 有关数据库进行检索，可以采用影印、缩印或扫描等复制手段保存和汇编 本学位论文。 本学位论文属于 l 、保密口，在年解密后适用本授权书。 2 、不保密团。 ( 请在以上相应方框内打“”) 纂曩瀚 导师签名：扪瞧邵 b 瓤：沙i 年爹只；日 日期： 沪，年夕月 纠日 基于角色访问控制系统的安伞授权分析与验证 摘要 访问控制通过对用户访问系统资源进行安全控制来保护系统资源。基于角色 的访问控制模型适合对各种访问控制需求进行建模而且能够简化访问控制管理， 基于角色的访问控制模型作为一种授权模型已经广泛用于商业应用系统。 由于访问控制模型及其扩展模型有许多约束，而这些约束由于相互影响可能 会产生冲突，因此通过验证访问控制模型来避免访问控制漏洞具有重要作用。传 统的访问控制模型验证方法针对独立的访问控制模型，能够发现访问控制模型内 部不同约束之间的可能潜在冲突。但是传统模型验证方法没有考虑实际系统，由 于访问控制系统的安全不仅与访问控制模型有关，还与系统的授权约束相关。因 此，对访问控制系统的授权约束进行安全性验证具有重要意义。 针对上述问题，本文提出一种基于角色访问控制系统的安全授权验证方法。 首先，利用形式化规范语言来描述访问控制系统及其授权约束，包括用统一建模 语言( u n i f i e dm o d e l i n gl a n g u a g e ，u m l ) 类图表示访问控制模型，用对象约束语言 ( 0 b j e c tc o n s t r a i n tl a n g u a g e ，o c l ) 描述访问控制系统的授权约束；然后，利用 模型驱动架构实现u m l 模型到形式化模型的转换；最后，利用形式化验证方法对 系统的授权约束进行安全性验证。 本文最后选取一个基于角色访问控制系统进行实例验证，实验表明针对基于 角色访问控制系统的授权约束，该方法能够进行有效的安全性验证。 关键词：r b a c ；u m l ；o c l ：授权约束；形式化验证 i i a b s t r a c t a c c e s sc o n t r o lp r o t e c tt h er e s o u r c e so fa no r g a n i z a t i o nb yc o n t r o l l i n gw h oh a s a c c e s st ow h a to b j e c t s r o l eb a s e da c c e s sc o n t r o lh a sb e c o m et h ed e f a c t oa u t h o r i z a t i o n m o d e l su s e db yc o m m e r c i a la p p l i c a t i o n sw i d e l yb e c a u s ei tc a nm o d e lv a r i o u sa c c e s s c o n t r o lr e q u i r e m e n t sa n di ts i m p l i f i e sa c c e s sc o n t r o lm a n a g e m e n t a c c e s sc o n t r o la n di t se x t e n s i o n sh a v ev a r i o u sc o n s t r a i n t st h a tm a yi n t e r a c tw i t h e a c ho t h e rr e s u l t i n gi nc o n f l i c t s t h u s ，i ti si m p o r t a n tt oe n s u r et h a ta c c e s sc o n t r o l b r e a c h e sd on o to c c u rb yv e r i f y i n gt h ea c c e s sc o n t r o lm o d e l t r a d i t i o n a la c c e s sc o n t r o l m o d e lv a l i d a t i o nm e t h o d sf o c u so na n a l y z i n gt h ea c c e s sc o n t r o lm o d e li ni s o l a t i o n a n da r eu s e f u li nd e s c r i b i n gp o t e n t i a lc o n f l i c t st h a tm a yo c c u rb e t w e e nt h ed i f f e r e n t f e a t u r e so ft h em o d e l s u c ha n a l y s i si si n d e p e n d e n to ft h ea p p l i c a t i o n h o w e v e r ，t h e s 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 mi s n o to n l yr e l e r a n tw i t ht h ea c c e s sc o n t r o l m o d e l b u ta l s oa s s o c i a t e dw i t ht h ea u t h o r i z a t i o nr u l e s s oi ti si m p o r t a n tt oa n a l y z et h e s e c u r i t yo ft h ea u t h o r i z a t i o nc o n s t r a i n t so ft h ea c c e s sc o n t r 0 1s y s t e m t h e r e f o r e ，w ep r o p o s eav e r i f i c a t i o nm e t h o do fs e c u r i t ya u t h o r i z a t i o nf o rr b a c s y s t e m f i r s t ，t h i sa p p r o a c hs p e c i f i e s t h er b a cs y s t e ma n dt h e i r a u t h o r i z a t i o n c o n s t r a i n t si naf o r m a ls p e c i f i c a t i o nl a n g u a g e i ts p e c i f i e st h ee n t i t i e st h a tt a k ep a r ti n t h ea c c e s sc o n t r o lm o d e li nt h ef o r mo ft h ec l a s sd i a g r a m sa n du s e do c l s t a t e m e n t st o s p e c i f yt h ea u t h o r i z a t i o nc o n s t r a i n t s t h e n i tt r a n s f o r m st h e s ec l a s sd i a g r a m sa n d c o n s t r a i n ts t a t e m e n t st oaf o r m a lm o d e l f o rt h el a s t s t e p ，i tu s e st h ef o r m a l v e r i f i c a t i o nt ov e r i f yt h es e c u r i t yo ft h ea u t h o r i z a t i o nc o n s t r a i n t s f i n a l l y ，w e i l l u s t r a t e o u r a p p r o a c hu s i n g ar e a l w o r l dr b a c s y s t e m e x p e r i m e n t ss h o wt h a ti t c a nv e r i f yt h es e c u r i t yo ft h ea u t h o r i z a t i o nc o n s t r a i n t sf o r r b a cs y s t e me f f e c t i v e l y k e yw o r d s ：r b a c ；u m l ；o c l ；a u t h o r i z a t i o nc o n s t r a i n t s ；f o r m a lv e r i f i c a t i o n i i i 基于角色访问控制系统的安令授权分析0 验证 目录 学位论文原创性声明和学位论文版权使用授权书i 摘要i i a b s t r a c t i i i 插图索引v i 附表索引一v i i 第1 章绪论1 1 1 课题背景与意义一1 1 2 相关研究现状1 1 3 论文研究内容6 1 4 论文组织结构6 第2 章相关技术7 2 1 访问控制7 2 1 。1 基本概念7 2 1 2 基于角色的访问控制8 2 2 面向对象建模1o 2 2 1 统一建模语言l0 2 2 2 对象约束语言1 1 2 3 形式化验证技术1 3 2 3 1 理论证明1 3 2 3 2 模型检测1 4 2 4 基于a l l o y 的模型验证技术。1 5 2 4 1 a l l o y 简介15 2 4 2 与其它形式化验证方法的比较1 7 2 5 小结18 第3 章基于角色访问控制系统的安全授权分析与验证1 9 3 1 安全授权分析一1 9 3 1 1 授权状态空间1 9 3 1 2 弱约束和强约束2 0 3 2 安全授权验证一2 2 3 3 基于角色访问控制系统的u m l 模型2 3 3 3 1 系统模型的u m l 表示2 3 i v 硕l j 学位论文 3 3 2 授权约束的o c l 表示2 4 3 4 u m l 到a l l o y 的模型转换一2 7 3 5 基于a l l o y 的安全授权约束验证2 9 3 5 1 安全授权约束2 9 3 5 2 基于a l l o y 的模型约束验证3 l 3 5 3 验证弱约束3 1 3 5 4 验证强约束一3 2 3 6 小结3 3 第4 章实验分析3 4 4 1 实验环境3 4 4 1 1 硬件环境3 4 4 1 2 软件环境3 4 4 2 授权约束的安全性验证3 4 4 2 1 系统的授权需求分析3 4 4 2 2 访问控制系统的u m l 和o c l 表示3 6 4 2 3 模型转换3 8 4 2 4 安全性验证4 0 4 3 小结4 2 结论4 3 参考文献4 5 致 射4 9 附录a 攻读硕士学位期间所发表的学术论文5 0 附录b 攻读硕士学位期间所参与的项目5 1 v 綦于角也访问控制系统的安全授权分析，j 验证 插图索引 2 1 访问控制模型基本组成7 2 2r b a c 的基本思想8 2 3n i s tr b a c 参考模型一9 2 4p e r s o n 类11 2 5 二元关联ll 2 6p l a y e r 类的不变量示意图1l 2 7r o o m 类的不变量示意图1 5 2 8a l l o y 软件框架1 6 3 1 弱约束2 1 3 2 强约束2 1 3 3 授权约束验证框架图2 2 3 4r b a c 的类图模板一2 4 3 5u m l 2 a l l o y 结构图2 7 3 6 基于m d a 的模型转换2 8 3 7u m l 2 a l l o y 的模型转换框架2 8 3 8 弱约束验证3 2 3 9 强约束验证3 3 4 1 银行数据库系统中角色继承关系图3 6 4 2 银行数据库系统的u m l 类图：3 7 4 3 检测弱约束结果4 l 4 4 检测强约束结果4 1 v i 图图图图图图图图图图图图图图图图图图图图图 硕上学位论文 附表索引 表2 1 访问控制矩阵- 8 表2 2a l l o y 常用修辞词1 7 表3 1u m l o c l 的元模型元素和a l l o y 的元模型元素的对应关系2 9 表4 1 银行权限表j 3 5 表4 2 角色权限分配表3 6 表4 3 授权规则表3 6 v l i 硕十学位论文 第1 章绪论 本章首先简述了访问控制模型及其约束的安全性验证的研究背景，接着介绍 了该研究领域的研究现状，并对相关技术作简要概述，然后说明了本论文的主要 研究内容，最后简单描述了文章的框架和组织结构。 1 1 课题背景与意义 网络安全是计算机和通信领域重要的研究内容，而对网络安全控制机制的研 究是保障网络安全的基本技术。国际标准化组织( i s o ) 的网络安全标准i s 0 7 4 9 8 2 中定义了5 种层次型安全服务：身份认证服务、访问控制服务、数据保密服务、 数据完整性服务和不可否认服务。其中，访问控制是信息安全的一个重要组成部 分，是一种保护信息资源的重要机制。访问控制不仅可以保证合法用户的正常访 问行为，还能避免非授权用户的非法操作和合法用户的误操作所造成的安全问题。 因此，访问控制是保证系统安全的重要措施。 访问控制模型是一种从访问控制的角度出发，描述安全系统，建立安全模型 的方法。当前基本的访问控制模型有以下三种类型：自主访问控制( d i s c r e t i o n a r y a c c e s sc o n t r o l ，d a c ) 、强制访问控制( m a n d a t o r ya c c e s s c o n t r o l ，m a c ) 和基于角 色的访问控带t ( r o l e b a s e da c c e sc o n t r o l ，r b a c ) 。它们的基本目标都是防止非法用 户进入系统和合法用户对系统资源的非法使用。其中基于角色的访问控制模型是 当前比较成熟的访问控制模型，该模型通过引入角色概念，极大地简化了授权管 理，目前r b a c 已经广泛应用于大型政府和商业信息系统_ 中。 传统的访问控制模型安全性验证方法仅针对访问控制模型本身，通过检测访问 控制模型内部约束之间有无冲突来验证模型的安全性，虽然这种模型验证方法能够 有效地验证模型的安全性，但是这种验证方法并不适用于对基于访问控制模型的应 用系统的安全性验证，因为访问控制系统的安全性不仅与系统的访问控制模型有 关，还与系统的授权约束密切相关，访问控制系统的授权约束是否真实反映了系统 的授权期望是确定系统安全性的重要依据。只有当系统的授权约束与系统的授权期 望相一致时，才能说明系统的授权约束才是安全和有效的。因此研究基于角色访问 控制系统的安全授权验证具有重要意义，本文通过对基于角色访问控制系统的授权 约束进行安全分析与验证，保证系统得到访问控制模型的有效保证。 1 2 相关研究现状 随着访问控制模型的发展，利用形式化方法对基于访问控制模型应用系统的 基于角色访问控制系统的安全授权分析j 验证 安全性进行分析与验证已经成为保证访问控制系统安全的一种重要方法。本文研 究了几种典型的基于r b a c 模型的形式化验证方法，根据验证方法中所使用的形 式化语言不同以及有无自动化分析工具支持，本文对基于r b a c 模型的验证方法 分为以下几类分析。 1 非自动化验证方法 ( 1 ) 非图形化的验证方法 在非图形化的验证方法中，验证方法所利用的形式化语言是非图形化的，这 一类有代表性的验证方法是：文献【l 】提出的利用形式化语言z 来描述r b a c 系统， 然后结合理论证明器验证模型系统的一致性。 该方法利用基于状态的可变模型表示r b a c 模型的基本元素、约束和状态变 换。软件工具z e v e s 被用来作为建模和理论证明器。r b a c 的基于状态的可变 模型是由r b a c 模型状态以及对状态的操作集合构成。r b a c 的状态定义了 r b a c 模型的集合以及与不变量之间的关系。r b a c 的操作用来描述事件。利用 z 语言对基于r b a c 系统进行建模后，系统的状态被分为三种：起始状态、安全 状态和状态一转换。其中起始状态表示系统的开始状态，安全状态表示满足所有安 全需要的状态，状态转换表示系统状态的变化。这篇文章作者利用z 语言以及理 论证明器验证了r b a c 模型在操作a d d n e w p e r m ( r ，p ) 和a d d r s s o d ( r l ，r 2 ) 上的一致 性，这里a d d n e w p e r m ( r ，p ) 表示对角色r 授予权限p 的操作，a d d r s s o d ( r l ，r 2 ) 表 示对s s o d 关系集增加两个有静态冲突的角色。在r b a c 模型运行操作 a d d n e w p e r m ( r ，p ) 后，如果权限p 与角色r 已具有的权限没有冲突，那么权限p 将 会被授予给角色r 并且模型发生状态转变，否则模型不发生状态变化。利用模型 的安全规则可以证明r b a c 模型的状态在操作过程中保持一致。基于理论证明可 以得出当且仅当系统由安全状态开始变化并且状态变化保持与状态转换约束一 致时系统状态是安全。正如文章指出该方法有它的局限和不足：由于理论证明的 形式化语义难以理解，当利用理论证明不能证明一个理论时，很难知道具体错误 原因；由于z e v e s 证明器只能证明简单的理论，这种验证方法并不是完全自动 化。 文献 2 提出了一种基于描述逻辑的访问控制模型策略冲突检测方法。该方法 首先选择描述逻辑作为策略验证的逻辑基础，然后选取合适的策略规格模型并对 相互冲突的策略进行安全分析，最后使用推理机r a c e r 验证策略冲突。该验证方 法的具体过程：首先，利用描述逻辑表示策略中的主体、客体、动作、角色事件 和约束。在模型的策略本体中分别建立策略、授权策略、义务策略这三类概念。 其中，授权策略定义主体对客体允许不允许执行的行为。然后，根据策略冲突的 不同类型，选取合适的基于描述逻辑推理的冲突策略检测方法。策略冲突可分为： 模态冲突检测和应用相关冲突。最后，使用建模工具p r o t 6 9 6 来表示使用推理机， 2 硕二l 学位论文 同时r a c e r 实现模型策略分析和冲突检测。由于策略冲突都使用了“检测概念交 集可满足性”这一描述逻辑。由于推理机r a c e r 不能针对单独的概念，只能对整 体进行检测，从而发现不可满足的问题。该文中的策略验证方法与其它策略冲突 检测方法相比，本文利用的描述逻辑表达能力强，适合于对访问控制系统策略进 行形式化验证。 ( 2 ) 图形化的验证方法 文献 3 】提出利用角色系统的有向图来检测r b a c 模型中的多域策略冲突。在 r b a c 的多域环境中，角色映射能够保证模型中各域间的安全操作。但是由于 r b a c 模型中角色间存在层次关系以及可能存在的互斥关系，角色映射可能会产 生不同类型的策略冲突。该文章分析了三种类型的策略冲突：角色继承环冲突， 角色非关联冲突和角色职责分离冲突。在检测r b a c 模型中的多域策略冲突时， 首先需要建立角色系统的有向图，然后根据角色系统的有向图检测具体的冲突。 针对角色继承环冲突，文章提出通过检测角色系统有向图中是否存在环路来判定 有无该冲突；针对角色非关联冲突，文章提出通过检测角色系统有向图中角色间 是否存在拓扑可达性来判定有无该冲突；针对角色职责分离冲突，文章提出通过 构造有向图的邻接矩阵并查找角色连通节点来判定有无该冲突。该方法虽然能够 有效检测基于r b a c 的多域策略冲突，但是该方法没有结合一个具体的应用 r b a c 系统进行策略冲突的检测。 文献 4 】利用有向无环图( d a g ) 表示访问控制系统元素间的相互关系，将抽 象化的策略冲突检测问题转化为有向图的连通性问题，同时该文章提出了一种能 够检测策略冲突的定量方法。该验证方法的具体过程：首先，对系统的安全策略 进行定义，授权策略定义为主体可以允许或禁止的某动作。其中安全策略存在的 冲突类型有：符号冲突和内外冲突。然后，建立主体和客体关系的有向无环图模 型。具体包括主体有向无环图模型和客体有向无环图模型，前者表示用户、用户 组之间的关系，后者表示用户、角色之间的关系。最后，根据建立后的有向无环 图模型，通过在有向无环图上寻找连通节点来判断策略之间的有无符号冲突，从 而实现对安全策略的冲突检测。这种验证方法还提供了检测策略冲突的定量方法， 能够得到冲突检测复杂度。 文献【5 】提出的利用统一建模语言( u n i f i e dm o d e ll a n g u a g e ，u m l ) 和对象约 束语言( o c l ) 表示r b a c 模型及其授权约束子集。这种方法的主体思想是利用 u m l 来图形化表示r b a c 模型中的基本元素及其之间的关系，用o c l 语言表示 模型的授权约束。这种方法的优点在于能够以图形化的方式表示与r b a c 约束相 违背的授权操作。这篇文章把r b a c 模型中的授权约束分为以下三类：阻止约束、 前提约束和数值约束。阻止约束是依据权限分离原则对r b a c 模型中元素相关操 作进行限制；前提约束用来说明对r b a c 模型中元素分配操作权限时的前提要求； 3 进行标记着色p e t r i 网的模型状态表示r b a c 模型状态，弧和弧表达式用来描述 4 硕士学位论文 r b a c 模型中的各种约束。p e t r i 网中的变迁用来表示r b a c 模型中的事件集合，这 些事件包括：用户一角色的分配、角色一授权的分配等等。然后，利用着色p e t r i 网对r b a c 策略的一致性进行可达性分析。其中包括：利用事件图表示r b a c 模型 的所有状态，由于r b a c 系统的p e t r i 网是有界的，因此系统的事件图的结点个数 是有限的。该方法的不足在于：由于该验证方法采用穷举法对状态间变化进行分 析，因此该验证过程所需要的时间会呈指数式的增长。 文献 8 】提出利用着色p e t r i 网( c o l o r e dp e t r in e t ，c p n ) 对基于角色的广义时态 访问控审0 ( g e n e r a l i z e dt e m p o r a lr o l e b a s e da c c e s sc o n t r o l ，g t r b a c ) 模型i 6 】进行安 全性验证。在表示g t r b a c 的c p n 模型中，着色集合表示g t r b a c 中的基本元 素及其数据类型，元素间的关系可以用一种特定着色表示。c p n 中的控制状态用 来表示g t r b a c 模型状态，带有标签的弧用来表示g t r b a c 模型中的约束。一 旦c p n 中的标记发生改变，表示g t r b a c 模型的状态转变为不安全或不一致的 状态。c p n 模型中的转换表示g t r b a c 模型中的操作，对用户一角色分配的c p n 表示可以用来证明这种分配行为的正确性，同时这种验证方法通过利用事件图进 行可达性分析来确定违反安全性的发生。这种模型验证方法的不足之处在于：为 了使事件图具有有限的节点，c p n 模型必须被严格地限定范围；当c p n 模型中 有新的元素加入时，可达性分析的时间会呈指数式的增长。这种验证方法的另一 个不足在于c p n 模型中安全性查询语言是m l 语言，这种语言难以解释和使人理 解。 文献 9 】提出利用时间自动机( t i m e da u t o m a t a ，t a ) 对g t r b a c 1 0 】模型中的 时态因素进行验证分析。这种验证方法利用时间自动机网络模型来表示g t r b a c 系统，g t r b a c 中的初始组成元素，如角色、用户、权限等都与基于时间自动机 的状态转换系统中相应元素相对应。期望的安全属性集合被c t l 表示的安全性查 询表示，这些安全属性集合通过与u p p a a l 模型比较进行验证。这种验证方法的 不足在于：如果考虑大量的时间约束，这种验证方法将会产生“状态空间爆炸” 即产生大量的状态空间；时间自动机的结构会随着元素行为的变化而发生改变。 文献 1 1 】提出了一种结合u m l 和模型检测技术对模型进行安全性验证的方法， 该方法首先利用u m l 语言中的状态机图和类图描述安全模型，其中类图可以表示 有着状态和行为的对象，类图属性和类图间的关联可以描述状态，状态机图可以 描述状态之间转换图。然后，通过状态机图的转化实现u m l 模型到模型检测器输 入模型的转化。最后，利用模型检测器验证模型的安全性。该方法能够利用自动 化工具对模型进行安全性验证，这种方法减少了对验证人员理论过高要求和手工 推导过程。但该方法的不足在于：该安全模型验证方法只能验证单一的安全属性， 同时对模型的u m l 建模过程依赖待验证的模型的安全属性。 5 基于角色访问控制系统的安伞授权分析j 验证 1 3 论文研究内容 本文对基于角色的访问控制系统的授权约束进行安全性分析，同时提出了一 种安全授权验证方法。具体来说，本文的研究工作主要包括以下几个方面： ( 1 ) 研究已有的访问控制模型的验证方法和技术，分析它们各自的优缺点和所 存在的问题； ( 2 ) 研究面向对象建模相关技术，为基于角色访问控制系统建立u m l 模型， 具体包括使用u m l 类图表示系统的访问控制模型，利用o c l 语言描述系统的授 权约束； ( 3 ) 研究了主要的形式化验证方法，重点介绍了基于a l l o y 的形式化验证方法； ( 4 ) 将本文提出的授权约束验证方法应用于基于角色的访问控制系统中，对系 统的授权约束进行安全性分析与验证。 1 4 论文组织结构 论文各章节的内容组织安排如下： 第一章首先简要介绍本课题的研究意义和背景，针对当前应用需求提出相关 研究内容；接着，重点分析访问控制模型的安全性验证的研究现状和技术支持以 及存在的优缺点，最后列出了本文内容的具体组织结构。 第二章是介绍相关技术，首先介绍访问控制的基本概念，重点介绍基于角色 的访问控s 0 ( r o l e b a s e da c c e sc o n t r o l ，r b a c ) ；然后介绍面向对象建模技术，对统一 建模语言( u n i f i e dm o d e ll a n g u a g e ，u m l ) 和对象约束语言( o c l ) 进行详细的 介绍；最后介绍了主要的形式化验证技术，重点分析本文使用的基于a l l o y 的形 式化验证技术。 第三章详细介绍了本文提出的基于角色访问控制系统的安全授权验证方法。 首先对访问控制模型中授权约束进行安全性分析；然后提出了一种基于角色访问 控制系统的安全授权验证框架，详细介绍验证框架的具体实施；最后介绍了安全 授权验证过程所应用的相关技术。 第四章是实验分析。首先介绍实验环境，然后对其将本文提出的验证方法运 用于实际基于角色的访问控制系统中，对系统的授权约束进行安全性验证和分析。 最后，对全文所做的工作进行了总结，并指出了下一步的研究方向 6 硕一 二学位论文 2 1 访问控制 第2 章相关技术 2 1 1 基本概念 访问是使信息在主体和客体之间流动的一种交互方式。访问控制是在保障授 权用户能获取所需资源的同时拒绝非授权用户的安全机制。访问控制决定了谁能 够访问系统，能访问系统的何种资源，以及如何使用这些资源。 访问控制模型是一种从访问控制的角度出发，描述安全系统，建立安全模型 的方法。在一个计算机系统中，访问控制的基本模型如图2 1 所示。 。 图2 1 访问控制模型基本组成 当前主要的访问控制模型有以下三种类型：自主访问控制( d i s c r e t i o n a r y a c c e s sc o n t r o l ，d a c ) 、强制访问控制( m a n d a t o r ya c c e s s c o n t r o l ，m a c ) 和基于角 色的访问控$ 1 j ( r o l e b a s e da c c e sc o n t r o l ，r b a c ) 。 下面分别介绍这三种访问控制模型的核心思想及其特点如下： 1 自主访问控$ 1 j ( d a c l d a c 是在确认主体身份及其所属组的基础上，根据访问者的身份和授权来决 定访问模式，对访问进行限定的一种控制策略。 d a c 将访问规则存储在访问控制矩阵中，访问控制矩阵中的每一行表示一个 主体，每一列则表示一个受保护的客体，矩阵中的元素表示主体可以对客体的访 问权限。表2 1 为一个访问控制矩阵，由该矩阵表示可知：主体c h r i s 对客体f i l e l 具有r e a d 和w r i t e 的权限。 d a c 的优点主要体现在其自主性为用户提供了极大的灵活性，从而使其适合 于许多系统和应用。但是由于同一用户对不同的客体有不同的存取权限，不同的 7 ( 二二用户分配- ( 二二权限分配，( 二二 基于角色的访问控制( r o l e b a s e da c c e s sc o n t r o l ，r b a c ) 是由美国国家标准 化和技术委员会( n a t i o n a li n s t i t u t eo fs t a n d a r d sa n dt e c h n o l o g y ，n i s t ) 的f e r r a i o l o 8 硕士学位论文 等人在2 0 世纪9 0 年代提出的，其特有的优点引起了学术界和工业界的广泛关注， 成为研究计算机和数据库安全性的一个热点。2 0 0 1 年n i s t 发表了r b a c 标准， 该标准成为一个权威的参考规范，从而标志着r b a c 模型具有了较为正式统一的 认识【12 1 。 n i s t 标准中的r b a c 模型如图2 3 所示，n i s tr b a c 由以下四部分组成： 核心r b a c ( c o r er b a c ) 、等级r b a c ( h i e r a r c h i c a lr b a c ) 、静态职责分离( s t a t i c s e p a r a t i o no fd u t i e s ，s s d ) 和动态职责分离( d y n a m i cs e p a r a t i o no fd u t i e s ，d s d ) 【l3 1 。 图2 3n i s tr b a c 参考模型 核心r b a c 主要由基本元素、用户角色分配( u s e ra s s i g n m e n t ，u a ) 和权限角色 分配( p e r m i s s i o na s s i g n m e n t ，p a ) 组成。基本元素有以下五类：用户( u s e r s ) 、 角色( r o l e s ) 、会话( s e s s i o n s ) 、对象( o b j e c t s ) 和操作( o p s ) 。用户角 色分配是用户到角色的多对多的关系，权限角色分配是权限到角色的多对多的关 系。 等级r b a c 为模型中的角色增加了角色的层次关系，用户可以为他具有的角 色或其下级角色建立一个会话，其获取的访问权限包括在该会话中激活角色所具 有的访问权限和下级角色所具有的访问权限。 静态职责分离( s t a t i cs e p a r a t i o no f d u t i e s ，s s d ) 和动态s o d ( d y n a m i c s e p a r a t i o no fd u t i e s ，d s d ) 都是r b a c 模型中引入的约束机制，前者是指同一用 户只能被赋予冲突角色集合中至多一个角色。后者是指相互冲突的角色不能被用 户在同一会话中激活。 r b a c 最突出的优点在于系统管理员能够按照部门、企业的安全策略划分不 同的角色，执行特定的任务。一个r b a c 系统建立起来后，主要的管理工作就是 授权或取消用户的角色。用户的职责变化时，只需要改变角色即可改变用户的权 9 基于角色访问控制系统的安全授权分析与验证 当组织的功能变化或演进时，则只需删除角色的旧功能，增加新功能或定义 色，不必更新每一个用户的权限设置。r b a c 的这种特点简化了授权管理， 信息资源的访问控制能够更好地适应特点单位的安全策略。r b a c 已被广泛 于数据库系统和分布式资源互访中。 面向对象建模 1 统一建模语言 统一建模语言( u n i f i e dm o d e l i n gl a n g u a g e ，u m l ) 是一种可视化建模语言， 对软件进行描述、可视化处理、构造和建立软件系统的文档1 4 】【15 1 。u m l 适 各种软件开发方法和软件生命周期的各个阶段，是一种通用的标准建模语言。 u m l 的基本语言要素构成由以下几部分构成： 事物：是一个模型的一级抽象成员，即构成模型的元素。 关系：语言要素之间的关系。 图：语言所能够提供的图形类型。 u m l 中事物有以下四类： 结构：语言的静态构成要素，如：对象类、用例图、接口、组件等。 行为：语言的动态构成要素，表示事物的变化和状态，如：消息。 分组：对模型中事物分组组织的要素，如：包。 注释：对模型中事物标注和解释，如：注解。 u m l 中的关系有四种关系，分别是关联、泛化、依赖和实现。 关联：本指事物之间存在的固有的牵连关系，在u m l 中，是对具有共同结 征、关系和语义的对象之间的链接描述。聚合关联是表示集合( 整体) 和部 间的整体部分关系的一种关联。聚合关联常称“有一个( 对于对象) ”和“有 ( 对于类) ”关系。在描述聚合关系时，使用一个空心菱形，将其附加在连接 合类的路径末端。 泛化：描述事物之间的一般和特殊关系。特殊事物具有并继承一般事物的结 能和行为功能。泛化关系的描述形式是从特定元素指向一般事物的实线路径， 径末端有一个空心三角，连接到一般事物。 依赖：描述两个事物之间的因果关系，其中一个事物( 独立元素) 发生变化 会影响另外一个事物( 依赖元素) 的语义。依赖的描述形式是一个虚线箭头，从 依赖的元素指向独立的元素。 实现：表示提供说明的元素和为说明提供实现的元素之间的关系。一种是接 口和实现它的类和构建：另一种是用例和实现它们的协作。 本文主要利用u m l 语言中的类图来表示访问控制系统，下面介绍类图的概 念及其使用： l o 硕上学位论文 在u m l 中，类图使用类和关联描述系统静态结构。 ( 1 ) 类 类是共享相同属性和行为的对象的集合，它为属于该类的所有对象提供统一 的抽象描述和生成模板。类具体定义了结构功能和行为功能，结构功能包括属性 和关联，它可以定义抽象的组成元素。行为功能包括操作和方法，定义组