Portal de Periódicos da CAPES

Transformation-Based Approach to Security Verification for Cyber-Physical Systems

2019; Institute of Electrical and Electronics Engineers; Volume: 13; Issue: 4 Linguagem: Inglês

10.1109/jsyst.2019.2923818

2373-7816

Saoussen Mili, Nga Nguyen, Rachid Chelouah,

Advanced Software Engineering Methodologies

The increasing complexity of cyber-physical systems motivates new modeling approaches to ensure system security right from the design process. In this paper, we present a model-based approach to formally validate communicating systems against cyber-attacks. Security requirements are modeled by using the unified modeling language (UML) extended attack tree profile with temporal logic operators. Moreover, to identify attack propagation, another UML profile, i.e., the connectivity profile, has been integrated to model interactions between system components. In order to carry out a formal verification of the system, a transformation platform that automatically generates a new symbolic model verifier code from systems modeling language (SysML) models for both static and dynamic aspects has been developed. The modeling and validation process is illustrated via two case studies on connected cars: 2014 Jeep Cherokee attack and 2016 Tesla Model S attack.