基于策略的信息安全模型及形式化建模的研究
|
摘要
安全模型(Security model)准确描述安全的重要方面及其与系统行为的关系，
建立安全模型的主要目的是提高对成功实现关键安全需求的理解层次。安全策略在
确定安全模型的内容上扮演了非常重要的角色，所以成功开发一个好的安全模型需
要一个清晰的、全面的安全策略。尤其重要的是，系统的构成必须确保它所支持的
安全策略的一致。但是当前并没有严格的和系统的方法来预测和保证安全系统设计
中这些重要的特性。
本论文以信息系统的安全和网络安全为出发点，对安全系统的形式化开发方
法、信息安全模型展开了深入的研究。首先对现有的安全模型进行了深入的分析后，
得出了基于策略的信息安全模型。在模型的正式描述中，往往需要通过适当的数学
方法来达到准确描述和分析的目的。本文提出了一个模拟安全系统体系结构并验证
所需的安全限制是否与组件的构成得到保证的一个方法，通过安全限制模式的概
念，形式化的说明系统所执行的安全策略的一般形式。然后通过时序逻辑(Temporal
Logic，TL)和Petri网这两个形式化描述的工具，对基于策略的安全模型中的访问
控制进行了形式化的描述与验证。TL是一个很流行的形式化描述，最适合描述结果
和限制，而Petri网是很好的操作模型，非常适合分布式系统的建模构成与控制。
最后通过Petri网的性质--可达性分析，验证了安全系统体系下的整体限制模式
与组件限制模式之间的一致性，从而保证早期设计决定的完整性，并为安全系统的
正确执行提供了一个导向的框架。
Security model, which aims at improving understanding of security requirement realization, precisely describe main aspects of security and its relationship with system action. Security policy plays an important role in confirming the content of security model. Therefore successfully developing a perfect security model needs clear and comprehensive policies. In particular, the composition of systems must consistently assure security policies that are supposed to enforce. However, there is currently no rigorous and systematic way to predict and assure such critical properties in security system design.
This paper starts at information system and network security, and focuses on formal developing method of security system and security model. First, after analyzing deeply current security model, policy-based information security model is educed. In formal description, proper mathematics methods are usually needed to insure precise description and analysis. Second, a methodoly, which aims at modeling security architecture and verifying whether required security constraints are assured by the composition of the components, is introduced in this paper. Through the concept of security constraint patterns, the generic form of security policies are formally specified that the system architecture must enforce. Then, temporal logic and Petri net are applied to describe and verify access control in policy-based security model. TL, as a popular descriptive formalism, is best suited for describing rules and constraints. By contrast, Petri net is a well-known operational model well suited for modeling the control and composition of distributed system. Last, the resultant architectural model is verified against the system
wide security constraint patterns using Petri net's analysis techniques--reachability
analysis, which not only ensures the integrity of early design decisions, but also provides a framework to guide correct implementations of the security system design.
建立安全模型的主要目的是提高对成功实现关键安全需求的理解层次。安全策略在
确定安全模型的内容上扮演了非常重要的角色，所以成功开发一个好的安全模型需
要一个清晰的、全面的安全策略。尤其重要的是，系统的构成必须确保它所支持的
安全策略的一致。但是当前并没有严格的和系统的方法来预测和保证安全系统设计
中这些重要的特性。
本论文以信息系统的安全和网络安全为出发点，对安全系统的形式化开发方
法、信息安全模型展开了深入的研究。首先对现有的安全模型进行了深入的分析后，
得出了基于策略的信息安全模型。在模型的正式描述中，往往需要通过适当的数学
方法来达到准确描述和分析的目的。本文提出了一个模拟安全系统体系结构并验证
所需的安全限制是否与组件的构成得到保证的一个方法，通过安全限制模式的概
念，形式化的说明系统所执行的安全策略的一般形式。然后通过时序逻辑(Temporal
Logic，TL)和Petri网这两个形式化描述的工具，对基于策略的安全模型中的访问
控制进行了形式化的描述与验证。TL是一个很流行的形式化描述，最适合描述结果
和限制，而Petri网是很好的操作模型，非常适合分布式系统的建模构成与控制。
最后通过Petri网的性质--可达性分析，验证了安全系统体系下的整体限制模式
与组件限制模式之间的一致性，从而保证早期设计决定的完整性，并为安全系统的
正确执行提供了一个导向的框架。
Security model, which aims at improving understanding of security requirement realization, precisely describe main aspects of security and its relationship with system action. Security policy plays an important role in confirming the content of security model. Therefore successfully developing a perfect security model needs clear and comprehensive policies. In particular, the composition of systems must consistently assure security policies that are supposed to enforce. However, there is currently no rigorous and systematic way to predict and assure such critical properties in security system design.
This paper starts at information system and network security, and focuses on formal developing method of security system and security model. First, after analyzing deeply current security model, policy-based information security model is educed. In formal description, proper mathematics methods are usually needed to insure precise description and analysis. Second, a methodoly, which aims at modeling security architecture and verifying whether required security constraints are assured by the composition of the components, is introduced in this paper. Through the concept of security constraint patterns, the generic form of security policies are formally specified that the system architecture must enforce. Then, temporal logic and Petri net are applied to describe and verify access control in policy-based security model. TL, as a popular descriptive formalism, is best suited for describing rules and constraints. By contrast, Petri net is a well-known operational model well suited for modeling the control and composition of distributed system. Last, the resultant architectural model is verified against the system
wide security constraint patterns using Petri net's analysis techniques--reachability
analysis, which not only ensures the integrity of early design decisions, but also provides a framework to guide correct implementations of the security system design.
引文
[1] 唐冶文 余巍 白英彩．信息安全形式化开发中的模型方法．小型微型计算机系 统，1997，18(9)
[2] J. Leiwo, C. Gamage and Y. Zheng. Organizational Modeling for Efficient Specification of Information Security Requirements. Springer-Verlag Vol.1691, pp.247-260
[3] 黄益民 平玲娣 潘雪增．计算机系统安全模型研究及技术方案设计．计算机研 究与发展，2000
[4] Ravi S. Sandhu, Edward J. Coyne, Hal L. Feinstein and Charles E. Youman. Role-Based Access Control Models. IEEE Computer, 1996,29(2) :38-47
[5] 蒋韬 李信满 刘积仁．信息安全模型研究．小型微型计算机系统，2000，21(10)
[6] 中国信息安全产品测评认证中心．信息安全理论与技术．人民邮电出版社，2003
[7] Sushil Jajodia. Trusted Computer Security Evaluation and Criteria. CMPB465 Data and Computer Security-November 2000
[8] http://www.cesg.gov.uk/assurance/iacs/itsec/cpl/index.cfm
[9] Common Criteria for Information Technology Security Evaluation, 1999
[10] 莫瑞．加瑟著．计算机安全的技术和方法．北京：电子工业出版社，1992，4
[11] Wing J M. A Symbiotic Relationship Between Formai Methods and Security. School of Computer Science, Carnegie Mellon University, Pittsburgh:CMU-CS-98-188,1998
[12] Denning D E. A Lattice Modei of Secure Information Flow. ACM, 1976, 19(5) :236-243
[13] Moskowitz I, Costich 0． A Classical Autom鈚a Approach to Noninterference Type Problem. In: Proc. Of the Computer Security Foundation Workshop V., 1992
[14] LaPadula L J, Bell D E. Secure Computer System: Mathematical Foundations. MITRE Technical Report 2547, Volume Ⅱ,1973
[15] Biba K J. Integrity Considerations for Secure Computer System. The Mitre Corporation, Bedford, MA, Technical Report:TR-3153, 1977
[16] Brewer D F C, Nash M J. The Chinese Wall Security Policy. In: Proc. Of the 1989 IEEE Computer society Symposium on Security abd Privacy. Oakland California. 1989,66-72
[17] H J Schumacher, Sumit Ghosli. A fundamental framework for network security[J]. Journal of Network and Computer Applications, 1997:20:305-322
[18] ISO IS 7498-2． Information Processing System-Open Systems Interconnection Basic Reference Modei-Part 2: Security Architecture[S]. ISO Geneva, Switzerland, 1989
[19] J D Melean. The Specification and Modeling of Computer Security[J]. Computer, 1990
[20] R Sandhu, P Samarati. Authentication, Access Control and Intrusion Detection[M]. The Computer Science and Engineering Handbook, CRC Press, 1997
[21] 冯登国．计算机通信网络安全．清华大学出版社，2001
[22] 冯涛 余冬梅 刘密霞．对象Petri网在信息安全建模中的应用．计算机工程与 应用，2004
[23] 余冬梅 刘密霞 冯涛．网络安全系统设计的研究．微机发展，2004，14(2)
[24] P. Bieber and N. Boulahia-Cuppens, "Formai Verification of Authentication Protocols," Proc. BCS-FACS Sixth Refinement Workshop, 1994
[25] D. Bolignano, "Towards a Mechanization Cryptographic Protocol Verification," Lecture Notes in Computer Science, vol. 1254, p. 131, 1997
[26] 袁崇义．Petri网原理[M]．北京：电子工业出版社，1998
[27] 古天龙 蔡国永．网络协议的形式化分析与设计．电子工业出版社，2003
[28] K. Beznosov and Y. Deng et al. "A Resource Access Decision Service for CORBA-Based Distributed Systems, " Proc. Ann Computer Security Applications Conf., pp. 310-319, 1999
[29] H. J. G. Genrich, "High-Level Nets Fundamentas," Proc. Advances in Petri Nets 1990, pp. 207-247, 1990
[30] http://www. daimi. au. dk/PetriNets
[31] http://jsliu.com/DOC/petri-1． htm
[2] J. Leiwo, C. Gamage and Y. Zheng. Organizational Modeling for Efficient Specification of Information Security Requirements. Springer-Verlag Vol.1691, pp.247-260
[3] 黄益民 平玲娣 潘雪增．计算机系统安全模型研究及技术方案设计．计算机研 究与发展，2000
[4] Ravi S. Sandhu, Edward J. Coyne, Hal L. Feinstein and Charles E. Youman. Role-Based Access Control Models. IEEE Computer, 1996,29(2) :38-47
[5] 蒋韬 李信满 刘积仁．信息安全模型研究．小型微型计算机系统，2000，21(10)
[6] 中国信息安全产品测评认证中心．信息安全理论与技术．人民邮电出版社，2003
[7] Sushil Jajodia. Trusted Computer Security Evaluation and Criteria. CMPB465 Data and Computer Security-November 2000
[8] http://www.cesg.gov.uk/assurance/iacs/itsec/cpl/index.cfm
[9] Common Criteria for Information Technology Security Evaluation, 1999
[10] 莫瑞．加瑟著．计算机安全的技术和方法．北京：电子工业出版社，1992，4
[11] Wing J M. A Symbiotic Relationship Between Formai Methods and Security. School of Computer Science, Carnegie Mellon University, Pittsburgh:CMU-CS-98-188,1998
[12] Denning D E. A Lattice Modei of Secure Information Flow. ACM, 1976, 19(5) :236-243
[13] Moskowitz I, Costich 0． A Classical Autom鈚a Approach to Noninterference Type Problem. In: Proc. Of the Computer Security Foundation Workshop V., 1992
[14] LaPadula L J, Bell D E. Secure Computer System: Mathematical Foundations. MITRE Technical Report 2547, Volume Ⅱ,1973
[15] Biba K J. Integrity Considerations for Secure Computer System. The Mitre Corporation, Bedford, MA, Technical Report:TR-3153, 1977
[16] Brewer D F C, Nash M J. The Chinese Wall Security Policy. In: Proc. Of the 1989 IEEE Computer society Symposium on Security abd Privacy. Oakland California. 1989,66-72
[17] H J Schumacher, Sumit Ghosli. A fundamental framework for network security[J]. Journal of Network and Computer Applications, 1997:20:305-322
[18] ISO IS 7498-2． Information Processing System-Open Systems Interconnection Basic Reference Modei-Part 2: Security Architecture[S]. ISO Geneva, Switzerland, 1989
[19] J D Melean. The Specification and Modeling of Computer Security[J]. Computer, 1990
[20] R Sandhu, P Samarati. Authentication, Access Control and Intrusion Detection[M]. The Computer Science and Engineering Handbook, CRC Press, 1997
[21] 冯登国．计算机通信网络安全．清华大学出版社，2001
[22] 冯涛 余冬梅 刘密霞．对象Petri网在信息安全建模中的应用．计算机工程与 应用，2004
[23] 余冬梅 刘密霞 冯涛．网络安全系统设计的研究．微机发展，2004，14(2)
[24] P. Bieber and N. Boulahia-Cuppens, "Formai Verification of Authentication Protocols," Proc. BCS-FACS Sixth Refinement Workshop, 1994
[25] D. Bolignano, "Towards a Mechanization Cryptographic Protocol Verification," Lecture Notes in Computer Science, vol. 1254, p. 131, 1997
[26] 袁崇义．Petri网原理[M]．北京：电子工业出版社，1998
[27] 古天龙 蔡国永．网络协议的形式化分析与设计．电子工业出版社，2003
[28] K. Beznosov and Y. Deng et al. "A Resource Access Decision Service for CORBA-Based Distributed Systems, " Proc. Ann Computer Security Applications Conf., pp. 310-319, 1999
[29] H. J. G. Genrich, "High-Level Nets Fundamentas," Proc. Advances in Petri Nets 1990, pp. 207-247, 1990
[30] http://www. daimi. au. dk/PetriNets
[31] http://jsliu.com/DOC/petri-1． htm