I report on ongoing work in which we have been applying formal methods to lay and streamline theoretical foundations to reason about Cyber-Physical Systems (CPSs) and physics-based attacks, i.e., attacks targeting physical devices. We focus on a formal treatment of both integrity and denial of service attacks to sensors and actuators of CPSs, and on the timing aspects of these attacks. The contributions of our work are fourfold.
(1) We define a hybrid process calculus to model both CPSs and physics-based attacks.
(2) We formalise a threat model that specifies MITM attacks that can manipulate sensor readings or control commands in order to drive a CPS into an undesired state, and we provide the means to assess attack tolerance/vulnerability with respect to a given attack.
(3) We formalise how to estimate the impact of a successful attack on a CPS and investigate possible quantifications of the success chances of an attack.
(4) We illustrate our definitions and results by formalising a non-trivial running example in Uppaal SMC, the statistical extension of the Uppaal model checker; we use Uppaal SMC as an automatic tool for carrying out a static security analysis of our running example in isolation and when exposed to three different physics-based attacks with different impacts.
Joint work with Ruggero Lanotte, Massimo Merro, Andrei Munteanu, Riccardo Muradore