Loading Seminars

« All Seminars

  • This seminar has passed.

Formal methodologies to secure cyber-physical systems: from static analysis to runtime enforcement

November 15 (2023) @ 3:00 pm - 4:00 pm

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 that are increasingly complex and therefore exposed to more complex cyber-physical attacks that attempt to bypass different IDSs.

In the third and final part, we move to runtime enforcement techniques to ensure specification compliance in networks of controllers, possibly compromised by colluding malware. We define a synthesis algorithm that, given a set of observable actions and a timed correctness property, returns a monitor that enforces the property during the execution of any (potentially corrupted) controller. Our enforcement enjoys a number of classical properties together with attack mitigation by correcting and suppressing incorrect actions of corrupted controllers and by generating safe actions in full autonomy when the controller under scrutiny is not able to do so in a correct manner.

This is a joint seminar with FM-SEC.

Attendance via Zoom (ID:969 1756 7239, Passcode: 254994)
Livestream via Youtube


November 15 (2023)
3:00 pm - 4:00 pm


Massimo Merro (UniVR)

Massimo Merro graduated with honors in Computer Science from the University of Pisa in 1996. In 2000 he obtained a PhD in Computer Science, with "très honorable avec félicitations du jury" mention, from the Ecole des Mines de Paris, France. From May 2000 to October 2002 he was Research Fellow at the University of Sussex (UK) and the Ecole Polytechnique Fédérale de Lausanne, Switzerland. From November 2016 to October 2022 he held the position of Coordinator of the PhD in Computer Science. Since October 2018 he has been a full professor in Computer Science at the Department of Computer Science of the University of Verona. Massimo Merro's research activity includes formal methods applied to concurrent and distributed languages. In particular, he has worked on process calculi for mobile systems, concurrent and distributed object-oriented languages and formalization of distributed algorithms. More recently, he has been working on semantics foundations and security analysis of cyber-physical systems and smart devices in the context of the Internet of Things paradigm. On these topics, he has taught several classes, tutorials, and industrial courses.

View Presenter Website