Formal Analysis of Interactions Between Safety and Security Requirements

Modern safety-critical control systems rely on networking to provide safety-critical functions. Network technologies not only offers a variety of benefits but also introduces cybersecurity threats. Exploiting security vulnerabilities might result in a loss of control and situation awareness as well as directly threaten safety. Therefore, the development of safety-critical systems should encompass a systematic analysis of the impact of potential cyberattacks on safety and explicit identification of security requirements early in the system development life cycle. In this paper, we propose a formal approach to modelling networked safety-critical systems within Event-B framework. We demonstrate how modelling and refinement in Event-B can systematically identify mutual interdependencies between safety and security and facilitate deriving explicit security requirements necessary for achieving system safety.