Measuring Robustness in Cyber-Physical Systems under Sensor Attacks
CoRR(2024)
Abstract
This paper contributes a formal framework for quantitative analysis of
bounded sensor attacks on cyber-physical systems, using the formalism of
differential dynamic logic. Given a precondition and postcondition of a system,
we formalize two quantitative safety notions, quantitative forward and backward
safety, which respectively express (1) how strong the strongest postcondition
of the system is with respect to the specified postcondition, and (2) how
strong the specified precondition is with respect to the weakest precondition
of the system needed to ensure the specified postcondition holds. We introduce
two notions, forward and backward robustness, to characterize the robustness of
a system against sensor attacks as the loss of safety. To reason about
robustness, we introduce two simulation distances, forward and backward
simulation distances, which are defined based on the behavioral distances
between the original system and the system with compromised sensors. Forward
and backward distances, respectively, characterize upper bounds of the degree
of forward and backward safety loss caused by the sensor attacks. We verify the
two simulation distances by expressing them as modalities, i.e., formulas of
differential dynamic logic, and develop an ad-hoc proof system to reason with
such formulas. We showcase our formal notions and reasoning techniques on two
non-trivial case studies: an autonomous vehicle that needs to avoid collision
and a water tank system.
MoreTranslated text
AI Read Science
Must-Reading Tree
Example
![](https://originalfileserver.aminer.cn/sys/aminer/pubs/mrt_preview.jpeg)
Generate MRT to find the research sequence of this paper
Chat Paper
Summary is being generated by the instructions you defined