Formal Modelling of the Impact of Cyber Attacks on Railway Safety

Modern railway signaling extensively relies on wireless communication technologies for efficient operation. The communication infrastructures that they rely on are increasingly based on standardized protocols and are shared with other users. As a result, it has an increased attack surface and is more likely to become the target of cyber attacks that can result in loss of availability and, in the worst case, in safety incidents. While formal modeling of safety properties has a well-established methodology in the railway domain, the consideration of security vulnerabilities and the related threats lacks a framework that would allow a formal treatment. In this paper, we develop a modeling framework for the analysis of the potential of security vulnerabilities to jeopardize safety in communications-based train control for railway signaling, focusing on the recently introduced moving block system. We propose a refinement-based approach enabling a structured and rigorous analysis of the impact of security on system safety.