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 paper, we propose a new framework, model driven security framework, for the analysis, design, and evaluation of security properties of 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, Object Constraint Language, Promela, and Spin. Copyright (c) 2015John Wiley & Sons, Ltd.