W-Sec: a Model-Based Formal Method for Assessing the Impacts of Security Countermeasures

Bastien Sultan (1, 2) , Ludovic Apvrille (1, 2) , Philippe Jaillon (3, 4, 5) , Sophie Coudert (1, 2)

1 LabSoC - System on Chip
2 COMELEC - Département Communications & Electronique
3 Mines Saint-Étienne MSE - École des Mines de Saint-Étienne
4 DSUD - CEA Tech en région Sud
5 CMP-ENSMSE - Centre Microélectronique de Provence - Site Georges Charpak (CMP-GC)

The chapter provides a detailed description of W-Sec, a formal model-based countermeasures' impact assessment method. It also introduces a new formal definition of the two SysML profiles used in SysML-Sec and W-Sec, enabling (i) for the future automation of several W-Sec stages and (ii) for the definition of consistency rules ensuring the consistency of the models written in these two distinct modeling languages. In addition, the chapter evaluates W-Sec with a new industry 4.0 case-study and discusses the strengths and the current limitations of the approach in this new application field.

Keywords: Impact assessment Formal methods Mutations SysML-Sec TTool Cyber-Physical Systems Safety Security Performance; Impact assessment; Formal methods; Mutations; SysML-Sec; TTool; Cyber-Physical Systems; Safety; Security; Performance

Domains: Computer Science [cs]

Bastien Sultan, Ludovic Apvrille, Philippe Jaillon, Sophie Coudert. W-Sec: a Model-Based Formal Method for Assessing the Impacts of Security Countermeasures. Model-Driven Engineering and Software Development, 1708, Springer Nature Switzerland, pp.203-229, 2023, Communications in Computer and Information Science, 978-3-031-38821-7. ⟨10.1007/978-3-031-38821-7_10⟩. ⟨hal-04177250⟩