基于Petri网的RBAC模型计算机安全性分析与冲突处理

第1章 绪论1.1课题背景及意义访问控制技术是信息系统安全的核心内容，其主要目的是通过对用户访问资源的活动进行有效监控，使合法的用户在合法的时间内获得有效的系统访问权限，防止非授权用户访问系统资源[1]。通常信息系统用一个访问控制规则集合来表示实现安全目标的安全策略，并依据安全访问控制模型制定安全策略[1, 2]。随着安全需求的不断变化和发展，研究人员已经提出了很多的安全访问控制模型并得到了广泛应用。安全访问控制模型描述了信息系统的安全特性，需要对安全策略所表述的安全需求进行简易、抽象、无歧义的描述，从而为设计开发安全的系统提供设计和评估标准。因此用形式化的方法准确地表述安全访问控制模型的安全策略所表述的安全的机密性、完整性和可用性需求以及与系统行为的关系这点十分重要。它是实现系统安全保护的重要依据，也是建立和评估安全系统的重要依据。在此基础上，安全访问控制模型的形式化安全分析也是设计开发高可信安全系统的重要前提，只有同时达到形式化定义和安全分析验证这两个目标才能避免系统中出现安全缺陷。因此，信息系统不仅需要功能强大的安全访问控制模型，同时需要对安全模型进行形式化设计和安全性分析，才能使其更好地满足安全需求，保证信息系统的安全。2021年我国政府制定了《国务院对于促进信息消费扩大内需的若干意见》，强调信息化对我国的经济安全水平具有严重影响，要加强建设信息基础设施，提高信息网络安全保障能力，确保信息安全来规避经济安全风险或最大限度地减少这类风险1。因此，信息安全问题是世界各国政府、企业关注的焦点。基于角色的访问控制（Role-Based Access Control，RBAC）模型作为访问控制模型研究的基石，是目前最成熟稳重和成功的访问控制模型，作为信息系统安全的核心技术之一，其在确保信息安全方面发挥了重要作用。RBAC模型具有策略无关、自管理和便于实施信息系统安全策略的优点[3]。但RBAC模型仍存在一些形式化的安全缺陷和冲突，导致攻击者能够在未授权的情况下访问或破坏系统，比如RBAC模型缺乏信息流控制机制，存在非法信息流安全隐患等；而多域环境下的IRBAC（Interoperable Role-Based AccessControl）模型未定义静态职责分离和其冲突处理方法，会造成域中静态互斥角色约束冲突；另外，具有时间约束的TRBAC（Temporal RBAC）和GTRBAC（Generalized TRBAC）模型的形式化定义也存在安全漏洞。这些安全缺陷和冲突可能造成访问控制的错误裁决，数据被泄漏到非授权方，造成十分严重的后果。如2021年2月，美国第二大医疗保险公司Anthem，由于其访问控制的安全策略存在安全问题被黑客入侵并盗走8000万个人信息2。因此RBAC模型安全问题的分析和解决、以及安全策略的冲突处理至关重要，是当前RBAC模型研究领域的挑战，对它们的研究工作对于信息系统的安全十分重要。.......1.2安全访问控制技术及国内外研究现状从上世纪70年代起，很多学者就开始研究信息安全。1985年，第一个公认的可信计算机评估标准《TCSEC》由美国国防部颁布，该标准也被称为桔皮书，至此，更多的学者开始研究系统安全模型，并且一些安全模型在实际的系统中得到了实现。传统的访问控制主要包括自主访问控制、强制访问控制和基于角色的访问控制三种[4]。自主访问控制（Discretionary Access Control，DAC）允许资源的所有人来配置该资源的访问策略。如UNIX、Linux和Windows等目前主流的操作系统都实现了DAC。自主访问控制的缺点是容易出现信息裂缝，从而引起信息泄露。强制访问控制（Mandatory Access Control，MAC）可以解决自主访问控制中的信息泄露问题，根据安全需求主体和客体会被分配各自的安全属性标签，当主体访问某个客体时，安全监视机构会检查主体和客体的安全标签是否一致，从而控制着主体对客体访问。强制访问控制相比自主访问控制不会出现信息泄露问题，安全性更高。目前，Linux系统中集成的SElinux便是MAC的一个具体实现。实际应用中的安全需求在不断变化和发展，传统的自主访问控制和强制访问控制已经不能满足新的安全需求，一些新的安全模型应运而生，其中基于角色的访问控制模型是目前最成熟稳重和成功的。该模型已经在一些系统中实现，比如Oracle的基于角色的数据库对象访问控制。除了RBAC模型，研究者进行了深入研究后也提出了一些其它访问控制模型，比如基于对象的访问控制（Object-based Access Control，OBAC）、基于任务的访问控制（Tas-basedAccess Control，TBAC）和基于内容的访问控制等。当一个RBAC模型安全系统的用户数量多且权限设置差异较大时，需要管理员对用户与角色进行关联以外，还需要将大量的对象访问权限赋予给对应的角色，安全管理代价将变得很大。此外随着角色、用户和权限的变更，安全管理员必须更新所有角色的访问权限设置。如果这些变化经常发生，访问控制管理的难度和工作量将显著增加。针对这些问题，1995年，Barley提出了一个使用面向对象技术实现RBAC的方法[5]，该方法不会由于角色和权限的变更对应用程序产生很大的影响，提供了灵活方便的安全管理。传统的DAC、MAC和RBAC等访问控制模型都是从系统的角度出发去保护资源，其访问控制的上下文环境是固定的，访问控制系统不能审计和跟踪主体对访问权限的使用，主体可以在任何时刻并且不受次数限制地使用自己拥有的权限[6]。1997年，Thomas和Sandhu首次提出了基于任务的访问控制模型（TBAC）[7]，该模型是一种从应用角度来建立的主动式访问控制模型，以面向任务的观点，根据工作流中不同的任务及现实，实现模型访问权限的动态管理[7]。2002年，Adam等人[8]针对数字图书馆环境提出了一个基于内容的授权模型（Content-Based Authorization Model），可以根据用户的特点自动决定其访问权限，支持内容相关和不相关的访问控制，且可以灵活的实现不同粒度的对象安全访问控制，大大降低了安全管理的难度和工作量。这些访问控制模型在特定环境下运行并得到了很好的应用。........第2章 基于Petri网的RBAC模型非法信息流检测与控制方法2.1引言基于角色的访问控制模型(RBAC)是一种策略中立的安全模型，其支持三个著名的安全规则：最小权限、职责分离和数据抽象。RBAC模型通过引入角色大大简化了用户和权限的管理操作，该模型已经成为了一个被广泛使用的安全模型，并在2004年被采纳为NIST模型[11]。访问控制可以通过访问控制规则控制用户对信息的非法访问，访问一般包括主体（subject）、客体（object）和操作（operation），可定义为一个三元组(s, o, op)，表示主体s可以对客体o执行操作op。在RBAC模型中，权限（Permission）被定义为一个二元组(o,op)。一个用户（主体）可以通过角色间接获取权限(o, op)，表示主体s可以对客体o执行操作op。当一个主体访问一个其可读访问的客体时，主体在读取到客体中的信息后可以把读取到的信息写入到另外一个其可写访问的客体，这种信息流动就可能产生非法信息流。在强制访问控制模型（MAC）中，访问控制通过绑定在主体和客体的安全标签实现[12]。著名的BLP[12]模型提供了两个属性实现具体的安全访问控制。一个属性为ss-property，该属性决定了一个主体是否允许从一个客体读信息，另外一个属性是*-property，它根据安全标签决定一个主体是否被允许向一个客体写入信息，明确定义了信息流和信息流的控制方法。虽然RBAC在某些方面有着自主访问控制和强制访问控制不具有的优点，但RBAC不像MAC，非法信息流和信息流控制机制都没有定义。在RBAC系统中，当主体对客体对象进行读写访问时，信息可能在被访问客体对象间发生流动，从而使某些用户获取到授权策略不允许其访问的客体中的信息，从而带来了严重的安全隐患，降低了系统的安全性。因此必须在RBAC中实现信息流的控制，阻止用户访问未授权的非法信息，这从安全角度考虑是一个十分重要的问题。........2.2基于有色Petri网的非法信息流控制模型如果一个RBAC配置是信息流安全的，则该RBAC模型不会产生非法信息流。但有时，即使RBAC配置不是信息流安全的，也需要在保证安全前提下继续正常工作，提供安全服务。实际上，只有一些特殊的操作序列可能产生非法信息流，上节中，操作序列(u(1),Read,object(1))，(u(1),Write,object(2))，(u(2),Read,object(2))产生了非法信息流，但其它操作序列则没有产生非法信息流，例如序列(u(1),Read,object(1)), (u(2),Read,object(2))，(u(1),Write,object(2)),其对应图2-11中node1→node2→node5→ node9。因此可以动态监测用户的操作，当用户的操作会读到非法信息时及时阻止用户的读操作就可以避免非法信息流的产生。为了可以将有色Petri网信息流模型用在实时系统中，有色Petri网必须具备实时监测和控制信息流的能力。本文通过在图2-6有色Petri网信息流模型为变迁R添加守卫函数来实现非法信息流的检测并阻止引起非法信息流的读操作。.......第3章 基于Petri网的IRBAC域间SMER约束冲突检测方法............ 453.1引言....... 453.2 IRBAC模型和SMER约束相关概念....... 463.3基于Petri网的域间SMER约束冲突检测........... 483.4 SMER约束安全的先决条件..... 503.5实验验证与效率分析.............. 533.6本章小结.......... 56第4章 面向隐私保护的IRBAC域间SMER约束冲突检测方法........ 574.1引言....... 574.2 SMC基础模块.............. 584.3基于矩阵乘积的SMER约束冲突检测............. 594.4面向隐私保护的三方矩阵乘积协议.... 654.5面向隐私保护的IRBAC域间SMER约束冲突检测协议........... 694.6面向隐私保护的三方安全矩阵乘积协议效率分析.... 704.7实验验证与分析........... 704.8本章小结.......... 73第5章 时间约束RBAC模型的安全分析与改进..... 755.1引言....... 755.2 TRBAC和GTRBAC模型............ 765.3周期表述式和周期时刻表述式........... 775.4 TRBAC和GTRBAC模型的安全分析..... 785.5 TRBAC和GTRBAC模型的形式化定义问题及分析...... 815.6 TRBAC和GTRBAC中周期性角色有效时间约束的简化表述............. 865.7改进的时间约束RBAC模型的形式化定义...... 9155.8基于有色Petri网的时间约束RBAC模型的形式化验证........... 1085.9实验验证与分析........... 1115.10本章小结.......... 123第5章 时间约束RBAC模型的安全分析与改进5.1引言自动化和职能是新模型中增加的。自动化是指自动化的权限授予和撤销。也就说在不降低安全需求情况下，实现用户/角色、权限/角色等本来需要管理员完成分配以及撤销的自动化操作。职能是随着安全信息共享和内部威胁的连续识别需求而得到重视的。它是指在一个系统中人类用户要对他（她）所作的个人操作负责。这需要对一些敏感操作进行详细的审计记录。这些详细的审计跟踪记录可以用来触发欺骗监测系统并直接把一些可疑的活动通知给一些用户而引起他们的注意。或者每当进行敏感操作时就触发一条消息通知适当的用户。这些可称为增强审计和目标通知。另外，当进行比较重大的工作时，可以用各种重新授权方法来保证人或恶意软件不能进行非法的活动，这被称之为认证调整。Sandhu认为基于这些新的原则及其扩展的下一代访问控制模型将能够满足下一代系统的真实世界中的安全和保护需求。虽然传统的RBAC模型已经十分的成熟稳重与强大，但在过去的十几年里，在传统RBAC模型基础上又做了很多很有影响的扩展和增强。它们实际上有很多是与下一代RBAC模型以及自动化的管理相关的。一些文献讨论了用户/角色和角色/权限的授权和撤销的自动化管理。文献[72]从会话级根据实际的用户行为来实现动态的权限分配与管理。文献[73–80]根据用户的当前空间位置信息来实现权限的动态管理与维护，这些模型特别是在移动网络环境下十分有意义。文献[81, 82]则是对传统的RBAC模型增加了时间约束后进行了讨论。带有时间约束的RBAC模型是较早提出的一种RBAC扩展模型，TRBAC[81]通过约束，也就是根据带有时间的策略配置以及管理员的管理操作，用户的请求操作决定用户在某个时刻t的某个访问是否被允许，是否在时刻t拥有相应的访问权限。文献[82]则在TRBAC模型基础上扩展了一些时间约束，提出了一个新的时间RBAC模型-GTRBAC。但前面两种模型都在周期性时间基础上进行定义和讨论，认为事件的发生是可持续的，忽略了事件发生的瞬时特性，因此模型定义存在很多缺点。在实际系统的开发和应用中，事件本身可以周期性的在某个时刻出现，也可以随机在某时刻出现，因此前面两种模型定义和实际应用存在不一致性，不易用程序直接表述和实现。另外，这两个模型的形式化设计和定义也不完全准确，存在安全性问题。安全访问控制模型的形式化验证是设计开发高可信安全系统的前提，达到形式化验证这个目标才能避免系统中出现安全缺陷。因此为了保证时间约束RBAC模型的安全性，需要对时间约束RBAC模型进行形式化验证。本文将对带有时间约束的RBAC模型的形式化和安全性进行研究，分析和解决存在的问题。

........结 论本文对RBAC及其扩展模型中依然存在的一些问题进行了研究，包括RBAC模型中非法信息流的检测与控制、多域环境下的IRBAC模型静态互斥角色约束违反检测、具有时间约束的TRBAC和GTRBAC模型的安全分析与改进以及改进时间约束RBAC模型的形式化验证。本文的研究成果主要包括以下几方面：第一、针对RBAC模型中非法信息流问题，本文提出了一种基于經典Petri网的RBAC非法信息流研究方法，该方法可以利用单托肯經典Petri网的可达标识和可达标识图十分方便地可视化RBAC中的非法信息流问题。基于安全对象的概念，提出了基于Petri网的非法信息流检测算法，该算法可以有效地检测RBAC模型中的非法信息流，并解决了可能由于RBAC配置策略中存在信息流环路产生的无界Petir网问题。针对經典Petri网的建模和表述能力不能有效地对信息流进行有效地控制的问题，提出了一种基于有色Petri网的RBAC非法信息流研究方法，使用颜色toen代表不同的信息，通过为有色Petri网模型中的变迁定义守卫函数的方法来有效地控制和阻止非法信息流，从而在保证信息流安全的前提下实现尽可能多的数据流动。第二、针对IRBAC模型SMER约束冲突问题，本文提出了一种基于Petri网的IRBAC静态互斥角色约束冲突分析方法，该方法可以方便地把IRBAC静态互斥角色约束冲突检测问题转化为Petri网的现实空间搜索问题，同时本文基于Petri网模型给出了IRBAC模型存在SMER约束冲突的充要条件并进行了证明，实验和证明显示该方法可以有效地分析和检测SMER约束冲突。本文也提出了角色关联和用户/角色分配操作时保证IRBAC模型SMER约束安全的先决条件，为IRBAC模型的角色关联和用户/角色分配动态操作提供了安全保证机制。第三、针对面向隐私保护的IRBAC模型SMER约束冲突检测问题，本文提出了基于矩阵乘积的SMER约束冲突的检测方法和面向隐私保护的IRBAC模型SMER约束冲突的检测框架，并分别基于OT1n茫然传输协议和Paillier同态加密模式提出了三方安全矩阵乘积协议，在此基础上提出了面向隐私保护的IRBAC域间动态转换静态互斥角色约束冲突检测协议。通过实验和分析比较了两种方案的效率，基于Paillier同态加密模式的三方安全矩阵乘积协议效率更高。..........参考文献（略）