Tag Archives: model checking

We present some research works over the past nine years on applying formal methods to secure cyber-physical systems (CPSs). The presentation will take place at a sufficiently high level of detail and will essentially be divided into three parts. In the first part, we highlight an hybrid process calculus to model both CPSs and physics-based attacks. We formalize a threat model that specifies MITM attacks that can manipulate sensor readings and/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.  We then formalize how to estimate the impact of a successful attack on a CPS and investigate possible quantifications of the success chances of an attack. In the second part, we report a line of work that uses model checking tools and statistical model checking techniques to perform static security analysis of CPSs…

Read more