【作者】 张昭理；

【导师】 洪帆；

【作者基本信息】 华中科技大学 ， 信息安全， 2007， 博士

【摘要】 伴随着科学技术的飞速发展,信息已成为推动社会前进的巨大动力。利用计算机和网络对信息进行收集、加工、存储以及交换等,越来越成为各行各业必不可少的手段,计算机已经渗透到了社会生活的各个方面,各种信息系统的建立和使用造成我们对计算机系统事实上的依赖。但是,由于各系统中存储的数据、网络上传输和交换的数据都是具有一定价值的信息,对这些信息的非法访问、窃取、篡改等行为必然导致计算机安全问题的出现。当前,系统的庞大和复杂化使得系统安全性能分析与验证问题变得越来越复杂并越来越引起人们的重视。提供有效的数学理论工具、直观的模型描述方法和有效的模型分析方法以及实用的辅助分析软件,是系统安全性能分析与验证所面临的迫切需要解决的问题,这也正是基于Petri网的安全策略分析与验证技术的核心。从计算机系统、Web服务以及安全协议的安全需求和现实基础出发,对相关理论、协议、关键技术以及具体实现进行了广泛深入的研究。主要研究工作包括以下几个方面:保密性策略和完整性策略是重要的安全策略,在许多军用和商用系统中得到广泛的应用。其代表模型分别是Bell-LaPadula模型和Biba模型,这两个模型是数学上的对偶。保密性策略用于防止信息的非授权泄漏,而完整性策略则是防止信息被非授权更改。对采用了特定安全模型的具体实用系统需要一个严格有效的方法对其保密性和完整性进行分析和验证。安全策略研究的一个关键问题是:用易于理解的和精确的形式表达策略。因此,提出了利用Petri网对安全策略进行描述,Petri网不仅适合策略的表达,而且可用于系统分析,以确定所定义的机制是否符合策略定义。对于一个安全策略,首先建立基于Petri网的形式化描述,然后就可以根据形式化的描述对实施了特定安全模型的进程或系统进行分析与验证。分别对Bell-LaPadula保密性模型和Biba完整性模型进行了描述。给出了这两个模型基于Petri网的形式化定义,并对实施了这两个安全模型的相应示例进程进行了分析和验证。显示出Petri网不仅能够用用易于理解的和精确的形式表达安全策略,而且可用于系统分析和验证。Petri网的覆盖图则在自动分析大型复杂系统方面很有用处。为了对实施了中国墙模型的系统进行分析与验证,提出了一种基于有色Petri网的混合安全策略分析方法。中国墙模型是一种兼顾保密性和完整性的混合安全模型。中国墙模型的显著特征是自由选择和强制性访问控制的结合。首先,对中国墙模型进行了非形式化的描述,并且将中国墙模型与其他安全模型进行了比较。然后,给出了中国墙模型基于有色Petri网的形式化定义。其突出特征在于,引入了“控制库所”的概念以解决跟踪主体访问记录的问题。并且“控制库所”代替访问控制矩阵,与单个主体关联,不需要集中存储,更加适合在分布式环境下部署。最后,根据中国墙模型基于有色Petri网的定义,通过对一个实施了中国墙模型的示例进程进行分析与验证,阐述了如何通过基于有色Petri网的形式化定义和覆盖图分析和验证实施了中国墙模型的系统的行为。当前的互联网正在经历着一些重要的变化,它已经成为了一个Web服务的载体,而不仅仅是一个信息的容器。Web服务提供了一个语言中立,连接松散,独立于平台的方式,使得散布在互联网上的各组织和企业内部的应用程序可以连接起来。Web服务合成可以让我们将许多现有的Web服务结合起来,形成一个新的,增值的Web服务。可靠的Web服务合成需要建模的技术和工具。因此,提出了一个基于有色Petri网的Web服务合成模型。这个模型为Web服务合成提供了充分的表达能力,能够直接变换为可执行的合成定义,并且独立于可执行的合成语言。基于Petri网的Web服务合成模型还可以利用Petri网的分析和验证能力对合成服务进行安全分析和验证。首先,对Web服务建立了有色Petri网模型(服务网),然后在此定义的基础上给出了四种基本Web服务合成结构:顺序结构,并发结构,选择结构,和循环结构以及一种高级合成结构置换结构的形式化定义。并且还定义了一个具有封闭性的Web服务合成算法。最后,根据基于Petri网的形式化验证方法对此Web服务合成模型的可用性,保密性,完整性以及混合安全性进行了分析和验证,得出了一些有用的结论。20年来,安全协议研究的进展十分可喜,取得了丰富的研究成果。特别是20世纪90年代以来,研究取得突破性进展,对安全协议若干本质性的问题有了更为深刻的认识。但是,这一领域还有许多问题有待解决。特别是形式化分析领域。因此,提出了一种基于有色Petri网的安全协议分析验证方法,该方法分为4个步骤:建立安全协议的Petri模型,建立入侵模型,找出不安全状态,验证不安全状态的可达性。并且通过对STS协议在特定攻击模式下的分析演示了该方法的工作原理和流程。更多还原

【Abstract】 With the rapidly development of science and technology, information technology has had an influence on the way we work and on society in general. Information technology is more and more becoming the requisite tools for gathering, processing, storing and exchanging information with computers. We are more and more relying on computer systems. However, the data stored in systems, transferred and exchanged on networks is valuable. When the information is unauthorized accessed, intercepted or modified, the problems of computer security are coming out.Nowadays, huge and complex systems make the security analysis and verification become more complex and get more concerned. Security analyzing and verifying systems needs available mathematical tools, visual model describing and analyzing methods and practical assistant software. And that is the core element for the security analysis and verification technology based on Petri nets.Based on realistic requirements and foundations, this thesis engaged in extensive research on some relevant theories, protocols and key technologies. The main contributions are as follows:Confidentiality policy and integrity policy are important security policies, implemented in many militarily and commercial systems. Bell-LaPadula model and Biba model are mathematical dual. A confidentiality policy prevents the unauthorized disclosure of information, and an integrity policy prevents the unauthorized modification of information. Both security models and practical systems need an available method to conduct security analysis and verification. One of the most important issues in security policies research is: to describe the policies in precise and easily understand form.Thus, this thesis proposes a method to describe security policies by Petri nets. Petri nets are not only good for define policies, but also well for system analysis to verify that the system mechanisms are corresponding with the definitions. For a security policy, firstly build the Petri net-based model and formal definitions of the model, and then The Petri net-based definitions and the coverability graph allow one to analyze and verify the security policy in Petri net model of a system. In this thesis, the Petri net-based definitions of Bell-LaPadula model and Biba Model are formally described in detail. Subsequently, examples of the confidentiality policy and integrity policy are illustrated and the conclusions show that Petri net is not only a concise graphic analysis method, but also suited to formal verification.For analyzing and verifying systems implemented with Chinese Wall policy, this thesis proposes a Petri net-based method to analyze hybrid policy. The Chinese Wall model is a model of a security policy that refers equally to confidentiality and integrity. The important feature of the Chinese Wall policy is the combination of discretionary access control and mandatory access control. Firstly, the Chinese Wall policy is informally described, and compared with other security policies. And then, the Petri net-based formal definitions are given. The main contribution of the definitions is the concept of "control place", which is used to trace the access record of subjects. The access control matrix is replaced by control place, which is associated with single subject and suited for implementation in distributed environment. Finally, the analysis and verification of the Chinese Wall policy by the method are addressed through a sample system.The Internet is going through several major changes. It has become a vehicle of Web services rather than just a repository of Information. Web services provide a language-neutral, loosely coupled, and platform-independent way for linking applications within organizations or enterprises across the Internet. Web services composition allows us to combine a number of existing Web services into a new, value-added Web service.Therefore, there is a need for modeling techniques and tools for reliable Web service composition. This thesis proposes a Colored Petri net-based model for Web service composition. This model is sufficiently expressive for Web service composition, can be transformed to directly executable composition specification; and is independent of the executable composition languages. Firstly, we model web service as colored Petri net (service net), based on which four basic composition construct and one advance composition construct are formally defined. Subsequently, we present the algebra that allows the creation of new value-add Web services using existing ones as building blocks. Finally, the colored Petri net-based web service composition model is verified on availability, confidentiality and integrity, and reaches some useful conclusions.In recent twenty years, the research on security protocols has made great achievements. Especially from 1990’s, some breakthroughs made us better understand several essential issues of security protocols. However, many problems need to be solved in this field, especially in formal analysis. Thus, this thesis proposes a Petri net-based method to analyze and verify security protocols. There are 4 steps: describe the protocol in a colored Petri net form, describe the intruder model, find the insecure states and verify the reachability of the insecure states. The theory and work flow of the method are illustrated by analysis of STS security protocol.更多还原