skip to main content
10.1145/2070425.2070451acmotherconferencesArticle/Chapter ViewAbstractPublication PagessinConference Proceedingsconference-collections
research-article

Model checking security policy model using both UML static and dynamic diagrams

Authors Info & Claims
Published:14 November 2011Publication History

ABSTRACT

An operating system relies heavily on its security model to defend against malicious attacks. It has been one of the hottest research domains for decades to validate security models' correctness by formal methods during the development of security operating systems. However, current studies on the formal verification of security models are sometimes too sophisticated for the developers of operating systems, who are usually not experts in mathematical reasoning and proving. So representing a security model in UML becomes a compromise choice for the developers' verification work during system developing. In this paper, we propose a new method to verify the security policy model against the security goals using model checker SPIN and UML modeling language. Given a security policy model and the security property to be validated, our approach leverages UML class diagrams and statechart diagrams to specify its state model and its state transitions respectively. Then we translate these UML diagrams into the input language of SPIN automatically, as well as the security property. The conformance between the security goal and security model can finally be analyzed by SPIN. We proved the effectiveness of our approach by checking the violation of confidentiality of the DBLP model.

References

  1. J. E. Tidswell and T. Jaeger. An access control model for simplifying constraint expression. In 7th ACM conference on Computer and Communications Security, 2000. Google ScholarGoogle ScholarDigital LibraryDigital Library
  2. M. Koch and F. Parisi-Presicce. Visual specifications of policies and their verification. In Workshop on Fundamental Approaches to Software Engineering. LNCS 2621, 2003. Google ScholarGoogle ScholarDigital LibraryDigital Library
  3. Dury. Arnaud, Boroday. Sergiy, Petrenko. Alexandre, and 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, Oct 2007. Google ScholarGoogle ScholarDigital LibraryDigital Library
  4. M. Drouineaud, A. Luder, and K. Sohr. A role based access control model for agent based control systems. In Proceedings of the IEEE International Conference on Industrial Informatics, 2003.Google ScholarGoogle ScholarCross RefCross Ref
  5. Kathi Fisler, Shriram Krishnamurthi, Leo Meyerovich, and Michael Tschantz. Verification and change impact analysis of access-control policies. In International Conference on Software Engineering (ICSE), 2005. Google ScholarGoogle ScholarDigital LibraryDigital Library
  6. Object Management Group. Unified Modeling Language Specification. OMG, 2001.Google ScholarGoogle Scholar
  7. M. Koch, L. Macini, and F. Parisi-Presicce. Foundations for a graph-based approach to the specification of access control policies. In Proc. of Foundations of Software Science and Computation Structures (FoSSaCS 2001). Lect. Notes in Comp. Sci. Springer, March 2001. Google ScholarGoogle ScholarDigital LibraryDigital Library
  8. Hansen F. and Oleshchuk V. A. Conformance checking of rbac policy and its implementation. In First Information Security Practice and Experience Conference (ISPEC 2005), pages 144--155, 2005. Google ScholarGoogle ScholarDigital LibraryDigital Library
  9. Kikuchi Shinji, Tsuchiya Satoshi, Adachi Motomitsu, and Katsuyama Tsuneo. Policy verification and validation framework based on model checking approach. In Fourth International Conference on Autonomic Computing, pages 1--1, 2007. Google ScholarGoogle ScholarDigital LibraryDigital Library
  10. Sachoun Park and Gihwon Kwon. Verification of uml-based security policy model. In ICCSA, pages 973--982, 2005. Google ScholarGoogle ScholarDigital LibraryDigital Library
  11. Richters M and Gogola M. Validating uml models and ocl constraints. In Proceedings of the 3rd International Conference on the Unified Modeling Language (UML 2000), pages 265--277, York, UK, 2000. Google ScholarGoogle ScholarDigital LibraryDigital Library
  12. Ahn Gail-Joon and Hu Hongxin. Towards realizing a formal rbac modelin real systems. In Proceedings of the 12th ACM Symposium on Access Control Models and Technologies(SACMAT), pages 215--224, New York, USA, 2007. Google ScholarGoogle ScholarDigital LibraryDigital Library
  13. Hu Hongxin and Ahn Gail-Joon. Enabling verification and conformance testing for access control model. In Proceedings of the 13th ACM Symposium on Access Control Models and Technologies(SACMAT), pages 195--204, EstesPark, Colorado, USA, 2008. Google ScholarGoogle ScholarDigital LibraryDigital Library
  14. Yu Lijun, France Robert, and Ray Indrakshi. Scenario-based static analysis of uml behavioral properties. In Proceedings of the ACM/IEEE 11th International Conference on Model Driven Engineering Languages and System, pages 234--248, Toulouse, France, 2008. Google ScholarGoogle ScholarDigital LibraryDigital Library
  15. L. Yu, R. France, I. Ray, and S. Ghosh. A rigorous approach to uncovering security policy violations in uml designs. In Engineering of Complex Computer Systems, 2009 14th IEEE International Conference on, pages 126 --135, june 2009. Google ScholarGoogle ScholarDigital LibraryDigital Library
  16. Wuliang Sun, Robert France, and Indrakshi Ray. Rigorous analysis of uml access control policy models. In IEEE International Symposium on Policies for Distributed Systems and Networks, 2011. Google ScholarGoogle ScholarDigital LibraryDigital Library
  17. Jackson D. Alloy : A lightweight object modeling notation. ACM Transactions on Software Engineering and Methodology, 11(2):256--290, 2002. Google ScholarGoogle ScholarDigital LibraryDigital Library
  18. Ji Qing-Guang and He Ye-Ping Qing Si-Han. An improved dynamically modified confidentiality policies model. Journal of Software, 15(10):1547--1557, 2004.Google ScholarGoogle Scholar
  19. G. J. Holzmann. The spin model checker. IEEE Trans. Softw. Eng, 23:279--295, 1997. Google ScholarGoogle ScholarDigital LibraryDigital Library
  20. Michael Balser, Simon Bäumler, Alexander Knapp, Wolfgang Reif, and Andreas Thums. Interactive verification of uml state machines. In Proc. 6th Int. Conf. Formal Engineering Methods (ICFEM'04), pages 434--448, 2004.Google ScholarGoogle ScholarCross RefCross Ref
  21. Bell D E and La Padula L J. Secure computer system: A retrospective. In Proceedings of the 1983 IEEE Symposium on Security and Privacy, pages 161--162, 1983. Google ScholarGoogle ScholarDigital LibraryDigital Library
  22. Knapp Alexander and Merz Stephan. Model checking and code generation for uml state machines and collaborations. In Proceedings of the 5th Workshop on Tools for System Design and Verification, pages 59--64, 2002. Google ScholarGoogle ScholarDigital LibraryDigital Library
  23. He Jian-Bo. Study on the key issues of security policy models in secure operating system. PhD thesis, Institute of Software, Chinese Academy of Science, Beijing, 2007.Google ScholarGoogle Scholar
  24. Latella D, Majzik I, and 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.Google ScholarGoogle ScholarCross RefCross Ref

Index Terms

  1. Model checking security policy model using both UML static and dynamic diagrams

          Recommendations

          Comments

          Login options

          Check if you have access through your login credentials or your institution to get full access on this article.

          Sign in
          • Published in

            cover image ACM Other conferences
            SIN '11: Proceedings of the 4th international conference on Security of information and networks
            November 2011
            276 pages
            ISBN:9781450310208
            DOI:10.1145/2070425

            Copyright © 2011 ACM

            Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

            Publisher

            Association for Computing Machinery

            New York, NY, United States

            Publication History

            • Published: 14 November 2011

            Permissions

            Request permissions about this article.

            Request Permissions

            Check for updates

            Qualifiers

            • research-article

            Acceptance Rates

            Overall Acceptance Rate102of289submissions,35%

          PDF Format

          View or Download as a PDF file.

          PDF

          eReader

          View online with eReader.

          eReader