基于模型检测的安全操作系统验证方法研究
|
摘要
安全操作系统的形式化验证,作为高等级安全操作系统评估准则的一项重要指标和操作系统安全性能最有效的证明手段,具有重要意义与实用价值。目前形式化验证主要分为模型检测和定理证明两大类方法。本论文集中探讨了模型检测技术在安全操作系统验证各个层次中的一些关键问题,主要工作和创新成果如下:
首先,针对SELinux策略配置复杂难以分析的问题,提出了一种基于模型检测的SELinux策略分析方法,以验证策略实施与安全需求之间的一致性问题。采用扩展的标签迁移系统,将MLS策略和普通TE-RBAC策略的描述融入到统一的描述框架下,并完整定义了策略配置语句的信息流属性,不仅考虑了型访问规则造成的信息流动,也兼顾了型转移以及MLS约束对策略模型信息流的影响。设计了一种新型的安全需求描述语言,将安全需求与和策略配置剥离开,使安全需求的描述不依赖于对实施细节的了解,扩展了模型检测器探索未知漏洞的能力。
其次,提出了安全模型与安全需求的一致性验证方法。利用UML类图和状态机图在系统动、静态建模方面的表达能力,设计了一种新的安全模型UML描述方式。并在此基础上给出了UML图的状态机语义,将UML模型编译成模型检测器的规范语言,使用模型检测分析安全模型的性能。这一成果使利用自动化工具辅助安全模型的正确性验证成为可能,减少了传统安全模型验证方法中对验证人员形式化理论的过高要求以及繁重的手工推导过程。
最后,探讨了安全验证中测试集的优化问题。提出简并测试集的概念,将测试冗余从状态扩展到状态迁移,将测试集中的冗余归为最小。在此定义的基础上,我们以模型检测作为后端的搜索引擎,给出简并测试集的生成算法。首次讨论了在测试集和系统实现相悖时对测试结果的判定。并据此对算法加以改进,使得在不影响测试集生成的前提下,即使测试失败,测试人员也可以准确地对失败位置进行定位。
As an important index of high-level operating system evaluation criterion,and the most effective proof of the security property of the operating system,formal verification of secure operating system has great significance and practical value.In the current stage,formal verification can be divided mainly into two classes:model checking and theory proving.This thesis focuses on some key issues of model checking,in each hierarchy of the formal verification framework of the secure operating system. The main work and innovations are listed as follows:
Fist,to the problem that SELinux policy configuration is complicated and hard to analyze,a unified information flow analysis of SELinux policies is proposed,which is based on the techniques of model checking.It can be used to verify the coherence of the security requirement and the policy implementations.A labeled transition system is adopted to merge MLS policies and TE-RBAC policies into a unified description framework.A complete definition of information flow property of the policy configuration is given,including the information flow caused by type access rules, type transition rules and especially MLS constraint rules in SELinux policy configuration. Also,a new security requirement description language is designed to strip off the high-level security requirement description from the low-level policy implementation, which makes the requirement representation independent of the detail of policy language and extends the capability to explore unknown vulnerability.
Secondly,a coherence verification of security model and requirement is proposed. In the use of the expression of UML class diagram and state machine diagram in the static and dynamic modeling,a new security model description method of UML is designed.The UMLized model is compiled to model checker's specification language after given the UML diagram's state machine semantics.Then the requirement,which is also translated to the model checker's input,can be checked accordingly against to the security model.This achievement makes it possible to verify the correctness of security model semi-automatically and reduces the high requirement of formal methods and the heavy work in the traditional security model verification.
Finally,about optimization of test sets in the security verification,the concept of degenerate test set is proposed,considering not only the redundant state,but also the state transition.The generation algorithm is represented then.A discussion is made to determine the algorithm's effectiveness when test case fails for the first time. After that,an improved DTS generation algorithm is given,which can show the failure location accurately without affecting the efficiency of the algorithm.
首先,针对SELinux策略配置复杂难以分析的问题,提出了一种基于模型检测的SELinux策略分析方法,以验证策略实施与安全需求之间的一致性问题。采用扩展的标签迁移系统,将MLS策略和普通TE-RBAC策略的描述融入到统一的描述框架下,并完整定义了策略配置语句的信息流属性,不仅考虑了型访问规则造成的信息流动,也兼顾了型转移以及MLS约束对策略模型信息流的影响。设计了一种新型的安全需求描述语言,将安全需求与和策略配置剥离开,使安全需求的描述不依赖于对实施细节的了解,扩展了模型检测器探索未知漏洞的能力。
其次,提出了安全模型与安全需求的一致性验证方法。利用UML类图和状态机图在系统动、静态建模方面的表达能力,设计了一种新的安全模型UML描述方式。并在此基础上给出了UML图的状态机语义,将UML模型编译成模型检测器的规范语言,使用模型检测分析安全模型的性能。这一成果使利用自动化工具辅助安全模型的正确性验证成为可能,减少了传统安全模型验证方法中对验证人员形式化理论的过高要求以及繁重的手工推导过程。
最后,探讨了安全验证中测试集的优化问题。提出简并测试集的概念,将测试冗余从状态扩展到状态迁移,将测试集中的冗余归为最小。在此定义的基础上,我们以模型检测作为后端的搜索引擎,给出简并测试集的生成算法。首次讨论了在测试集和系统实现相悖时对测试结果的判定。并据此对算法加以改进,使得在不影响测试集生成的前提下,即使测试失败,测试人员也可以准确地对失败位置进行定位。
As an important index of high-level operating system evaluation criterion,and the most effective proof of the security property of the operating system,formal verification of secure operating system has great significance and practical value.In the current stage,formal verification can be divided mainly into two classes:model checking and theory proving.This thesis focuses on some key issues of model checking,in each hierarchy of the formal verification framework of the secure operating system. The main work and innovations are listed as follows:
Fist,to the problem that SELinux policy configuration is complicated and hard to analyze,a unified information flow analysis of SELinux policies is proposed,which is based on the techniques of model checking.It can be used to verify the coherence of the security requirement and the policy implementations.A labeled transition system is adopted to merge MLS policies and TE-RBAC policies into a unified description framework.A complete definition of information flow property of the policy configuration is given,including the information flow caused by type access rules, type transition rules and especially MLS constraint rules in SELinux policy configuration. Also,a new security requirement description language is designed to strip off the high-level security requirement description from the low-level policy implementation, which makes the requirement representation independent of the detail of policy language and extends the capability to explore unknown vulnerability.
Secondly,a coherence verification of security model and requirement is proposed. In the use of the expression of UML class diagram and state machine diagram in the static and dynamic modeling,a new security model description method of UML is designed.The UMLized model is compiled to model checker's specification language after given the UML diagram's state machine semantics.Then the requirement,which is also translated to the model checker's input,can be checked accordingly against to the security model.This achievement makes it possible to verify the correctness of security model semi-automatically and reduces the high requirement of formal methods and the heavy work in the traditional security model verification.
Finally,about optimization of test sets in the security verification,the concept of degenerate test set is proposed,considering not only the redundant state,but also the state transition.The generation algorithm is represented then.A discussion is made to determine the algorithm's effectiveness when test case fails for the first time. After that,an improved DTS generation algorithm is given,which can show the failure location accurately without affecting the efficiency of the algorithm.
引文
[1]J.Smith and F.Weingarten.Research challenges for the next generation internent.Technical report,Research Directions for NGI,1997.
[2]Baker,Dixie B.Fortresses built upon sand.In NSPW '96:Proceedings of the 1996 workshop on New security paradigms,volume 0-89791-944-0,pages 148-153.ACM,1996.
[3]P.A.Loscocco,S.D.Smalley,P.A.Muckelbauer,R.C.Taylor,S.J.Turner and J.F.Farrell.The inevitability of failure:the flawed assumption of security in modern computing environments.In Proceedings of the 21th National Information Systmes Security Conference,pages 303-314.ACM,1998.
[4]D.E.Bell and L.J.La Padula.Secure Computer System Unified Exposition and MULTICS Interpretation,Technical Report MTR-2997.MITRE Corporation,Bedford,MA,1976.
[5]K.J.Biba.Integrity considerations for secure computer systems.Technical Report MTR3153,MITRE Corp.,1977.
[6]David Ferraiolo and Richard Kuhn.Role-based access controls.In In 15th NISTINCSC National Computer Security Conference,pages 554-563,Baltimore,MD,Oct 1992.
[7]W.E.Boebert and R.Y.Kain.A pratical alternative to hiearchial integrity policies.In In Proc.8th National Computer Security Conference,pages 18-27.Gaithersburg,MD,1985.
[8]E.McCauley and P.Drognowski..Ksos:The design of a secure operating system.In 1979 NCC AFIPS Conference Proceedings,volume 48,pages 345-353.AFIPS Press,1979.
[9]P.G.Neumann,L.Robinson.Karl N.Levitt.R.S.Boyer,and A.R.Saxena.A provabley secure operating system.Technical report,Stanford Research Institute,1975.
[10]Department of Defense.Trusted computer evaluation criteria(tcsec).Technical report,Department of Defense,USA,1985.
[11]Commission of European Communities.Information technology security evalutation criteria(itsec).Technical report,Office for Official Publications of the European Communities,1991.
[12]International Standards Organization.Common criteria for information technology security evaluation.Technical report,ISO/IEC,1999.
[13]P.Neumann,R.Feiertag,L.Robinson,and K.Levitt.Software development and proofs of multi-level security.In Proc.of 2nd International Conf on Software Engineering,pages 421-428.ACM,Oct 1976.
[14]Walker,,Bruce J.and Kemmerer,,Richard A.and Popek,,Gerald J..Specification and verification of the ucla unix security kernel.Commun.ACM,23(2):118-131,1980.
[15]N.A.Waldhart.The army secure operating system,pages 50-60,May 1990.
[16]O.Sami Saydjari.Lock:An historical perspective.Computer Security Applications Conference,Annual,0:96,2002.
[17]Secure Computing Corp..Dtos formal security policy model.Technical report,DTOS CDRL,1996.
[18]Secure Computing Corp..Dtos formal top level specification report.Technical report,DTOS CDRL,1996.
[20]McLean,J.Twenty years of formal methods.In Proc.of the IEEE Symposium on Security and Privacy.,pages 115-116.IEEE,Jan 1999.
[21]刘克龙,冯登国,石文昌.安全操作系统原理与技术.科学出版社,北京,2004.
[22]Tresys Technology.Apol:SE Policy Tools for SELinux.http://www.tresys.com/selinux/selinuxpolicytools.shtml,2006.
[23]Jaeger,T.,Zhang,X.,and Cacheda,F.Policy management using access control spaces.ACM Trans.Inf Syst.Secur.,6(3):327-364,2003.
[24]Hinrichs,S.,and Naldurg,P.Attack-based domain transition analysis.In In 2nd Annual Security Enhanced Linux Symposium,2006.
[25]Herzog,A.,and Guttman,J.Achieving security goals with security-enhanced linux.Technical report,Mitre Corporation,2002.
[26]Guttman,J.D.,Herzog,A.L.,Ramsdell,J.D.,and Skorupka,C.W.Verifying information flow goals in security-enhanced linux.J.Comput.Secur.,13(1):115 - 134,2005.
[27]Prasad Naldurg,Stefan Schwoon,Sriram Rajamani,John Lambert.Netra::seeing through access control.In Proceedings of the fourth ACM workshop on Formal methods in security,pages 55-66.ACM,2006.
[28]何建波.安全操作系统策略模型的关键问题研究.中国科学院软件研究所,北京,中国,2007.
[29]张阳.高等级安全操作系统测评关键技术研究.PhD thesis,中国科学院软件研究所,北京,中国,2008.
[30]中华人民共和国公安部.中华人民共和国行业标准GA/T 388-2002.计算机信息系统安全等级保护操作系统技术要求.中国标准出版社,北京,中国,2002
[31]G.L(u｜¨)ttgen.Formal verification & its role in testing.Technical Report YCS-2006-400,Department of Computer Science,University of York,England,May 2006.
[32]Morrie Gasser.Building a Secure Computer System.Van Nostrand Reinhold Co.,New York,1988.
[33]石文昌.安全操作系统开发方法的研究与实施.PhD thesis,博士学位论文,中国科学院软件研究所,北京,2001.
[34]梁彬.可信进程机制及相关问题研究.软件学报,14(3):547-552,2003.
[35]武延军.安全操作系统动态策略支持的关键技术研究.PhD thesis,博士学位论文,中国科学院软件研究所,北京,2006.
[36]National Computer Security Center.Glossary of computer security terms(aqua book).Technical report,NCSC-TG004,1988.
[37]M.Bishop.Computer Security:Art and Science.Addison-Wiley,New York,2002.
[38]Elisabeth C.Sullivan.Security Policy Models.Seminar for Computer Security Courses,2001.
[39]C.Payne.Secure policy model,navy handbook for the computer security certification of trusted system,chapter 3.Technical report,NRL Technical Memorandum,1995.
[40]D.E.Bell and L.J.La Padula.Secure Computer Systems:Mathematical Foundations,Rep.FSD-TR-73-278,vol.1.Hanscom AFB,ESD/AFSC,Bedford,MA,1973.
[41]D.E.Bell and L.J.La Padula.Secure Computer Systems:A Mathematical Model,Rep.FSD-TR-73-278,vol.2.Hanscom AFB,ESD/AFSC,Bedford,MA,1973.
[42]D.E.Bell and L.J.La Padula.Secure Computer Systems:A Refinement of the Mathematical Model,,Rep.FSD-TR-73-278,vol.3.Hanscom AFB,ESD/AFSC,Bedford,MA,1974.
[43]D.E.Bell and L.J.La Padula.Secure Computer Systems:Mathematical Foundations and Model,Rep.M74-244.MITRE Corporation,Bedford,MA,1974.
[44]Pal A.Karger.Implementing commercial data integrity with secure capabilities.In In Proceedings of 1988 IEEE Symposium on Security and Privacy,pages 140-146,1988.
[45]E.Stewart Lee.Essays about Computer Security.Cambridge,London,UK,1999.
[46]Carl Landwehr,C.L.Heitmeyer and J.McLean.A security model for military message system.ACM Transactions on Computer Systems,9(3):198-222,198.
[47]F.Cohen.Computer viruses:Theory and experiments.Computer and Security,6:22-35,1987.
[48]Paul A.Karger,Vernon R.Austel and David C.Toll.A New Mandantory Security Policy Combining Securecy and Integrity,Rearch Report RC21717.IBM Corp.,2000.
[49]R.O'Brien and C.Rogers.Developing applications on lock.In In Proc.14th National Computer Security Conference,pages 147-156,Washington DC,Oct 1991.
[50]D.F.Ferraiolo,R.Sandhu,S.Gavrila,D.R.Kuhn and R.Chandramouli.Proposed nist standard for role-based access control.ACM Transactions on Information and System Security,4(3):224-274,2001.
[51]D.R.Kuhn.Mutual exclusion as a means of implementing separation of duty requirements in role based access control systems.In In Proceedings 2nd ACM Workshop on Role based access control,1997.
[52]Serban Gavrila and John Barkley.Formal specification for role based access control user/role and role/role relationship management.In In Proceedings of the 3rd ACM Workshop on Role-Based Access Control,ACM,October 1998.
[53]R.Sandhu,E.J.Coyne,H.L.Feinstein and C.E.Youman.Role-based access control models.IEEE Computer,29(2):38-47,1996.
[54]S.Osborn,R.Sandhu,Q.Munawer.Configuring role-based access control to enforce mandatory and discretionary access control policies.ACM Transactions on Information and System Security,3(2):85-106,2000.
[55]J.Hoffman.Implementing rbac on a type enforced system.In In Proc of 13th Annual Computer Security Application Conference,pages 158-163,Dec 1997.
[56]Michael Huth,Mark Ryan.Logic in Computer Science:Modelling and Reasoning about Systems,2nd edition.Cambridge University Press,London,UK,2004.
[57]Edmund M.Clarke,Jr.Orna Grumberg,Doron A.Peled.Model Cheeking.The MIT Press,London,England,1999.
[58]P.A.Loscocco,S.D.Smalley.Integrating flexible support for security policies into the linux operating system.Technical report,NAI Labs,2001.
[59]Alan Ashton Dickerson.Model and analysis of role-based access control in selinux using description logic.Master's thesis,Informatics and Mathematical Modelling,Technical University of Denmark,DTU,Richard Petersens Plads,Building 321,DK-2800 Kgs.Lyngby,2006.
[60]Harrison,M.A.,Ruzzo,W.L.,and Ullman,J.D.Protection in operating systems.Commun.of the ACM,19(8):461-471,1976.
[61]Lipton,R.J.,and Snyder,L.A linear time algorithm for deciding subject security.J.ACM,24(3):455-464,1977.
[62]Bishop,M.,and Snyder,L.The transfer of information and authority in a protection system.In In Proc.SOSP(1979),pages 45-54.ACM Press,1979.
[63]Beata Sarna-Starosta and Scott D.Stoller.Policy analysis for security-enhanced linux.In In Proceedings of the 2004 Workshop on Issues in the Theory of Security(WITS),pages 1-12.ACM,2004.
[64]Aleks Kissinger Dr.John Hale.Lopol:A deductive database approach to policy analysis and rewriting.In In 2nd Annual Security Enhanced Linux Symposium,2006.
[65]Stephen Smalley,Timothy Fraser.A security policy configuration for the security-enhanced linux.Technical report,NAI Labs,2001.
[66]Hicks,Boniface and Rueda,Sandra and St.Clair,Luke and Jaeger,Trent and McDaniel,Patrick.A logical specification and analysis for selinux mis policy.In SACMAT'07:Proceedings of the 12th ACM symposium on Access control models and technologies,pages 91-100.ACM,2007.
[67]M.Bishop.Computer Security:Art and Science.Addison-Wesley Professional,2003.
[68]David D.Clark and David R.Wilson.A comparison of commercial and military security policies.In In Proc.1987 IEEE Symposium on Security and Privacy,pages 184-194.IEEE Computer Society Press,1987.
[69]Doug Brown,John Levine,Tony Mason.Lex & Yacc(2nd edition).O'Reilly Media,Inc,1995.
[70]A.Cimatti,E.M.Clarke,F.Giunchiglia,and M.Roveri.Nusmv:A new symbolic model verifier.In CAV 9,pages 495^499.Springer-Verlag,1999.
[71]J.E.Tidswell,T.Jaeger.An access control model for simplifying constraint expression.In Proceedings of the 7th ACM conference on Computer and Communications Security,pages 154-163.ACM New York,NY,USA,2000.
[72]M.Koch,F.Parisi-Presicce.Visual specifications of policies and their verification.In Workshop on Fundamental Approaches to Software Engineering,pages 278-293.Springer-Verlog,2003.
[73]Dury.Arnaud,Boroday.Sergiy,Petrenko.Alexandre,Lotz.Volkmar.Formal verification of business workflows and role based access control systems.In The International Conference on Emerging Security Information,Systems,and Technologies(SECUREWARE 2007),pages 201-210.IEEE Computer SOciety Press,Oct 2007.
[74]中华人民共和国公安部.中华人民共和国国家标准GB17859-1999.计算机信息系统安全保护等级划分准则.中国国家质量技术监督局,北京,中国,1999.
[75]Object Management Group.Unified Modeling Language Specification,Version 1.4.OMG,2001.
[76]Sachoun Park,Gihwon Kwon.Policy verification and validation framework based on model checking approach.In Proceedings of International Conference on Computational Science and Its Applications,pages 973-982.Springer,Berlin,May 2005.
[77]Jackson D.Alloy:a lightweight object modeling notation.ACM Transaction on Software.Engineering.Methodology,11(2):256-290,2002.
[78]Richters M.,Gogolla M.Validating uml models and ocl constraints.In First Information Security Practice and Experience Conference(ISPEC 2005),pages 144-155.Spinger-Verlog,May 2005.
[79]Hu Hongxin and Alan Gail-Joon.Enabling verification and conformance testing for access control model.In Proceedings of 13th ACM Symposium on Access Control Models And Technologies(SACMAT).Spinger-Verlog,Jun,11-12 2008.
[80]Alan G.J.and Hu H.Towards realizing a formal rbac model in real systems.In Proceedings of the 12th ACM symposium on Access control models and technologies,pages 215-224.ACM,2007.
[81]Yu Lijun,France Robert and Ray Indrakshi.Scenario-based static analysis of uml behavioral properties.In Proceedings of the 11th International Conference on Model Driven Engineering Languages and Systems.ACM/IEEE,Sept 2008.
[82]Frode Hansen,Vladimir Oleshchuk.Conformance checking of rbac policy and its implementation.In Proceedings of the 3rd International Conference on the Unified Modeling Language(UML 2000),pages 144-155.Spinger-Verlog,May 2005.
[83]G.J.Holzmann.The model checker spin.IEEE Transactions on Software Engineering,23(5):279-295,1997.
[84]Latella D,Majzik I,Massink M.Automatic verification of a behavioural subset of uml statechart diagram using spin model-checker.Formal Aspects of Computing,11(6):637-664,1999.
[85]A.Knapp and Stephan Merz.Model checking and code generation for uml state machines and collaborations.Proc.5th Wsh.Tools for System Design and Verification,Technical Report 2002-11,Institut f(u｜¨)r Informafik,Universit(a｜¨)t Augsburg:59-64,2002.
[86]张频,罗贵明.Uml模型检测方法的研究.计算机应用,27(10):2493-2497,2007.
[87]董威,王戟,齐治昌.Uml statecharts的模型检验方法.软件学报,14(4):750-756,2003.
[88]J.Lilius,I.R Paltor.Foramalising uml state machines for model checking.In Proc.2nd Int.Conf,Unified Modeling Language(UML'99),pages 430-445.Springer-Verlog,1999.
[89]A.Knapp.Semantics of uml state machine.Technical Report 0408,Institut f(u｜¨)r Informatik,Ludwig-Maxilians-Universit(a｜¨)t,M(u｜¨)nchen,2004.
[90]M.Gasser.Building A Security Computer System.Van Nostrand Reinhold Company,New York,1988.
[91]季庆光,卿斯汉,贺也平.一个改进的可动态调节的机密性策略模型.软件学报,15(10):1547-1557,2004.
[92]梁洪亮,孙玉芳,赵庆松,张相锋,孙波.一个安全标记公共框架的设计与实现.软件学报,14(3):547-552,2003.
[93]D.E.Bell and L.J.La Padula.Secure computer system:A retrospective.In Proc.of the 1983 IEEE Symp.on Security and Privacy.,pages 161-162.IEEE Computer Society Press,1983.
[94]Guido Wimmel,Jan Jiirjens.Specification-based test generation for securitycritical systems using mutations.In Proceedings of the 4th International Conference on Formal Engineering Methods:Formal Methods and Software Engineering,pages 471-482.Springer-Verlog,2002.
[95]G.Hamon,L.Moura,and J.Rushby.Generating efficient test sets with a model checker.In Proceedings of the 2nd International Conference on Software Engineering and Formal Methods(SEFM),pages 261-270.IEEE Computer Society Press,2004.
[96]Harry Rudin,Colin H.West,and Pitro Zafiropulo.Automated protocol validation:One chain of development.Computer Networks,2:373-380,1978.
[97]Daniel Geist,Monica Farkas,Avner Landver,Yossi Lichtenstein,Shmuel Ur,Yaron Wolfsthal.Coverage-directed test generation using symbolic techniques.In Proceedings of the First International Conference on Formal Methods in Computer-Aided Design,pages 143-158.Springer-Verlag,1996.
[98]John Callahan,Francis Schneider,Steve Easterbrook.Automated software testing using model-checking.In Technical Report NASA-IVV-96-022.NASA Independent Verification and Validation Facility,Fairmont,WV,Aug 1996.
[99]M.Huth and M.Ryan.Logic in Computer Science:Modeling and Reasoning about Systems.Cambridge University Press,London,2004.
[100]K.L.McMillan.Symbolic Model Checking.Ph.D.Thesis,Carnegie Mellon University,Pittsburgh,1992.
[101]M.P.E.Heimdahl,S.Rayadurgam,W.Visser,G.Devaraj,and J.Gao.Autogenerating test sequences using model checkers:A case study.In 3rd International Workshop on Formal Approaches to Testing of Software(FATES 2003),pages 42-59.Springer-Verlag,2003.
[102]D.Beyer,A.J.Chlipala,T.A.Henzinger,R.Jhala,and R.Majumdar.Generating tests from counterexamples.In Proceedings of the 26th International Conference on Software Engineering(ICSE2004),pages 326-335.IEEE Computer Society Press,2004.
[103]J.Offutt,Y.Xiong,and S.Liu.Criteria for generating specification-based tests.In 1st IEEE Conference on Engineering of Complex Computer Systems,pages 119-129.IEEE Computer Society Press,1999.
[104]E.M.Clarke,E.A.Emerson,and A.P.Sistla.Automatic verification of finitestate concurrent systems using temporal logic specifications.Transactions on Programming Languages and Systems,8(2):244-263,1986.
[105]J.P.Queille and J.Sifakis.Specification and verification of concurrent systems in cesar.In Intl.Symp.on Programming,volume vol.137 of LNCS.Springer-Verlag.
[106]E.P.K.Tsang.Foundations of Constraint Satisfaction.Academic Press,1993.
[107]A.Robinson and A.Voronkov.Handbook of Automated Reasoning.MIT Press,2001.
[108]E.M.Clarke,J.M.Wing.Formal methods:State of the art and future directions.ACM Computing Surveys,28(4):626-643,1996.
[109]T.A.Henzinger,R.Jhala,R.Majumdar,and G.Sutre.Software verification with blast.In SPIN 2003,pages 235-239.Springer-Verlog,2003.
[110]T.Ball and S.K.Rajamani.Automatically validating temporal safety properties of interfaces.In SPIN 2001,pages 103-122.Springer-Verlog,2001.
[111]J.Callahan,F.Schneider,and S.Easterbrook.Automated software testing using model-checking.In SPIN 1996,pages 118-127.Rutgers Univ.,1996.
[112]H.S.Hong,I.Lee,O.Sokolsky,and S.D.Cha.Automatic test generation from statechart using model checking.In FATES '01,vol.NS-01-4 of BRICS Notes Series,pages 15-30.BRICS,2001.
[113]A.Gargantini and C.Heitmeyer.Using model checking to generate tests from requirements specifications.In ESEC '99,vol.1687 of LNCS,pages 146-162.Springer-Verlag,1999.
[114]P.E.Ammann and P.E.Black.Test generation and recognition with formal methods.In Intl.Workshop on Automated Program Analysis,Testing and Verification,pages 64-67,2000.
[115]A.Engels,L.M.G.Feijs,and S.Mauw.Test generation for intelligent networks using model checking.In TACAS '97,vol.1217 of LNCS.Springer-Verlag,1997.
[116]R.de Vries and J.Tretmans.On-the-fly conformance testing using spin.Software Tools for Technology Transfer,2(4):382-393,2000.
[117]M.Jean Harrold,Rajiv Gupta,Mary Lou Soffa.A methodology for controlling the size of a test suite.ACM Transactions on Software Engineering and Methodology(TOSEM),2(3):270-285,1993.
[118]聂长海,徐宝文.一种最小测试集生成方法.计算机学报,26(12):1690-1695,2003.
[119]H.S.Hong,S.D.Cha,I.Lee,O.Sokolsky,and H.Ural.Data flow testing as model checking.In Proceedings of 25th International Conference on Software Engineering,pages 232-242.IEEE Computer Society Press,2003.
[120]Zeng.Hongwei,Miao.Huaikou,Liu.Jing.Specification-based test generation and optimization using model checking.In 1st Joint IEEE/IFIP Symposium on Theoretical Aspects of Software Engineering,pages 349-355.IEEE Computer Society Press,2007.
[121]章晓芳,徐宝文,聂长海,史亮.一种基于测试需求约简的测试集优化方法,软件学报,18(4):821-831,2007.
[2]Baker,Dixie B.Fortresses built upon sand.In NSPW '96:Proceedings of the 1996 workshop on New security paradigms,volume 0-89791-944-0,pages 148-153.ACM,1996.
[3]P.A.Loscocco,S.D.Smalley,P.A.Muckelbauer,R.C.Taylor,S.J.Turner and J.F.Farrell.The inevitability of failure:the flawed assumption of security in modern computing environments.In Proceedings of the 21th National Information Systmes Security Conference,pages 303-314.ACM,1998.
[4]D.E.Bell and L.J.La Padula.Secure Computer System Unified Exposition and MULTICS Interpretation,Technical Report MTR-2997.MITRE Corporation,Bedford,MA,1976.
[5]K.J.Biba.Integrity considerations for secure computer systems.Technical Report MTR3153,MITRE Corp.,1977.
[6]David Ferraiolo and Richard Kuhn.Role-based access controls.In In 15th NISTINCSC National Computer Security Conference,pages 554-563,Baltimore,MD,Oct 1992.
[7]W.E.Boebert and R.Y.Kain.A pratical alternative to hiearchial integrity policies.In In Proc.8th National Computer Security Conference,pages 18-27.Gaithersburg,MD,1985.
[8]E.McCauley and P.Drognowski..Ksos:The design of a secure operating system.In 1979 NCC AFIPS Conference Proceedings,volume 48,pages 345-353.AFIPS Press,1979.
[9]P.G.Neumann,L.Robinson.Karl N.Levitt.R.S.Boyer,and A.R.Saxena.A provabley secure operating system.Technical report,Stanford Research Institute,1975.
[10]Department of Defense.Trusted computer evaluation criteria(tcsec).Technical report,Department of Defense,USA,1985.
[11]Commission of European Communities.Information technology security evalutation criteria(itsec).Technical report,Office for Official Publications of the European Communities,1991.
[12]International Standards Organization.Common criteria for information technology security evaluation.Technical report,ISO/IEC,1999.
[13]P.Neumann,R.Feiertag,L.Robinson,and K.Levitt.Software development and proofs of multi-level security.In Proc.of 2nd International Conf on Software Engineering,pages 421-428.ACM,Oct 1976.
[14]Walker,,Bruce J.and Kemmerer,,Richard A.and Popek,,Gerald J..Specification and verification of the ucla unix security kernel.Commun.ACM,23(2):118-131,1980.
[15]N.A.Waldhart.The army secure operating system,pages 50-60,May 1990.
[16]O.Sami Saydjari.Lock:An historical perspective.Computer Security Applications Conference,Annual,0:96,2002.
[17]Secure Computing Corp..Dtos formal security policy model.Technical report,DTOS CDRL,1996.
[18]Secure Computing Corp..Dtos formal top level specification report.Technical report,DTOS CDRL,1996.
[20]McLean,J.Twenty years of formal methods.In Proc.of the IEEE Symposium on Security and Privacy.,pages 115-116.IEEE,Jan 1999.
[21]刘克龙,冯登国,石文昌.安全操作系统原理与技术.科学出版社,北京,2004.
[22]Tresys Technology.Apol:SE Policy Tools for SELinux.http://www.tresys.com/selinux/selinuxpolicytools.shtml,2006.
[23]Jaeger,T.,Zhang,X.,and Cacheda,F.Policy management using access control spaces.ACM Trans.Inf Syst.Secur.,6(3):327-364,2003.
[24]Hinrichs,S.,and Naldurg,P.Attack-based domain transition analysis.In In 2nd Annual Security Enhanced Linux Symposium,2006.
[25]Herzog,A.,and Guttman,J.Achieving security goals with security-enhanced linux.Technical report,Mitre Corporation,2002.
[26]Guttman,J.D.,Herzog,A.L.,Ramsdell,J.D.,and Skorupka,C.W.Verifying information flow goals in security-enhanced linux.J.Comput.Secur.,13(1):115 - 134,2005.
[27]Prasad Naldurg,Stefan Schwoon,Sriram Rajamani,John Lambert.Netra::seeing through access control.In Proceedings of the fourth ACM workshop on Formal methods in security,pages 55-66.ACM,2006.
[28]何建波.安全操作系统策略模型的关键问题研究.中国科学院软件研究所,北京,中国,2007.
[29]张阳.高等级安全操作系统测评关键技术研究.PhD thesis,中国科学院软件研究所,北京,中国,2008.
[30]中华人民共和国公安部.中华人民共和国行业标准GA/T 388-2002.计算机信息系统安全等级保护操作系统技术要求.中国标准出版社,北京,中国,2002
[31]G.L(u｜¨)ttgen.Formal verification & its role in testing.Technical Report YCS-2006-400,Department of Computer Science,University of York,England,May 2006.
[32]Morrie Gasser.Building a Secure Computer System.Van Nostrand Reinhold Co.,New York,1988.
[33]石文昌.安全操作系统开发方法的研究与实施.PhD thesis,博士学位论文,中国科学院软件研究所,北京,2001.
[34]梁彬.可信进程机制及相关问题研究.软件学报,14(3):547-552,2003.
[35]武延军.安全操作系统动态策略支持的关键技术研究.PhD thesis,博士学位论文,中国科学院软件研究所,北京,2006.
[36]National Computer Security Center.Glossary of computer security terms(aqua book).Technical report,NCSC-TG004,1988.
[37]M.Bishop.Computer Security:Art and Science.Addison-Wiley,New York,2002.
[38]Elisabeth C.Sullivan.Security Policy Models.Seminar for Computer Security Courses,2001.
[39]C.Payne.Secure policy model,navy handbook for the computer security certification of trusted system,chapter 3.Technical report,NRL Technical Memorandum,1995.
[40]D.E.Bell and L.J.La Padula.Secure Computer Systems:Mathematical Foundations,Rep.FSD-TR-73-278,vol.1.Hanscom AFB,ESD/AFSC,Bedford,MA,1973.
[41]D.E.Bell and L.J.La Padula.Secure Computer Systems:A Mathematical Model,Rep.FSD-TR-73-278,vol.2.Hanscom AFB,ESD/AFSC,Bedford,MA,1973.
[42]D.E.Bell and L.J.La Padula.Secure Computer Systems:A Refinement of the Mathematical Model,,Rep.FSD-TR-73-278,vol.3.Hanscom AFB,ESD/AFSC,Bedford,MA,1974.
[43]D.E.Bell and L.J.La Padula.Secure Computer Systems:Mathematical Foundations and Model,Rep.M74-244.MITRE Corporation,Bedford,MA,1974.
[44]Pal A.Karger.Implementing commercial data integrity with secure capabilities.In In Proceedings of 1988 IEEE Symposium on Security and Privacy,pages 140-146,1988.
[45]E.Stewart Lee.Essays about Computer Security.Cambridge,London,UK,1999.
[46]Carl Landwehr,C.L.Heitmeyer and J.McLean.A security model for military message system.ACM Transactions on Computer Systems,9(3):198-222,198.
[47]F.Cohen.Computer viruses:Theory and experiments.Computer and Security,6:22-35,1987.
[48]Paul A.Karger,Vernon R.Austel and David C.Toll.A New Mandantory Security Policy Combining Securecy and Integrity,Rearch Report RC21717.IBM Corp.,2000.
[49]R.O'Brien and C.Rogers.Developing applications on lock.In In Proc.14th National Computer Security Conference,pages 147-156,Washington DC,Oct 1991.
[50]D.F.Ferraiolo,R.Sandhu,S.Gavrila,D.R.Kuhn and R.Chandramouli.Proposed nist standard for role-based access control.ACM Transactions on Information and System Security,4(3):224-274,2001.
[51]D.R.Kuhn.Mutual exclusion as a means of implementing separation of duty requirements in role based access control systems.In In Proceedings 2nd ACM Workshop on Role based access control,1997.
[52]Serban Gavrila and John Barkley.Formal specification for role based access control user/role and role/role relationship management.In In Proceedings of the 3rd ACM Workshop on Role-Based Access Control,ACM,October 1998.
[53]R.Sandhu,E.J.Coyne,H.L.Feinstein and C.E.Youman.Role-based access control models.IEEE Computer,29(2):38-47,1996.
[54]S.Osborn,R.Sandhu,Q.Munawer.Configuring role-based access control to enforce mandatory and discretionary access control policies.ACM Transactions on Information and System Security,3(2):85-106,2000.
[55]J.Hoffman.Implementing rbac on a type enforced system.In In Proc of 13th Annual Computer Security Application Conference,pages 158-163,Dec 1997.
[56]Michael Huth,Mark Ryan.Logic in Computer Science:Modelling and Reasoning about Systems,2nd edition.Cambridge University Press,London,UK,2004.
[57]Edmund M.Clarke,Jr.Orna Grumberg,Doron A.Peled.Model Cheeking.The MIT Press,London,England,1999.
[58]P.A.Loscocco,S.D.Smalley.Integrating flexible support for security policies into the linux operating system.Technical report,NAI Labs,2001.
[59]Alan Ashton Dickerson.Model and analysis of role-based access control in selinux using description logic.Master's thesis,Informatics and Mathematical Modelling,Technical University of Denmark,DTU,Richard Petersens Plads,Building 321,DK-2800 Kgs.Lyngby,2006.
[60]Harrison,M.A.,Ruzzo,W.L.,and Ullman,J.D.Protection in operating systems.Commun.of the ACM,19(8):461-471,1976.
[61]Lipton,R.J.,and Snyder,L.A linear time algorithm for deciding subject security.J.ACM,24(3):455-464,1977.
[62]Bishop,M.,and Snyder,L.The transfer of information and authority in a protection system.In In Proc.SOSP(1979),pages 45-54.ACM Press,1979.
[63]Beata Sarna-Starosta and Scott D.Stoller.Policy analysis for security-enhanced linux.In In Proceedings of the 2004 Workshop on Issues in the Theory of Security(WITS),pages 1-12.ACM,2004.
[64]Aleks Kissinger Dr.John Hale.Lopol:A deductive database approach to policy analysis and rewriting.In In 2nd Annual Security Enhanced Linux Symposium,2006.
[65]Stephen Smalley,Timothy Fraser.A security policy configuration for the security-enhanced linux.Technical report,NAI Labs,2001.
[66]Hicks,Boniface and Rueda,Sandra and St.Clair,Luke and Jaeger,Trent and McDaniel,Patrick.A logical specification and analysis for selinux mis policy.In SACMAT'07:Proceedings of the 12th ACM symposium on Access control models and technologies,pages 91-100.ACM,2007.
[67]M.Bishop.Computer Security:Art and Science.Addison-Wesley Professional,2003.
[68]David D.Clark and David R.Wilson.A comparison of commercial and military security policies.In In Proc.1987 IEEE Symposium on Security and Privacy,pages 184-194.IEEE Computer Society Press,1987.
[69]Doug Brown,John Levine,Tony Mason.Lex & Yacc(2nd edition).O'Reilly Media,Inc,1995.
[70]A.Cimatti,E.M.Clarke,F.Giunchiglia,and M.Roveri.Nusmv:A new symbolic model verifier.In CAV 9,pages 495^499.Springer-Verlag,1999.
[71]J.E.Tidswell,T.Jaeger.An access control model for simplifying constraint expression.In Proceedings of the 7th ACM conference on Computer and Communications Security,pages 154-163.ACM New York,NY,USA,2000.
[72]M.Koch,F.Parisi-Presicce.Visual specifications of policies and their verification.In Workshop on Fundamental Approaches to Software Engineering,pages 278-293.Springer-Verlog,2003.
[73]Dury.Arnaud,Boroday.Sergiy,Petrenko.Alexandre,Lotz.Volkmar.Formal verification of business workflows and role based access control systems.In The International Conference on Emerging Security Information,Systems,and Technologies(SECUREWARE 2007),pages 201-210.IEEE Computer SOciety Press,Oct 2007.
[74]中华人民共和国公安部.中华人民共和国国家标准GB17859-1999.计算机信息系统安全保护等级划分准则.中国国家质量技术监督局,北京,中国,1999.
[75]Object Management Group.Unified Modeling Language Specification,Version 1.4.OMG,2001.
[76]Sachoun Park,Gihwon Kwon.Policy verification and validation framework based on model checking approach.In Proceedings of International Conference on Computational Science and Its Applications,pages 973-982.Springer,Berlin,May 2005.
[77]Jackson D.Alloy:a lightweight object modeling notation.ACM Transaction on Software.Engineering.Methodology,11(2):256-290,2002.
[78]Richters M.,Gogolla M.Validating uml models and ocl constraints.In First Information Security Practice and Experience Conference(ISPEC 2005),pages 144-155.Spinger-Verlog,May 2005.
[79]Hu Hongxin and Alan Gail-Joon.Enabling verification and conformance testing for access control model.In Proceedings of 13th ACM Symposium on Access Control Models And Technologies(SACMAT).Spinger-Verlog,Jun,11-12 2008.
[80]Alan G.J.and Hu H.Towards realizing a formal rbac model in real systems.In Proceedings of the 12th ACM symposium on Access control models and technologies,pages 215-224.ACM,2007.
[81]Yu Lijun,France Robert and Ray Indrakshi.Scenario-based static analysis of uml behavioral properties.In Proceedings of the 11th International Conference on Model Driven Engineering Languages and Systems.ACM/IEEE,Sept 2008.
[82]Frode Hansen,Vladimir Oleshchuk.Conformance checking of rbac policy and its implementation.In Proceedings of the 3rd International Conference on the Unified Modeling Language(UML 2000),pages 144-155.Spinger-Verlog,May 2005.
[83]G.J.Holzmann.The model checker spin.IEEE Transactions on Software Engineering,23(5):279-295,1997.
[84]Latella D,Majzik I,Massink M.Automatic verification of a behavioural subset of uml statechart diagram using spin model-checker.Formal Aspects of Computing,11(6):637-664,1999.
[85]A.Knapp and Stephan Merz.Model checking and code generation for uml state machines and collaborations.Proc.5th Wsh.Tools for System Design and Verification,Technical Report 2002-11,Institut f(u｜¨)r Informafik,Universit(a｜¨)t Augsburg:59-64,2002.
[86]张频,罗贵明.Uml模型检测方法的研究.计算机应用,27(10):2493-2497,2007.
[87]董威,王戟,齐治昌.Uml statecharts的模型检验方法.软件学报,14(4):750-756,2003.
[88]J.Lilius,I.R Paltor.Foramalising uml state machines for model checking.In Proc.2nd Int.Conf,Unified Modeling Language(UML'99),pages 430-445.Springer-Verlog,1999.
[89]A.Knapp.Semantics of uml state machine.Technical Report 0408,Institut f(u｜¨)r Informatik,Ludwig-Maxilians-Universit(a｜¨)t,M(u｜¨)nchen,2004.
[90]M.Gasser.Building A Security Computer System.Van Nostrand Reinhold Company,New York,1988.
[91]季庆光,卿斯汉,贺也平.一个改进的可动态调节的机密性策略模型.软件学报,15(10):1547-1557,2004.
[92]梁洪亮,孙玉芳,赵庆松,张相锋,孙波.一个安全标记公共框架的设计与实现.软件学报,14(3):547-552,2003.
[93]D.E.Bell and L.J.La Padula.Secure computer system:A retrospective.In Proc.of the 1983 IEEE Symp.on Security and Privacy.,pages 161-162.IEEE Computer Society Press,1983.
[94]Guido Wimmel,Jan Jiirjens.Specification-based test generation for securitycritical systems using mutations.In Proceedings of the 4th International Conference on Formal Engineering Methods:Formal Methods and Software Engineering,pages 471-482.Springer-Verlog,2002.
[95]G.Hamon,L.Moura,and J.Rushby.Generating efficient test sets with a model checker.In Proceedings of the 2nd International Conference on Software Engineering and Formal Methods(SEFM),pages 261-270.IEEE Computer Society Press,2004.
[96]Harry Rudin,Colin H.West,and Pitro Zafiropulo.Automated protocol validation:One chain of development.Computer Networks,2:373-380,1978.
[97]Daniel Geist,Monica Farkas,Avner Landver,Yossi Lichtenstein,Shmuel Ur,Yaron Wolfsthal.Coverage-directed test generation using symbolic techniques.In Proceedings of the First International Conference on Formal Methods in Computer-Aided Design,pages 143-158.Springer-Verlag,1996.
[98]John Callahan,Francis Schneider,Steve Easterbrook.Automated software testing using model-checking.In Technical Report NASA-IVV-96-022.NASA Independent Verification and Validation Facility,Fairmont,WV,Aug 1996.
[99]M.Huth and M.Ryan.Logic in Computer Science:Modeling and Reasoning about Systems.Cambridge University Press,London,2004.
[100]K.L.McMillan.Symbolic Model Checking.Ph.D.Thesis,Carnegie Mellon University,Pittsburgh,1992.
[101]M.P.E.Heimdahl,S.Rayadurgam,W.Visser,G.Devaraj,and J.Gao.Autogenerating test sequences using model checkers:A case study.In 3rd International Workshop on Formal Approaches to Testing of Software(FATES 2003),pages 42-59.Springer-Verlag,2003.
[102]D.Beyer,A.J.Chlipala,T.A.Henzinger,R.Jhala,and R.Majumdar.Generating tests from counterexamples.In Proceedings of the 26th International Conference on Software Engineering(ICSE2004),pages 326-335.IEEE Computer Society Press,2004.
[103]J.Offutt,Y.Xiong,and S.Liu.Criteria for generating specification-based tests.In 1st IEEE Conference on Engineering of Complex Computer Systems,pages 119-129.IEEE Computer Society Press,1999.
[104]E.M.Clarke,E.A.Emerson,and A.P.Sistla.Automatic verification of finitestate concurrent systems using temporal logic specifications.Transactions on Programming Languages and Systems,8(2):244-263,1986.
[105]J.P.Queille and J.Sifakis.Specification and verification of concurrent systems in cesar.In Intl.Symp.on Programming,volume vol.137 of LNCS.Springer-Verlag.
[106]E.P.K.Tsang.Foundations of Constraint Satisfaction.Academic Press,1993.
[107]A.Robinson and A.Voronkov.Handbook of Automated Reasoning.MIT Press,2001.
[108]E.M.Clarke,J.M.Wing.Formal methods:State of the art and future directions.ACM Computing Surveys,28(4):626-643,1996.
[109]T.A.Henzinger,R.Jhala,R.Majumdar,and G.Sutre.Software verification with blast.In SPIN 2003,pages 235-239.Springer-Verlog,2003.
[110]T.Ball and S.K.Rajamani.Automatically validating temporal safety properties of interfaces.In SPIN 2001,pages 103-122.Springer-Verlog,2001.
[111]J.Callahan,F.Schneider,and S.Easterbrook.Automated software testing using model-checking.In SPIN 1996,pages 118-127.Rutgers Univ.,1996.
[112]H.S.Hong,I.Lee,O.Sokolsky,and S.D.Cha.Automatic test generation from statechart using model checking.In FATES '01,vol.NS-01-4 of BRICS Notes Series,pages 15-30.BRICS,2001.
[113]A.Gargantini and C.Heitmeyer.Using model checking to generate tests from requirements specifications.In ESEC '99,vol.1687 of LNCS,pages 146-162.Springer-Verlag,1999.
[114]P.E.Ammann and P.E.Black.Test generation and recognition with formal methods.In Intl.Workshop on Automated Program Analysis,Testing and Verification,pages 64-67,2000.
[115]A.Engels,L.M.G.Feijs,and S.Mauw.Test generation for intelligent networks using model checking.In TACAS '97,vol.1217 of LNCS.Springer-Verlag,1997.
[116]R.de Vries and J.Tretmans.On-the-fly conformance testing using spin.Software Tools for Technology Transfer,2(4):382-393,2000.
[117]M.Jean Harrold,Rajiv Gupta,Mary Lou Soffa.A methodology for controlling the size of a test suite.ACM Transactions on Software Engineering and Methodology(TOSEM),2(3):270-285,1993.
[118]聂长海,徐宝文.一种最小测试集生成方法.计算机学报,26(12):1690-1695,2003.
[119]H.S.Hong,S.D.Cha,I.Lee,O.Sokolsky,and H.Ural.Data flow testing as model checking.In Proceedings of 25th International Conference on Software Engineering,pages 232-242.IEEE Computer Society Press,2003.
[120]Zeng.Hongwei,Miao.Huaikou,Liu.Jing.Specification-based test generation and optimization using model checking.In 1st Joint IEEE/IFIP Symposium on Theoretical Aspects of Software Engineering,pages 349-355.IEEE Computer Society Press,2007.
[121]章晓芳,徐宝文,聂长海,史亮.一种基于测试需求约简的测试集优化方法,软件学报,18(4):821-831,2007.