Security modelling and formal verification of survivability properties: Application to cyber–physical systems

The modelling and verification of systems security is an open research topic whose complexity and importance needs, in our view, the use of formal and non-formal methods. This paper addresses the modelling of security using misuse cases and the automatic verification of survivability properties using model checking. The survivability of a system characterises its capacity to fulfil its mission (promptly) in the presence of attacks, failures, or accidents, as defined by Ellison. The original contributions of this paper are a methodology and its tool support, through a framework called surreal. The methodology starts from a misuse case specification enriched with UML profile annotations and obtains, as a by-product, a survivability assessment model (SAM). Using predefined queries the survivability properties are proved in the SAM. A total of fourteen properties have been formulated and also implemented in surreal, which encompasses tools to model the security specification, to create the SAM and to prove the properties. Finally, the paper validates the methodology and the framework using a cyber–physical system (CPS) case study, in the automotive field.