Security Analysis of a Digital Twin Framework Using Probabilistic Model Checking

Digital Twins (DTs) have been gaining popularity in various applications, such as smart manufacturing, smart energy, smart mobility, and smart healthcare. In simple terms, DT is described as a virtual replica of a given physical product, system, or process. It consists of three major segments: the physical entity, its virtual counterpart, and the connections between them. While the data is collected from a physical entity, processed at the virtual layer, and accessed in the form of a DT at the application layer, it is exposed to several security risks. To ensure the applicability of a DT system, it is imperative to understand these security risks and their implications. However, there is a lack of a framework that can be used to assess the security of a DT. This paper presents a framework in which the security of a DT can be analyzed with the help of a formal verification technique. The framework captures the defense of the system at different layers and considers various attacks at each layer. The security of the DT system is represented as a state-transition system and the security properties are captured in temporal logic. Probabilistic model checking (PMC) is used to verify the systems against these properties. In particular, the framework is used to analyze the probability of success and the cost of various potential attacks that can occur at each layer in a DT system. The applicability of the proposed framework is demonstrated with the help of a detailed case study in the healthcare domain.