【作者】 马健丽；

【导师】 刘欣然；

【作者基本信息】 北京邮电大学 ， 信息安全， 2010， 博士

【摘要】 近年来,针对政府、企业计算机信息系统的漏洞攻击、黑客恶意代码传播以及拒绝服务攻击活动频有发生,对国家安全和社会稳定造成了极大危害。为保证系统业务安全运行及其处理信息不会泄露或被篡改,我国提出了对计算机信息系统实现安全等级保护的要求,并将等级保护作为国家信息安全保障的一项基本制度、基本策略和基本方法。近十年,我国在信息安全等级保护方面出台了一系列相关的政策法规及其技术标准。本文以信息系统等级保护安全功能符合性检验为背景,研究了国内外已有的信息安全评估、安全测评方法及技术,结合我国信息安全等级保护要求,基于证据理论构建了一个多层安全功能符合性检验框架,并给出一种确定检验要素集合的方法。此外,本文将模型检测技术应用于信息系统的安全功能符合性检验中,给出安全策略的符合性、有效性和一致性验证方法。本文主要工作和研究成果有：(1)研究了与检验相关的安全评估、测试理论和协议一致性测试方法等,设计了安全功能符合性检验一般模型。由信息系统安全功能符合性检验的目标,参考软件测试的理论基础,提出了检验方法正确性的形式化表示方法。具体为：在给出衡量检验准则有效性和可靠性定义及其形式化描述的基础上,提出了理想检验集的概念；(2)研究了国内外信息安全相关标准,并深入分析了我国信息系统安全等级保护相关的几个主要标准,综合这些标准要求,得出不同等级的信息系统安全功能需求。针对这些安全功能要求,建立了基于证据理论的安全功能符合性检验三层证据框架,基于此框架提出一种信息系统安全功能检验集的确定方法；(3)将模型检测应用于信息系统安全策略的符合性检验,主要完成了安全策略与安全需求的符合性验证以及安全策略对其实施系统的有效性验证。在符合性验证中将系统的安全策略转化为策略规则约束下的系统操作,并采用有限状态机对其进行建模,安全需求则采用线性时态逻辑公式描述,基于模型检测完成了系统安全策略与安全需求的符合性检验。而在有效性验证中,安全策略则采用线性时态逻辑公式描述,对系统的结构及性能分别进行建模,最后应用模型检测方法验证安全策略的有效性；(4)防火墙是应用广泛的网络访问控制技术之一,目前对其安全分析的研究主要集中在安全规则分析及其冲突检测两个方面,而针对安全规则与访问策略的一致性验证研究得较少。本文提出了基于模型检测的防火墙安全分析验证方法,在安全规则形式化建模及访问策略时态逻辑描述基础上,使用模型检验工具SPIN完成了防火墙安全规则与系统安全访问策略的一致性验证；(5)设计了一个信息系统安全功能符合性检验原型系统。检验原型系统由检验管理平台和检验工具集组成,检验管理平台完成工具管理、任务管理、问卷管理、知识库管理等,管理平台提供统一的接口规范管理各检验工具。各检验工具的检验结果提供给检验管理平台后首先被解析成统一的数据格式,然后对这些数据进行综合分析而得出信息系统安全功能等级保护符合性结果。更多还原

【Abstract】 In the recent years, the computer information systems for government and business have been intruded frequently, such as security vulnerabilities, malicious code spreading, and denial of service attacks. These intrusions harmed the national security and social stability greatly. To ensure the system running securely and the information that processes without leakage and tamper, the information systems have proposed to apply classified protection. The information security classified protection has been a basic regulation, strategy and methods in our country. A series of policies, regulations, and standards have been developed in the near decade.To complete the conformance validation for the classified information systems’ security function, the methods and technologies of the information security evaluating and testing are researched. The secure requirements have also been analyzed for the different classes in the primary classified information standards. Then, a multi-layered evidence framework has been constructed for security function conformance validation, and a method based on the evidence theory is proposed to creating the verification and validation set. In addition, the model checking technology is applied to validate the information systems security function. The conformance, validity, and compliance have been validated for security policy in this paper. The main research contents and results are shown as follows.1. Based on the research of security evaluation, testing theory, and conformance validation, a general conformance model is proposed for the information systems’ security function validation. A formal representation for the correct of validating method referenced on the software testing theory is given in according with the validating objectives. That is, the concept of the ideal test set is proposed based on the definition and formal description of the effectiveness and reliability;2. By studying on the international standards related to the information security and the primary standards for the information security classified protection, the security function requirements for the different levels have been analyzed. A multi-layered framework which is based on evidence theory has been established for the conformance verification of the information system’s security function. In addition, a method of determining the test sets has been proposed for the security verification.3. Model checking is applied to the conformance verification for the information system security function. The security policies have been verified by checking if they match the security requirements and analyzing if they are valid for the system which applies these policies. In the verification between the security policies and requirements, the policies are transformed to the system operations according to the rules and modeled as the extended finite state machines, and the security requirements is described as the linear temporal logic formulas. Then, the model checking is used to complete the conformance verification for them. The validity of security policies is also verified by using the model checking technology. The structure and performance for the information system and security policies are modeled and described respectively.4. Most studies focus on the security rules analyzing and the conflict detecting in the research for firewall security analysis. There are few studies on the consistency verification between the firewall security rules and the system access policies. This article focuses on the security rules and access policies for consistency checking. Model checking based method is proposed to complete the verification. The security rules are modeled formally, and the access policies are described by linear temporal logic. The model checker SPIN is used to complete the consistency verification for the firewall security realizations and the system security access policies.5. A verification prototype system is designed to check the information system security functions. This system is composed by the verification management platform and verification tools component. The system contains the tool management, task management, questionnaire management, and knowledge management. The check results produced by the different tools will be processed to a uniform format after they provided to the management platform. The conformance result for the information system classified protection will be given through the comprehensive analysis.更多还原