【作者】 卢亚辉；

【导师】 孙家广； 张力；

【作者基本信息】 清华大学 ， 计算机科学与技术， 2008， 博士

【摘要】 工作流技术是支持企业内部和企业之间业务过程协同的重要使能技术,它将企业的人员、数据、应用程序等资源通过业务过程自动化的形式联系了起来。在工作流系统中,为了保护企业的私有业务数据不受用户的非法访问,需要建立一个灵活而全面的访问控制机制,以便对管理员和普通用户的权限进行控制。同时,为了保证工作流系统的正确性和安全性,必须对业务过程与访问控制策略之间的一致性进行形式化分析和验证,以避免工作流系统在运行期间因为资源访问的限制而出现死锁、例外、失败等问题。本文研究了工作流系统的访问控制模型及其安全性分析的方法。论文的主要工作如下:1.提出了一种基于域管理的访问控制模型DATRBAC。该模型综合了访问检查、授权和管理等几个方面,并引入了管理域和管理角色的概念来对管理权限进行分配。对于由多个管理角色所定义的不同访问控制策略之间的冲突,给出了冲突解决方法。2.提出了一种基于着色Petri网的工作流系统建模和安全性分析的方法。该方法首先用着色Petri网对工作流系统中的控制流、授权规则以及权职分离约束进行建模。然后通过可达树的方法来分析该工作流系统在权职分离约束下的安全性。3.提出了一种基于Pi演算的工作流系统建模和安全性分析的方法。首先提出了WFPI演算,该演算扩展了Pi演算的语法和语义,可以更好地对面向服务的工作流系统进行建模。然后提出了一种类型系统,该类型系统可以保证通过类型检测的WFPI系统会一直遵守访问控制策略。4.给出了DATRBAC模型在国产全生命周期软件TiPLM上的实现方法,包括需求分析、功能设计、数据库设计等步骤。然后使用企业中的实际数据,对所实现的访问控制模块的性能进行了实验评测。更多还原

【Abstract】 The fast evolving workflow technologies facilitate organizations to interact and cooperate with each other to achieve their business goals by process collaborations. The workflow system connect people, data and applications by the automation of business processes. Access control is an important security mechanism for organizations to protect their resources. It is rather a great challenge to balance the competing goals of collaboration and security in workflow systems. A flexible and complete access control model is required for workflow systems to restrict the permissions of the system administrators and the common users. Meanwhile, to guarantee the correctness and security of the workflow systems, the formal methods should be used to analyze and verify the consistence between the workflow processes and the access control policies, to avoid deadlocks, exceptions and failures in workflow systems during the run time.The thesis is focused on the access control model for workflow systems and the security analysis of workflow systems by formal methods. The main contributions of the thesis are as follows:1. A domain administration of task-role based access control model (DATRBAC) is proposed. This model integrates access check, authorization and administration aspects of access control. The authorization and administration permissions are distributed to multiple administrative domains and administrative roles. It also propose the solutions to detect and resolve the conflicts between access control policies defined by different administrative roles.2. It proposes a method to formalize and analyze workflow with SoD constraints based on Colored Petri Nets (CPN). The control flow, authorization rules and SoD constraints in a workflow are all represented by CPN and combined into one integrated CPN model. Then the execution paths of this model can be derived by reachability tree analysis. By analyzing these execution paths, some latent deadlocks caused by the inconsistency between authorization rules and SoD constraints can be detected. 3. It proposes a method to formalize and analyze security properties of workflow systems by process calculus and types. It first present WFPI, workflow Pi calculus, to formalize the elements of workflow systems. Based on WFPI, a type system is then proposed to ensure that the specified TBAC policy is respected. By subject reduction, the well-typed system can respect the TBAC policy at run time, by avoiding runtime access violations. A java-based type tool is developed to implement the type judgment and type inference on the WFPI systems.4. It describes the method to implement the DATRBAC model in the Product Lifecycle Management System TiPLM. It describes main steps of the implementation, including requirement analysis, function design and database design. The access control performance of the system is also tested by practical enterprise data.更多还原