Formal Quantitative Tolerance of Cyber-Physical Systems Under Periodic Attacks

Cyber-physical systems are often safety- and security-critical systems with a broad attack surface. Among the diverse range of threats, periodic attacks are a special class of timed attacks in which attack windows and sleep windows alternate over repeated cycles to subtly disrupt system behavior. In this paper, we study the quantitative tolerance of cyber-physical systems under periodic attacks in the formalism of hybrid programs and differential dynamic logic. Building on timed quantitative safety and timed tolerance notions, we introduce a formal framework that: 1) models periodic attacks and their quantitative effects on safety; and 2) determines whether, and to what extent, a system can tolerate such attacks across repeated cycles. We define a notion of periodic quantitative tolerance to characterize how much unsafety a system may experience under periodic attacks while still recovering within bounded time. Finally, we develop proof principles that reduce reasoning about periodic tolerance to reasoning about timed tolerance over one representative cycle or a few cycles, by means of suitable boundary invariants. We illustrate the approach with a water tank case study featuring constant-window, varying-window, and compounding-impact periodic attacks.