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.
- 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 ScholarDigital Library
- 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 ScholarDigital Library
- 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 ScholarDigital Library
- 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 ScholarCross Ref
- 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 ScholarDigital Library
- Object Management Group. Unified Modeling Language Specification. OMG, 2001.Google Scholar
- 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 ScholarDigital Library
- 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 ScholarDigital Library
- 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 ScholarDigital Library
- Sachoun Park and Gihwon Kwon. Verification of uml-based security policy model. In ICCSA, pages 973--982, 2005. Google ScholarDigital Library
- 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 ScholarDigital Library
- 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 ScholarDigital Library
- 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 ScholarDigital Library
- 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 ScholarDigital Library
- 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 ScholarDigital Library
- 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 ScholarDigital Library
- Jackson D. Alloy : A lightweight object modeling notation. ACM Transactions on Software Engineering and Methodology, 11(2):256--290, 2002. Google ScholarDigital Library
- 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 Scholar
- G. J. Holzmann. The spin model checker. IEEE Trans. Softw. Eng, 23:279--295, 1997. Google ScholarDigital Library
- 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 ScholarCross Ref
- 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 ScholarDigital Library
- 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 ScholarDigital Library
- 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 Scholar
- 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 ScholarCross Ref
Index Terms
Model checking security policy model using both UML static and dynamic diagrams
Recommendations
Model Checking UML Statechart Diagrams Using JACK
HASE '99: The 4th IEEE International Symposium on High-Assurance Systems EngineeringStatechart Diagrams provide a graphical notation for describing dynamic aspects of system behaviour within the Unified Modeling Language (UML). In this paper we present a branching time model-checking approach to the automatic verification of formal ...
Model Checking UML Activity Diagrams in FDR
ICIS '09: Proceedings of the 2009 Eigth IEEE/ACIS International Conference on Computer and Information ScienceThe Unified Modeling Language (UML) is the de-facto industrial standard for modeling object-oriented software systems. UML Activity diagrams (ADs) can be used for software modeling and they have under gone significant changes with UML 2.0 specification, ...
Model checking dynamic UML consistency
ICFEM'06: Proceedings of the 8th international conference on Formal Methods and Software EngineeringUML is widely accepted and extensively used in software modeling. However, using different diagrams to model different aspects of a system brings the risk of inconsistency among diagrams. In this paper, we investigate an approach to check the ...
Comments