Chinese Journal of Computers   Full Text
Title	A Verification Method of Security Model Based on UML and Model Checking
Authors	CHENG Liang1),2) ZHANG Yang2)
Address	1)(Department of Electronic Engineering and Information Science, University of Science and Technology of China, Hefei 230027) 2)(State Key Laboratory of Information Security， Institute of Software, Chinese Academy of Sciences, Beijing 100190)
Year	2009
Issue	No.4(699—708)
Abstract &   Background	Abstract As the development of security operating system, the formal analysis and verification of the security models has been one of the hottest topics now. A new method to verify the correctness of security models is proposed in this paper based on the study of predecessors’ work, which made use of the Unified Modeling Language (UML) and model checking. This approach first used the UML to specify the security model in the form of finite state machine diagrams and the class diagrams, and then translated these UML diagrams to the input language of model checkers. And it used the model checker to verify the model’s correctness or the violation of security properties for the last step. The authors demonstrate the violation of confidentiality of the DBLP and SLCF model by the new approach. Keywords security operating system; security model; formal verification; model checking; UML Background The work attributes to the project “Security Analysis of Windows Vista Kernel and Operating System Controllability Research”, which is supported by the National High Technology Research and Development Program (863 Program) of China under grant Nos.2007AA01Z465, 2006AA01Z433, 2007AA01Z475, 2007AA01Z414. Since the UML is nowadays widely used in software development and it does not require complicated foundations of mathematics, the UML representation of security model has been adopted in the design and development of software for years. However, the verification of such “UMLized” security policy model is still employing Alloy or USE, which is a lightweight formal tool with poor function and can not deal with the temporal properties and workflow of state machines. In this paper, the authors introduce model checking to the verification of UML representation of security policy model and propose a new method of representing the security model by UML. The approach uses UML class diagrams and state machine diagrams to specify both the static and dynamic properties of security model fully and then translates these diagrams into model checkers’ input language in order to employ model checkers’ power of formal verification. At last, The authors demonstrate our approach’s validity by verifying the confidentiality property of DBLP security model.