信息系统安全功能符合性检验关键技术研究
|
摘要
近年来,针对政府、企业计算机信息系统的漏洞攻击、黑客恶意代码传播以及拒绝服务攻击活动频有发生,对国家安全和社会稳定造成了极大危害。为保证系统业务安全运行及其处理信息不会泄露或被篡改,我国提出了对计算机信息系统实现安全等级保护的要求,并将等级保护作为国家信息安全保障的一项基本制度、基本策略和基本方法。近十年,我国在信息安全等级保护方面出台了一系列相关的政策法规及其技术标准。
本文以信息系统等级保护安全功能符合性检验为背景,研究了国内外已有的信息安全评估、安全测评方法及技术,结合我国信息安全等级保护要求,基于证据理论构建了一个多层安全功能符合性检验框架,并给出一种确定检验要素集合的方法。此外,本文将模型检测技术应用于信息系统的安全功能符合性检验中,给出安全策略的符合性、有效性和一致性验证方法。本文主要工作和研究成果有：
(1)研究了与检验相关的安全评估、测试理论和协议一致性测试方法等,设计了安全功能符合性检验一般模型。由信息系统安全功能符合性检验的目标,参考软件测试的理论基础,提出了检验方法正确性的形式化表示方法。具体为：在给出衡量检验准则有效性和可靠性定义及其形式化描述的基础上,提出了理想检验集的概念；
(2)研究了国内外信息安全相关标准,并深入分析了我国信息系统安全等级保护相关的几个主要标准,综合这些标准要求,得出不同等级的信息系统安全功能需求。针对这些安全功能要求,建立了基于证据理论的安全功能符合性检验三层证据框架,基于此框架提出一种信息系统安全功能检验集的确定方法；
(3)将模型检测应用于信息系统安全策略的符合性检验,主要完成了安全策略与安全需求的符合性验证以及安全策略对其实施系统的有效性验证。在符合性验证中将系统的安全策略转化为策略规则约束下的系统操作,并采用有限状态机对其进行建模,安全需求则采用线性时态逻辑公式描述,基于模型检测完成了系统安全策略与安全需求的符合性检验。而在有效性验证中,安全策略则采用线性时态逻辑公式描述,对系统的结构及性能分别进行建模,最后应用模型检测方法验证安全策略的有效性；
(4)防火墙是应用广泛的网络访问控制技术之一,目前对其安全分析的研究主要集中在安全规则分析及其冲突检测两个方面,而针对安全规则与访问策略的一致性验证研究得较少。本文提出了基于模型检测的防火墙安全分析验证方法,在安全规则形式化建模及访问策略时态逻辑描述基础上,使用模型检验工具SPIN完成了防火墙安全规则与系统安全访问策略的一致性验证；
(5)设计了一个信息系统安全功能符合性检验原型系统。检验原型系统由检验管理平台和检验工具集组成,检验管理平台完成工具管理、任务管理、问卷管理、知识库管理等,管理平台提供统一的接口规范管理各检验工具。各检验工具的检验结果提供给检验管理平台后首先被解析成统一的数据格式,然后对这些数据进行综合分析而得出信息系统安全功能等级保护符合性结果。
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.
本文以信息系统等级保护安全功能符合性检验为背景,研究了国内外已有的信息安全评估、安全测评方法及技术,结合我国信息安全等级保护要求,基于证据理论构建了一个多层安全功能符合性检验框架,并给出一种确定检验要素集合的方法。此外,本文将模型检测技术应用于信息系统的安全功能符合性检验中,给出安全策略的符合性、有效性和一致性验证方法。本文主要工作和研究成果有：
(1)研究了与检验相关的安全评估、测试理论和协议一致性测试方法等,设计了安全功能符合性检验一般模型。由信息系统安全功能符合性检验的目标,参考软件测试的理论基础,提出了检验方法正确性的形式化表示方法。具体为：在给出衡量检验准则有效性和可靠性定义及其形式化描述的基础上,提出了理想检验集的概念；
(2)研究了国内外信息安全相关标准,并深入分析了我国信息系统安全等级保护相关的几个主要标准,综合这些标准要求,得出不同等级的信息系统安全功能需求。针对这些安全功能要求,建立了基于证据理论的安全功能符合性检验三层证据框架,基于此框架提出一种信息系统安全功能检验集的确定方法；
(3)将模型检测应用于信息系统安全策略的符合性检验,主要完成了安全策略与安全需求的符合性验证以及安全策略对其实施系统的有效性验证。在符合性验证中将系统的安全策略转化为策略规则约束下的系统操作,并采用有限状态机对其进行建模,安全需求则采用线性时态逻辑公式描述,基于模型检测完成了系统安全策略与安全需求的符合性检验。而在有效性验证中,安全策略则采用线性时态逻辑公式描述,对系统的结构及性能分别进行建模,最后应用模型检测方法验证安全策略的有效性；
(4)防火墙是应用广泛的网络访问控制技术之一,目前对其安全分析的研究主要集中在安全规则分析及其冲突检测两个方面,而针对安全规则与访问策略的一致性验证研究得较少。本文提出了基于模型检测的防火墙安全分析验证方法,在安全规则形式化建模及访问策略时态逻辑描述基础上,使用模型检验工具SPIN完成了防火墙安全规则与系统安全访问策略的一致性验证；
(5)设计了一个信息系统安全功能符合性检验原型系统。检验原型系统由检验管理平台和检验工具集组成,检验管理平台完成工具管理、任务管理、问卷管理、知识库管理等,管理平台提供统一的接口规范管理各检验工具。各检验工具的检验结果提供给检验管理平台后首先被解析成统一的数据格式,然后对这些数据进行综合分析而得出信息系统安全功能等级保护符合性结果。
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.
引文
[1]Common Criteria Project Sponsoring Organizations. Common Criteria for Information Security Evaluation Part 1-3, Version2.1. Aug.1999.
[2]International Organization for Standardization. Code for Practice for Information Security Management. ISO/IEC 17799:2000, Dec.2000.
[3]SSE-CMM. Model Description Document Version 2.0.1999.
[4]刘芳.信息系统安全评估理论及其关键技术研究.[学位论文],长沙,国防科学技术大学,2005.
[5]朱方洲.基于BS7799的信息系统安全风险评估研究.[学位论文],合肥,合肥工业大学,2007.
[6]Alberts, J.Christopher, and A.J.Dorofee. OCTAVE method implementation guide, v2.0. Pittsburgh, PA:Software Engineering Institute, Carnegie Mellon University,2001.
[7]冯登国,张阳,张玉清.信息安全风险评估综述.通信学报,25(7),2004,10-18.
[8]T. L.Satty The analysis hierarchy process. New York L:McGrae-Hill,1980.
[9]T. Bedford, R.Cooke. Probabilistic risk analysis. Cambridge University Press, 2001.
[10]A.R.Karen, J.D.Andrews. A fault tree analysis strategy using binary decision diagrams. Reliability Engineering and System Safety,78(1),2002,45-56.
[11]C.Acosta, N.Siu Dynamic event trees in accident sequence analysis: application to a team generator tube rupture. Reliability Engineering and System Safety,41(2),1993,135-154.
[12]范红,冯登国,吴亚非.信息安全风险评估方法与应用.清华大学出版社,北京,2006.
[13]L.Labuschagne, JHP Eloff. The use of real-time risk analysis to enable dynamic activation of counter measures. Computers and Security,17(4), 1998,347-357.
[14]Lynete Bsmard, Rossouwvon Solums. A formalized approach to the effective selection and evaluation of information security control. Computers and Security, Vol.8,2001,185-194.
[15]蔡煜,张玉清,冯登国.基于GB 17859-1999标准体系的风险评估方法.计算机工程与应用,(12),2005,134-137.
[16]段云所,刘欣,陈钟等.信息系统组合安全强度和脆弱性分析.北京大学学报(自然科学版),41(3),2005,484-490.
[17]汤永利,徐国爱,杨义先等.基于信息熵的信息安全风险分析模型.北京邮电大学学报,31(2),2008,50-53.
[18]科飞管理咨询公司.信息安全管理概论——理解与实施.机械工业出版社,北京,2001,18-43.
[19]阎强.信息系统安全评估研究.[学位论文],北京,北京大学,2003.
[20]史简,郭山清,谢立.一种实时的信息安全风险评估方法.计算机工程与应用,(1),2006,109-111.
[21]李嵩,孟亚平,孙铁等.一种基于模型的信息安全风险评估方法.计算机工程与应用,(29),2005,159-162.
[22]C&A. System's security:The COBRA risk consultant methodology. Jul.1999.
[23]CCRA. Risk Analysis and Management Method (CRAMM).1985.
[24]NIST. Automated Security Self-Evaluation Tool (ASSET).
[25]Cost-of-Risk Analysis (CORA). International Security Technology, Inc.
[26]陈驰,冯登国,张敏,徐震.信息安全产品测评平台的设计与实现.计算机工程,33(8),2007,256-258.
[27]刘海峰,张晓梅,李嵩等.信息系统安全测评工具的设计与实现.信息网络安全,(6),2006,30-33.
[28]范红.信息安全风险评估规范国家标准理解与实施.中国标准出版社,北京,2008,120-123.
[29]公信安[2009]1429号.2009.
[30]公安部信息安全等级保护评估中心.信息系统安全等级保护实施指南(报批稿)
[31]National Security Agency. Information Assurance Technical Framework. Release 3.0. Sept.2000.
[32]Nishio S, Ozawa R, Amemiya S, and et al. Standardization of Evaluation criteria for IT security. NIT Review,12(4),2000,65-67.
[33]邹芳.信息系统安全等级测评方法研究.[学位论文],长沙,国防科学技术大学,2005.
[34]闫强.信息系统安全评估研究.[学位论文],北京,北京大学,2003.
[35]卫剑钒,刘欣,段云所.信息系统分布式安全检查模型及其设计.计算机工程,31(20),Oct.2005,141-143.
[36]魏丕会,卿斯汉,黄建.安全操作系统等级测评系统.计算机工程,29(22),2003,135-137.
[37]常伟华,蔡勉,王亚军.基于驱动表机制的操作系统等级测评系统.信息安全与通信保密,Jun.2007,121-123.
[38]程亮.基于模型检测的安全操作系统验证方法研究.[博士学位论文],北京,中国科学技术大学,2009.
[39]ISO/IEC 9646. Information technology-open systems interconnection-conformance testing methodology and framework. ISO standard,1998.
[40]J.B.Goodenough, S.L.Gerhart. Toward a theory of test data selection. IEEE Transactions on Software Engineering, Vol.SE-1, Jun.1975,493-510.
[41]古天龙.软件开发的形式化方法.高等教育出版社,北京,2005.
[42]M.Huth and M. Ryan. Logic in computer science:modeling and reasoning about systems. Cambridge University Press, Cambridge, UK,2000.
[43]Michael Huth, Mark Ryan.面向计算机科学的数理逻辑系统建模与推理.何伟,潘磊译,机械工业出版社,北京,2005.
[44]A.Pnueli. A temporal logic of concurrent programs. Theoretical Computer Sciense. Vol.13,1981,45-60.
[45]E.M.Clarke, O.Grumberg, and D.Long. Model Checking. The MIT Press, Massachusetts,1999.
[46]Edmund.M.Clarke, E.A.Emerson, and A.P. Sistla. Automatic verification of finite state concurrent systems using temporal logic specifications:a practical approach. In Proceedings of the 10th ACM Symposium on Principles of Programming Languages, Austin, TX,1983,24-26.
[47]Cindy Eisner, Doron Peled. Comparing symbolic and explicit model checking of a software system. In Proceedings of the 9th International SPIN Workshop on Model Checking of Software, Springer-Verlag,2002,230-239.
[48]J.R.Burch, Edmund M. Clarke, K.L.Mcmillan, and et al. Symbolic model checking:1020 states and beyond. In Proceedings of the 5th Annual IEEE Symposium Logic in Computer Science,1990,428-439.
[49]林惠民,张文辉.模型检测：理论、方法与应用.电子学报,30(12A),2002, 1907-1912.
[50]H.S.Hong, S.D.cha, O.Sokolsky, and et al. Data flow testing as model checking. In Proceedings of the 25th International Conference on Software Engineering,2003.232-242.
[51]P.E.Ammann, P.E.Black, and W.Majurski. Using model checking to generate tests for specifications. In proceedings of the 2nd IEEE International Conference on Formal Engineering Method. IEEE Computer Society,1998, 46-54.
[52]O.Grumberg, E.M.Clarke, and D.A.Peled. Model Checking. The MIT Press, Massachusetts,2000,27-108.
[53]M.Y.Vardi and P.Wolper. Reasoning about infinite computations. Information and Computation, Vol.115,1994,1-37.
[54]Ken L.McMillan. Symbolic model checking:an approach to the state explosiong problem. Technical Report CMU-CS-92-131, Carnegie Mellon University,1992.
[55]Gerard J. Holzmann. The model checker SPIN. IEEE Transactions on Software Engineering,23(5),1997,279-295.
[56]http://www.formal.demon.co.uk/FDR2.html.
[57]The VIS Group. VIS:a system for verification and synthesis. In the Proceedings of the 8th International Conference on Computer Aided Verification, July.1996,428-432.
[58]http://210.40.7.188/E'yan/Maria/100.asp.
[59]K.Larsen, P.Petterson, and Y. Wang. Uppaal in a nutshell. Software Tools for Technlogy Transfer, Oct.1997,134-152.
[60]T.A.Henzinger, R.Jhala. Software verification with Blast. In the Proceeding of the 10th International Workshop on Model Checking of Software. Springer-Verlag,2003,235-239.
[61]S.Chaki, E.Clarke, A.Groce, and et al. Modular verification of software components in C. IEEE Transactions on Software Engineering,30(6),2004, 388-402.
[62]K.Havelund, T.Pressburger. Model checking Java programs using java pathfinder. International Journal on Software Tools for Technology Transfer, 2(4),2000,366-381.
[63]T.Ball, S.k.Rajamani. Automatically validating temporal safety properties of interfaces. In Proceedings of the 8th International SPIN Workshop on Model Checking of Software, Springer,2001,103-122.
[64]http://www.research.microsoft.com/zing/.
[65]E.clarke, O.Grumberg, and D.Long. Model checking and abstraction. In Proceeding of ACM Symposium on Principles of Programming Languages, 1992,343-354.
[66]E.M.Clarke, O.Grumberg, and D.E.Long. Model checking and abstraction. ACM Transactions on Programming Languages and System,16(5),1994, 1512-1542.
[67]Karsten Stahl, Kai Baukus, Yassine lakhnech and et al. Divide, abstract, and model check. In SPIN.1999,57-76.
[68]Basten, Twan Bosnacki. Cluster-based partial-order reduction. Automated Software Engineering, Vol.10,2004,365-402.
[69]Rajeer Alur, K.Robert, Brayton and et al. Partial-order reduction in symbolic state-space exploration. Formal Methods in System Design,18,2001, 97-116.
[70]A.Pnueli. In transition for global to modular temporal reasoning about programs. Logics and Models of Concurrent Systems. Berlin, Springer,1984, 123-144.
[71]G.J.Holzmann. Design and validation of computer protocols. New Jersey: Prentice Hall,1991.
[72]G.Shafer. A mathematics theory of evidence. Princeton, Princeton University Press,1976,20-46.
[73]L.A.Zadeh. On the validity of Dempster's rule of combination of evidence. Mmo No.UCB/ERL-M79/24, University of California, Berkeley,1979.
[74]J.Gordon, E.H.Shortiliffe. A method of managing evidential reasoning in a hierarchical hypothesis space. Artificial Intelligence,26(3),1985,323-357.
[75]J.Lowtance, T.Garvey. Shafer-Dempster reasoning:an implementation for multi-sensor integration. SIR International, Menlo Part, CA, Tech. Note, Dec.1983.
[76]A.P.Dempster. Upper and lower probabilities induced by a multi-valued mapping. Annual Math Statist,38(4),1967,325-339.
[77]R.R.Yager. On the Dempster-Shafer framework and new combination rules. Information Science,41,1987,93-137.
[78]T.Inagaki. Interdependence between safety-control policy and multiple-sensor schemes via Dempster-Shafer theory. IEEE Transactions on Reliability,40(2),1991,182-188.
[79]孙全,叶秀清,顾伟康.一种新的基于证据理论的合成公式.电子学报,28(8),2000,117-119.
[80]向阳,史习智.证据理论合成方法的一点修正.上海交通大学学报,33(3),1999,357-360.
[81]Yen J.Gretis. A Dempster-Shafer approach to diagnosing hierarchical Hypothesis. Communications of the AC,32(5),1989,537-585.
[82]R.mahler. Combining Ambiguous evidence with respect to ambiguous a priori knowledge. Boolean Logic. IEEE Transactions on System Man Cyber, 26(1),1996,27-41.
[83]T.Fister, R.A.Mitrhell. Modified Dempster-Shafer with entropy based belief body compression. In Proceedings of Service Combat Identification Systems Conference. Monerey, CA,1994,281-310.
[84]肖人彬,王雪,费奇等.相关证据合成方法的研究.模式识别与人工智能,6(3),1993,227-234.
[85]孙怀江,杨靖宇.一种相关证据合成方法.计算机学报,22(9),1999.1004-1007.
[86]R.Malher. Combining ambiguous evidence with respect to ambiguous a priori knowledge, Part II:fuzzy Logic. Fuzzy Sets and Systems,75,1995, 319-354.
[87]H.Dubio. Presentation and combination of uncertainty with belief functions and possibility measures. Computational Intelligence, Jan.1988,88-101.
[88]P.Smets. The degree of belief in a fuzzy set. Information Science,25(1), 1981,1-19.
[89]Z.Pawlak. Rough Sets. Computer Information Science,11(5),1982,341-356.
[90]P.L.Bogler. Dempster-Shafer reasoning with application to multi-sensor target identification systems. IEEE Transactions on System, Man and Cyber, 17(6),1987,968-977.
[91]刘志言,章树鸿,王艳.基于证据理论的多分类器集成方法研究.电机与控制学报,Sep2001,208-212.
[92]M.Bauer. Approximations for decision making in the Dempster-Shafer theory of evidence. In Proceeding of the 12th annual Conference on Uncertainty in Artificial Intelligence, San Francisco, California,1996,73-80.
[93]周兆英,蓝天,马宝华等.DS证据理论数据融合方法在目标识别中的应用.清华大学学报(自然科学版),41(2),2001,53-55,59.
[94]王凤朝,刘兴堂,黄树采.基于模糊证据理论的多特征目标融合检测算法.光学学报,30(3),2010,713-719.
[95]诸葛建伟,王大为,陈昱等.基于DS证据理论的网络异常检测方法.软件学报,17(3),2006,463-471.
[96]段新生.证据推理与决策、人工智能 中国人民大学出版社,北京,1993.
[97]R.V.Hartley. Transmission of information. The Bell System Technical,7(3), 1928,535-563.
[98]G.J.Klir, M.Mariano. On the uniqueness of possibilistic measure and information. Fuzzy Sets and Systems,2(24),1987,197-219.
[99]A.Ramer. Uniqueness of information measure in the theory of evidence. Fuzzy Sets and System,24(2),1987,183-196.
[100]G.J.Klir, M.S.Richard. Recent developments in generalized information theory. International Journal of Fuzzy Systems,1(1),1999,1-13.
[101]G.J.Klir. Generalized information theory. Fuzzy Sets and Systems,40(1), 127-142.
[102]D.Dubios, H.Prade. Properties of measures of information in evidence and possibility theories. Fuzzy Sets and Systems,2(25),1987,161-182.
[103]M.T.Lamata, S.Moral. Measures of entropy in the theory of evidence. International Journal of General Systems,14,1987,297-305.
[104]R. A. Kowalski, M. J. Segot. A logic-based calculus to events. New Generation Computing,1986,67-95.
[105]A. K. Bandara, E. C. Lupu, and A. Russo. Using event calculus to formalize policy specification and analysis. In Proceedings of the 4th International Workshop on Policies for Distributed Systems and Networks,2003,26-39.
[106]K. Juszcsyszyn. Verifying enterprise's mandatory access control policies with colored Petri nets. IEEE International Workshops on Infrastructure for Collaborative Enterprise,2003,184-189.
[107]E. C. Lupu, M. Sloman. Conflict in policy-based distributed systems management. IEEE Transactions on Software Engineering, Vol.25, Jun.1999, 852-869.
[108]IEEE guide to software requirements specification. ANSI IEEE std.830.
[109]R. Abbassi, S. Guemara EL Fatmi. An automated validation method for security policies:the Firewall Case. In Proceedings of the 4th International Conference on Information Assurance and Security,2008,291-294.
[110]J.Allen. The CERT Guide To System and Network Security Practices. New York:Addison-Wesley,2001,1-200.
[111]Adel El-Atawy, Khaled Ibrahim. Policy segmentation for intelligent firewall testing. The IEEE Workshop on Secure Network Protocols, Boston, USA, 2005,67-72.
[112]P.Eronen, J.Zitting. An expert system for analyzing firewall rules. In Nordic Workshop on Secure IT System, NOV 2001.
[113]邓文俊,梁意文.防火墙安全策略的语义分析方法.计算机工程与应用,43(26),2007,135-137.
[114]S.Hazehurst. Algorithms for analyzing firewall and router access lists. Technical report trwitscs-1999, Department of Computer Science, University of the Witwatersrand, South Africa, July 1999.
[115]S.Pozo, R.Ceballos, and R.M.Gasca. CSP-based firewall rule set diagnosis using security policies. In Proceedings of the 2nd International conference on availability, reliability and security,2007,723～729.
[116]E.AL-Shaer, H.Hamed. Management and translation of filtering security Policies. In Proceedings of IEEE International Conference on Communications, Vol.1, May 2003,256-260.
[117]E.AL-Shaer, H.Hamed. Firewall policy advisor for anomaly detection and rule editing. In Proceedings of IEEE/IFIP Integrated Management, March 2003:17-30.
[118]E.AL-Shaer, H.Hamed. Firewall policy advisor for anomaly discovery and rule editing. In Proceedings of the 8th International Symposium on Integrated Network Management, Orlando, FL, USA, May.2003,17-30.
[119]E.Al-Shaer, H.H.Hamed. Modeling and management of firewall policies. IEEE Transactions on Network and Service Management,1(1),2004,1-10.
[120]E.Al-Shaer, H.H.Hamed, and M.Hasan. Conflict classification and analysis of distributed firewall policies. IEEE Journal on Selected areas in communication, Vol.23,2005,2069-2084.
[121]A.Harib, S.Suris, and G.Parulkar. Detecting and resolving packet filter conflicts. In Proceedings of IEEE INFOCOM'2000, Mar.2003,1203-1212.
[122]F.Baboescu, G.Vrghese. Fast and scalable conflict detection for packet classifiers. In Proceedings of the 10th IEEE International Conference on Network Protocols,2002,270-279.
[123]Yiwen Liang, Wenjun Deng. Verify consistency between security policy and firewall policy with answer set programming. In Proceedings of the International Conference on Computer Science and Software Engineering, 2008,196-200.
[2]International Organization for Standardization. Code for Practice for Information Security Management. ISO/IEC 17799:2000, Dec.2000.
[3]SSE-CMM. Model Description Document Version 2.0.1999.
[4]刘芳.信息系统安全评估理论及其关键技术研究.[学位论文],长沙,国防科学技术大学,2005.
[5]朱方洲.基于BS7799的信息系统安全风险评估研究.[学位论文],合肥,合肥工业大学,2007.
[6]Alberts, J.Christopher, and A.J.Dorofee. OCTAVE method implementation guide, v2.0. Pittsburgh, PA:Software Engineering Institute, Carnegie Mellon University,2001.
[7]冯登国,张阳,张玉清.信息安全风险评估综述.通信学报,25(7),2004,10-18.
[8]T. L.Satty The analysis hierarchy process. New York L:McGrae-Hill,1980.
[9]T. Bedford, R.Cooke. Probabilistic risk analysis. Cambridge University Press, 2001.
[10]A.R.Karen, J.D.Andrews. A fault tree analysis strategy using binary decision diagrams. Reliability Engineering and System Safety,78(1),2002,45-56.
[11]C.Acosta, N.Siu Dynamic event trees in accident sequence analysis: application to a team generator tube rupture. Reliability Engineering and System Safety,41(2),1993,135-154.
[12]范红,冯登国,吴亚非.信息安全风险评估方法与应用.清华大学出版社,北京,2006.
[13]L.Labuschagne, JHP Eloff. The use of real-time risk analysis to enable dynamic activation of counter measures. Computers and Security,17(4), 1998,347-357.
[14]Lynete Bsmard, Rossouwvon Solums. A formalized approach to the effective selection and evaluation of information security control. Computers and Security, Vol.8,2001,185-194.
[15]蔡煜,张玉清,冯登国.基于GB 17859-1999标准体系的风险评估方法.计算机工程与应用,(12),2005,134-137.
[16]段云所,刘欣,陈钟等.信息系统组合安全强度和脆弱性分析.北京大学学报(自然科学版),41(3),2005,484-490.
[17]汤永利,徐国爱,杨义先等.基于信息熵的信息安全风险分析模型.北京邮电大学学报,31(2),2008,50-53.
[18]科飞管理咨询公司.信息安全管理概论——理解与实施.机械工业出版社,北京,2001,18-43.
[19]阎强.信息系统安全评估研究.[学位论文],北京,北京大学,2003.
[20]史简,郭山清,谢立.一种实时的信息安全风险评估方法.计算机工程与应用,(1),2006,109-111.
[21]李嵩,孟亚平,孙铁等.一种基于模型的信息安全风险评估方法.计算机工程与应用,(29),2005,159-162.
[22]C&A. System's security:The COBRA risk consultant methodology. Jul.1999.
[23]CCRA. Risk Analysis and Management Method (CRAMM).1985.
[24]NIST. Automated Security Self-Evaluation Tool (ASSET).
[25]Cost-of-Risk Analysis (CORA). International Security Technology, Inc.
[26]陈驰,冯登国,张敏,徐震.信息安全产品测评平台的设计与实现.计算机工程,33(8),2007,256-258.
[27]刘海峰,张晓梅,李嵩等.信息系统安全测评工具的设计与实现.信息网络安全,(6),2006,30-33.
[28]范红.信息安全风险评估规范国家标准理解与实施.中国标准出版社,北京,2008,120-123.
[29]公信安[2009]1429号.2009.
[30]公安部信息安全等级保护评估中心.信息系统安全等级保护实施指南(报批稿)
[31]National Security Agency. Information Assurance Technical Framework. Release 3.0. Sept.2000.
[32]Nishio S, Ozawa R, Amemiya S, and et al. Standardization of Evaluation criteria for IT security. NIT Review,12(4),2000,65-67.
[33]邹芳.信息系统安全等级测评方法研究.[学位论文],长沙,国防科学技术大学,2005.
[34]闫强.信息系统安全评估研究.[学位论文],北京,北京大学,2003.
[35]卫剑钒,刘欣,段云所.信息系统分布式安全检查模型及其设计.计算机工程,31(20),Oct.2005,141-143.
[36]魏丕会,卿斯汉,黄建.安全操作系统等级测评系统.计算机工程,29(22),2003,135-137.
[37]常伟华,蔡勉,王亚军.基于驱动表机制的操作系统等级测评系统.信息安全与通信保密,Jun.2007,121-123.
[38]程亮.基于模型检测的安全操作系统验证方法研究.[博士学位论文],北京,中国科学技术大学,2009.
[39]ISO/IEC 9646. Information technology-open systems interconnection-conformance testing methodology and framework. ISO standard,1998.
[40]J.B.Goodenough, S.L.Gerhart. Toward a theory of test data selection. IEEE Transactions on Software Engineering, Vol.SE-1, Jun.1975,493-510.
[41]古天龙.软件开发的形式化方法.高等教育出版社,北京,2005.
[42]M.Huth and M. Ryan. Logic in computer science:modeling and reasoning about systems. Cambridge University Press, Cambridge, UK,2000.
[43]Michael Huth, Mark Ryan.面向计算机科学的数理逻辑系统建模与推理.何伟,潘磊译,机械工业出版社,北京,2005.
[44]A.Pnueli. A temporal logic of concurrent programs. Theoretical Computer Sciense. Vol.13,1981,45-60.
[45]E.M.Clarke, O.Grumberg, and D.Long. Model Checking. The MIT Press, Massachusetts,1999.
[46]Edmund.M.Clarke, E.A.Emerson, and A.P. Sistla. Automatic verification of finite state concurrent systems using temporal logic specifications:a practical approach. In Proceedings of the 10th ACM Symposium on Principles of Programming Languages, Austin, TX,1983,24-26.
[47]Cindy Eisner, Doron Peled. Comparing symbolic and explicit model checking of a software system. In Proceedings of the 9th International SPIN Workshop on Model Checking of Software, Springer-Verlag,2002,230-239.
[48]J.R.Burch, Edmund M. Clarke, K.L.Mcmillan, and et al. Symbolic model checking:1020 states and beyond. In Proceedings of the 5th Annual IEEE Symposium Logic in Computer Science,1990,428-439.
[49]林惠民,张文辉.模型检测：理论、方法与应用.电子学报,30(12A),2002, 1907-1912.
[50]H.S.Hong, S.D.cha, O.Sokolsky, and et al. Data flow testing as model checking. In Proceedings of the 25th International Conference on Software Engineering,2003.232-242.
[51]P.E.Ammann, P.E.Black, and W.Majurski. Using model checking to generate tests for specifications. In proceedings of the 2nd IEEE International Conference on Formal Engineering Method. IEEE Computer Society,1998, 46-54.
[52]O.Grumberg, E.M.Clarke, and D.A.Peled. Model Checking. The MIT Press, Massachusetts,2000,27-108.
[53]M.Y.Vardi and P.Wolper. Reasoning about infinite computations. Information and Computation, Vol.115,1994,1-37.
[54]Ken L.McMillan. Symbolic model checking:an approach to the state explosiong problem. Technical Report CMU-CS-92-131, Carnegie Mellon University,1992.
[55]Gerard J. Holzmann. The model checker SPIN. IEEE Transactions on Software Engineering,23(5),1997,279-295.
[56]http://www.formal.demon.co.uk/FDR2.html.
[57]The VIS Group. VIS:a system for verification and synthesis. In the Proceedings of the 8th International Conference on Computer Aided Verification, July.1996,428-432.
[58]http://210.40.7.188/E'yan/Maria/100.asp.
[59]K.Larsen, P.Petterson, and Y. Wang. Uppaal in a nutshell. Software Tools for Technlogy Transfer, Oct.1997,134-152.
[60]T.A.Henzinger, R.Jhala. Software verification with Blast. In the Proceeding of the 10th International Workshop on Model Checking of Software. Springer-Verlag,2003,235-239.
[61]S.Chaki, E.Clarke, A.Groce, and et al. Modular verification of software components in C. IEEE Transactions on Software Engineering,30(6),2004, 388-402.
[62]K.Havelund, T.Pressburger. Model checking Java programs using java pathfinder. International Journal on Software Tools for Technology Transfer, 2(4),2000,366-381.
[63]T.Ball, S.k.Rajamani. Automatically validating temporal safety properties of interfaces. In Proceedings of the 8th International SPIN Workshop on Model Checking of Software, Springer,2001,103-122.
[64]http://www.research.microsoft.com/zing/.
[65]E.clarke, O.Grumberg, and D.Long. Model checking and abstraction. In Proceeding of ACM Symposium on Principles of Programming Languages, 1992,343-354.
[66]E.M.Clarke, O.Grumberg, and D.E.Long. Model checking and abstraction. ACM Transactions on Programming Languages and System,16(5),1994, 1512-1542.
[67]Karsten Stahl, Kai Baukus, Yassine lakhnech and et al. Divide, abstract, and model check. In SPIN.1999,57-76.
[68]Basten, Twan Bosnacki. Cluster-based partial-order reduction. Automated Software Engineering, Vol.10,2004,365-402.
[69]Rajeer Alur, K.Robert, Brayton and et al. Partial-order reduction in symbolic state-space exploration. Formal Methods in System Design,18,2001, 97-116.
[70]A.Pnueli. In transition for global to modular temporal reasoning about programs. Logics and Models of Concurrent Systems. Berlin, Springer,1984, 123-144.
[71]G.J.Holzmann. Design and validation of computer protocols. New Jersey: Prentice Hall,1991.
[72]G.Shafer. A mathematics theory of evidence. Princeton, Princeton University Press,1976,20-46.
[73]L.A.Zadeh. On the validity of Dempster's rule of combination of evidence. Mmo No.UCB/ERL-M79/24, University of California, Berkeley,1979.
[74]J.Gordon, E.H.Shortiliffe. A method of managing evidential reasoning in a hierarchical hypothesis space. Artificial Intelligence,26(3),1985,323-357.
[75]J.Lowtance, T.Garvey. Shafer-Dempster reasoning:an implementation for multi-sensor integration. SIR International, Menlo Part, CA, Tech. Note, Dec.1983.
[76]A.P.Dempster. Upper and lower probabilities induced by a multi-valued mapping. Annual Math Statist,38(4),1967,325-339.
[77]R.R.Yager. On the Dempster-Shafer framework and new combination rules. Information Science,41,1987,93-137.
[78]T.Inagaki. Interdependence between safety-control policy and multiple-sensor schemes via Dempster-Shafer theory. IEEE Transactions on Reliability,40(2),1991,182-188.
[79]孙全,叶秀清,顾伟康.一种新的基于证据理论的合成公式.电子学报,28(8),2000,117-119.
[80]向阳,史习智.证据理论合成方法的一点修正.上海交通大学学报,33(3),1999,357-360.
[81]Yen J.Gretis. A Dempster-Shafer approach to diagnosing hierarchical Hypothesis. Communications of the AC,32(5),1989,537-585.
[82]R.mahler. Combining Ambiguous evidence with respect to ambiguous a priori knowledge. Boolean Logic. IEEE Transactions on System Man Cyber, 26(1),1996,27-41.
[83]T.Fister, R.A.Mitrhell. Modified Dempster-Shafer with entropy based belief body compression. In Proceedings of Service Combat Identification Systems Conference. Monerey, CA,1994,281-310.
[84]肖人彬,王雪,费奇等.相关证据合成方法的研究.模式识别与人工智能,6(3),1993,227-234.
[85]孙怀江,杨靖宇.一种相关证据合成方法.计算机学报,22(9),1999.1004-1007.
[86]R.Malher. Combining ambiguous evidence with respect to ambiguous a priori knowledge, Part II:fuzzy Logic. Fuzzy Sets and Systems,75,1995, 319-354.
[87]H.Dubio. Presentation and combination of uncertainty with belief functions and possibility measures. Computational Intelligence, Jan.1988,88-101.
[88]P.Smets. The degree of belief in a fuzzy set. Information Science,25(1), 1981,1-19.
[89]Z.Pawlak. Rough Sets. Computer Information Science,11(5),1982,341-356.
[90]P.L.Bogler. Dempster-Shafer reasoning with application to multi-sensor target identification systems. IEEE Transactions on System, Man and Cyber, 17(6),1987,968-977.
[91]刘志言,章树鸿,王艳.基于证据理论的多分类器集成方法研究.电机与控制学报,Sep2001,208-212.
[92]M.Bauer. Approximations for decision making in the Dempster-Shafer theory of evidence. In Proceeding of the 12th annual Conference on Uncertainty in Artificial Intelligence, San Francisco, California,1996,73-80.
[93]周兆英,蓝天,马宝华等.DS证据理论数据融合方法在目标识别中的应用.清华大学学报(自然科学版),41(2),2001,53-55,59.
[94]王凤朝,刘兴堂,黄树采.基于模糊证据理论的多特征目标融合检测算法.光学学报,30(3),2010,713-719.
[95]诸葛建伟,王大为,陈昱等.基于DS证据理论的网络异常检测方法.软件学报,17(3),2006,463-471.
[96]段新生.证据推理与决策、人工智能 中国人民大学出版社,北京,1993.
[97]R.V.Hartley. Transmission of information. The Bell System Technical,7(3), 1928,535-563.
[98]G.J.Klir, M.Mariano. On the uniqueness of possibilistic measure and information. Fuzzy Sets and Systems,2(24),1987,197-219.
[99]A.Ramer. Uniqueness of information measure in the theory of evidence. Fuzzy Sets and System,24(2),1987,183-196.
[100]G.J.Klir, M.S.Richard. Recent developments in generalized information theory. International Journal of Fuzzy Systems,1(1),1999,1-13.
[101]G.J.Klir. Generalized information theory. Fuzzy Sets and Systems,40(1), 127-142.
[102]D.Dubios, H.Prade. Properties of measures of information in evidence and possibility theories. Fuzzy Sets and Systems,2(25),1987,161-182.
[103]M.T.Lamata, S.Moral. Measures of entropy in the theory of evidence. International Journal of General Systems,14,1987,297-305.
[104]R. A. Kowalski, M. J. Segot. A logic-based calculus to events. New Generation Computing,1986,67-95.
[105]A. K. Bandara, E. C. Lupu, and A. Russo. Using event calculus to formalize policy specification and analysis. In Proceedings of the 4th International Workshop on Policies for Distributed Systems and Networks,2003,26-39.
[106]K. Juszcsyszyn. Verifying enterprise's mandatory access control policies with colored Petri nets. IEEE International Workshops on Infrastructure for Collaborative Enterprise,2003,184-189.
[107]E. C. Lupu, M. Sloman. Conflict in policy-based distributed systems management. IEEE Transactions on Software Engineering, Vol.25, Jun.1999, 852-869.
[108]IEEE guide to software requirements specification. ANSI IEEE std.830.
[109]R. Abbassi, S. Guemara EL Fatmi. An automated validation method for security policies:the Firewall Case. In Proceedings of the 4th International Conference on Information Assurance and Security,2008,291-294.
[110]J.Allen. The CERT Guide To System and Network Security Practices. New York:Addison-Wesley,2001,1-200.
[111]Adel El-Atawy, Khaled Ibrahim. Policy segmentation for intelligent firewall testing. The IEEE Workshop on Secure Network Protocols, Boston, USA, 2005,67-72.
[112]P.Eronen, J.Zitting. An expert system for analyzing firewall rules. In Nordic Workshop on Secure IT System, NOV 2001.
[113]邓文俊,梁意文.防火墙安全策略的语义分析方法.计算机工程与应用,43(26),2007,135-137.
[114]S.Hazehurst. Algorithms for analyzing firewall and router access lists. Technical report trwitscs-1999, Department of Computer Science, University of the Witwatersrand, South Africa, July 1999.
[115]S.Pozo, R.Ceballos, and R.M.Gasca. CSP-based firewall rule set diagnosis using security policies. In Proceedings of the 2nd International conference on availability, reliability and security,2007,723～729.
[116]E.AL-Shaer, H.Hamed. Management and translation of filtering security Policies. In Proceedings of IEEE International Conference on Communications, Vol.1, May 2003,256-260.
[117]E.AL-Shaer, H.Hamed. Firewall policy advisor for anomaly detection and rule editing. In Proceedings of IEEE/IFIP Integrated Management, March 2003:17-30.
[118]E.AL-Shaer, H.Hamed. Firewall policy advisor for anomaly discovery and rule editing. In Proceedings of the 8th International Symposium on Integrated Network Management, Orlando, FL, USA, May.2003,17-30.
[119]E.Al-Shaer, H.H.Hamed. Modeling and management of firewall policies. IEEE Transactions on Network and Service Management,1(1),2004,1-10.
[120]E.Al-Shaer, H.H.Hamed, and M.Hasan. Conflict classification and analysis of distributed firewall policies. IEEE Journal on Selected areas in communication, Vol.23,2005,2069-2084.
[121]A.Harib, S.Suris, and G.Parulkar. Detecting and resolving packet filter conflicts. In Proceedings of IEEE INFOCOM'2000, Mar.2003,1203-1212.
[122]F.Baboescu, G.Vrghese. Fast and scalable conflict detection for packet classifiers. In Proceedings of the 10th IEEE International Conference on Network Protocols,2002,270-279.
[123]Yiwen Liang, Wenjun Deng. Verify consistency between security policy and firewall policy with answer set programming. In Proceedings of the International Conference on Computer Science and Software Engineering, 2008,196-200.