Integrating Design time and Run time Methods for Detecting Cyber Attacks: Marjan Sirjani
Integrating Design-time and Run-time Methods for Detecting Cyber-Attacks: Marjan Sirjani (Mälardalen University)
In this talk I will explain our method for detecting cyber-attacks on CPS using formal verification at design time, and runtime monitoring during operation. We develop a monitor that uses an abstract digital twin, the so-called Tiny Twin, to detect false sensor data and faulty control commands. The Tiny Twin is a state transition diagram that represents the required behavior of the system, observable from the monitor point of view. We model the components of the system and the physical processes using Rebeca modeling language and use its model checker to generate the state space. The Tiny Twin is built automatically by reducing the state space, keeping the observable behavior of the system, and preserving the trace equivalence. Lingua Franca language is used to develop the system and run the simulations. I show the method using a few case studies. In our future work we will focus on causality and finding the sources of anomalies and vulnerabilities. We will also focus on human interactions with the systems and trustworthiness.
Bio: Marjan Sirjani is a Professor at Mälardalen University, and the leader of Cyber-Physical Systems Analysis research group. Her main research interest is applying formal methods in Software Engineering. She works on modeling and verification of concurrent, distributed, timed, and self-adaptive systems. Marjan and her research group are pioneers in building model checking tools, compositional verification theories, and state-space reduction techniques for actor-based models. She has been working on analyzing actors since 2001 using the modeling language Rebeca (http://www.rebeca-lang.org). Her research is now focused on safety and security assurance and performance evaluation of cyber-physical and autonomous systems. Marjan has been the PC member and PC chair of several international conferences including SEFM, iFM, Coordination, FM, FMICS, SAC, FSEN, and DATE. She is an editor of the journal of Science of Computer Programming.
