Model driven security framework for software design and verification

Information system security is receiving increasing attention every day because a security problem can cause serious financial loss or even loss of lives. Some of these security problems occur as a result of poor design practices, where important security functionality is not designed properly and is directly implemented later in the development cycle in an unmethodical way. Researchers have put a great deal of effort into defining processes and tools to design and develop more secure information systems. However, verification of the designed and developed security functionality is of utmost importance. In some cases, designs and codes also need to be formally or semi-formally verified and certified by authorities. The Common Criteria is one of the widely used universal frameworks for evaluating the security functionality of information systems. In this thesis, we propose a new framework, Model Driven Security Framework (MDSF), for the analysis, design and evaluation of security properties of the information systems. Our aim is to support information system developers and evaluation authorities who implement the higher-level Common Criteria (Levels 6 and 7) security assurance process using formal methods based on Unified Modelling Language (UML), Object Constraint Language (OCL), Promela and Spin. With MDSF, we extend UML to support security analysis and design on the UML models of the information system. In addition to UML, we use OCL in MDSF for threat identification, consistency checking among diagrams and security policy enforcement in the design model. We also propose a model transformation and model checking approach to formally verify whether the design model satisfies the security requirements listed in the analysis model.