We propose 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. Two simulation distances, which respectively characterize upper bounds of the degree of forward and backward safety loss caused by the sensor attacks, are developed to reason with robustness. We verify the two simulation distances by expressing them as formulas of differential dynamic logic and prove the formulas with existing tool support. We showcase an example of an autonomous vehicle that needs to avoid collision.