POSTER: Towards Cyber Resilience of Cyber-Physical Systems using Tiny Twins Fereidoun Moradi* M¨alardalen University V¨aster˚as, Sweden fereidoun.moradi@mdu.se Sara Abbaspour Asadollah M¨alardalen University V¨aster˚as, Sweden sara.abbaspour@mdu.se Marjan Sirjani M¨alardalen University V¨aster˚as, Sweden marjan.sirjani@mdu.se Abstract—We propose a method to detect attacks on sensor data and control commands in cyber-physical systems. We develop a monitor module that uses an abstract digital twin, Tiny Twin, to detect false sensor data and faulty control commands. The Tiny Twin is a state transition system that represents the observable behavior of the system. The monitor observes the sensor data and the control commands transmitted in the network, walks over the Tiny Twin and checks whether the observed data and commands are con- sistent with the transitions in the Tiny Twin. The monitor produces an alarm when an attack is detected. The Tiny Twin is built automatically based on a timed actor code of the system. We demonstrate the method and evaluate it in detecting attacks using a temperature control system. Index Terms—Monitoring, Model Checking, Cyber-Physical Systems, Attack Detection and Prevention, Cyber-Security 1. Introduction Cyber-Physical Systems (CPSs) are safety-critical sys- tems that integrate physical processes in the industrial plants (e.g., thermal power plants or smart water treatment plants) with sensors, actuators and controller components. Since these components are integrated via a communica- tion network (usually wireless), a CPS is vulnerable to malicious cyber-attacks that may cause catastrophic dam- age to the physical infrastructure and processes. Cyber- attacks may be performed over a significant number of attack points and in a coordinated way. So, detecting and preventing attacks in CPSs are of significant importance. Intrusion Detection Systems (IDSs) are deployed in communication networks to defend the system against cyber-attacks. Regular IDSs cannot easily catch complex attacks. They need to be equipped with complicated logic, based on human (safety and security engineers) reason- ing [1]. In rule-based IDSs [1], a set of properties that are extracted from the system design specification are considered as rule-sets to detect attacks. Indeed, if an IDS finds a deviation between the observed packets in the network and the defined rules, it produces an alarm and takes a predefined action such as dropping the packets. The key challenge is the effort required to specify the correct system behavior as rules. 2. Overview We propose a method to detect cyber-attacks on sensor data and control commands in CPSs. The overview of Model Checking (Afra) Abstraction (Abstraction tool) Generate Monitor (LF compiler) Timed Rebeca model State Space Tiny Twin LF code Monitor module + Mapping Rebeca to LF Step (1) Step (2) Step (3) Figure 1: The overview of our method. Step (1), we generate the state space of the Timed Rebeca code of a CPS by the Afra model checker (see Sec. 3). Step (2), the state space is abstracted by our abstraction tool (see Sec. 4). The result of the abstraction is a Tiny Twin that is used within a monitor module (see Sec. 5) to detect the attacks. Step (3), we develop the monitor module in LF language and use the LF compiler to generate an executable file. our method is shown in Figure 1. The model of a CPS is developed in Timed Rebeca [2] and the Afra model checker [3] is used to verify the model (step (1) in Fig- ure 1). In [4], it is shown that how entities of a CPS, i.e., sensors, actuators, controllers, and physical plant are mod- eled as actors, and interactions between them are modeled as messages passed between the actors. We develop an abstraction tool (step (2) in Figure 1) that abstracts the state space of the Timed Rebeca model (generated by Afra model checking tool) to create a Tiny Twin (TT) [5]. Digital Twins (DT) [6] are used as digital representation of the system to advanc