Formal Robustness for Cyber-Physical Systems Under Timed Attacks

Cyber-physical systems are increasingly deployed in safety-critical applications, making their robustness under adversarial conditions a critical concern. Among the diverse range of threats, timed attacks, i.e., attacks triggered at particular timing, pose a unique challenge due to their ability to disrupt system behaviors in subtle and complex ways. In this paper, we propose a formal framework for quantitative analysis of the robustness of system's safety against timed attacks on cyber-physical systems modeled via the formalism of hybrid programs and differential dynamic logic. We introduce a series of timing related properties to characterize the robustness of safety against timed attacks, and develop a system of reasoning techniques, with a focus on the timing of dynamics, to establish these properties. We showcase the reasoning techniques with a case study on a water tank system with non-trivial dynamics.