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

Bernardi, S. (Universidad de Zaragoza) ; Gentile, U. ; Marrone, S. ; Merseguer, J. (Universidad de Zaragoza) ; Nardone, R.

Resumen: 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.

Idioma: Inglés

DOI: 10.1016/j.jss.2020.110746

Año: 2021

Publicado en: JOURNAL OF SYSTEMS AND SOFTWARE 171, 110746 (2021), [26 pp]
ISSN: 0164-1212

Factor impacto JCR: 3.514 (2021)

Categ. JCR: COMPUTER SCIENCE, THEORY & METHODS rank: 30 / 111 = 0.27 (2021) - Q2 - T1
Categ. JCR: COMPUTER SCIENCE, SOFTWARE ENGINEERING rank: 29 / 110 = 0.264 (2021) - Q2 - T1

Factor impacto CITESCORE: 8.9 - Computer Science (Q1)

Factor impacto SCIMAGO: 1.418 - Information Systems (Q1) - Hardware and Architecture (Q1)

Financiación: info:eu-repo/grantAgreement/ES/MICIU/Medrese-RTI2018-098543-B-I00

Tipo y forma: Artículo (PostPrint)

Área (Departamento): Área Lenguajes y Sistemas Inf. (Dpto. Informát.Ingenie.Sistms.)