Automated Integrated Analysis of Safety-Security Interactions for Railway Systems

Abstract

Over recent years, the number and scale of cyberattacks on safety-critical systems have been rapidly growing. Thus it raised a serious concern over the safety of critical infrastructures such as railway signaling systems. Formal modeling and verification are often used to verify the safety of railway signaling systems. Currently, industry practitioners are willing to utilize their expertise and extend it also to reason about safety in the presence of cyberthreats. This motivated our research on integrating safety and security modeling to analyze the potential ways in which cyberattacks could jeopardize system safety. We developed and automated an integrated approach to combining modeling in SysML and Event-B to support a rigorous integrated analysis of the impact of cyberattacks on system safety. Our approach allows the designers to model the system in SysML and then automatically translate it into Event-B, which formally supports the process of identifying safety requirements that are violated by cyberattacks. The safety requirements are formalized as model invariants and the violated requirements are identified via the failed invariant preservation proof obligations. Such an analysis serves as a basis for the consecutive security analysis aiming at defining security control mechanisms and prioritizing their implementation.

Date
Dec 7, 2023 10:30 AM — 11:30 AM
Event
KTH Railway Group Seminar
Location
Vehicle Engineering Laboratory (VEL), Teknikringen 8
Stockholm,