K-corruption intermittent attacks for violating the codiagnosability

1 K-Corruption Intermittent Attacks for Violating the Codiagnosability Ruotian Liu, Member, IEEE, Yihui Hu, Agostino Marcello Mangini, Senior Member, IEEE, and Maria Pia Fanti, Fellow, IEEE Abstract—In this work, we address the codiagnosability analysis problem of a networked discrete event system under malicious attacks. The considered system is modeled by a labeled Petri net and is monitored by a series of sites, in which each site possesses its own set of sensors, without requiring communication among sites or to any coordinators. A net is said to be codiagnosable with respect to a fault if at least one site could deduce the occurrence of this fault within finite steps. In this context, we focus on a type of malicious attack that is called stealthy intermittent replacement attack. The stealthiness demands that the corrupted observations should be consistent with the system’s normal behavior, while the intermittent replacement setting entails that the replaced transition labels must be recovered within a bounded of consecutive corrupted observations (called as K-corruption intermittent attack). Particularly, there exists a coordination between attackers that are separately effected on different sites, which holds the same corrupted observation for each common transition under attacks. From an attacker viewpoint, this work aims to design K-corruption intermittent attacks for violating the codiagnosability of systems. For this purpose, we propose an attack automaton to analyze K-corruption intermittent attack for each site, and build a new structure called complete attack graph that is used to analyze all the potential attacked paths. Finally, an algorithm is inferred to obtain the K-corruption intermittent attacks, and examples are given to show the proposed attack strategy. Index Terms—Discrete event system, decentralized structure, Petri net, intermittent attack, codiagnosability. NOMENCLATURE NPetri net. M0Initial marking of a Petri net. NLabeled Petri net (LPN). TuSet of unobservable transitions. ToSet of observable transitions. TfSet of fault transitions. Treg Set of regular unobservable transitions. Tr,a Set of regular unobservable transitions that can be attacked. This work was supported in part by the IN2CCAM project that has received funding from the European Union’s Horizon Europe research and innovation programme under grant agreement No 101076791, and the Natural Science Basic Research Program of Shaanxi Province under Grant 2024JCYBQN-0669. This manuscript reflects only the authors’ views and opinions, neither the European Union nor the European Commission can be considered responsible for them. (Corresponding author: Ruotian Liu.) Ruotian Liu, Agostino Marcello Mangini, and Maria Pia Fanti are with the Department of Electrical and Information Engineering, Polytechnic University of Bari, 70125 Bari, Italy (e-mails: {ruotian.liu, agostinomarcello.mangini, mariapia.fanti}@poliba.it). Yihui Hu is with the School of Automation, Xi’an University of Posts and Telecommunications, 710121 Xi’an, China (e-mail: [email protected]). Tr,u Set of regular unobservable transitions that cannot be attacked. π(σ)Parikh vector of σ. lLabeling function. ljLabeling function of site j. ΣEvent set. ΣjEvent set of site j. Pr,u(σ)Projection of σover Tr,u. GeExtended basis reachability graph (EBRG). JSet of sites in LPN system. MdDead marking. Gεε-BRG: enhanced version of EBRG. Gj ε,n Nonfailure ε-BRG of site j. Uεε-unfolded verifier. AAttack structure. AjAttack structure of site j. ΣAj(t)Set of replaced labels associated with tin terms of Aj. Tj a,s Attackable transitions with respect to Aj. lj aModified labeling function of site j. AjReplacement attack of site j. AAttack tuple. KjMaximum value of consecutive corrupted observation of site j. KRow vector whose j-th element is Kj. Tj aSet of attackable transitions that are associated with different labels with respect to site j. Tj na Set of attackable transitions that hold their original labels with respect to site j. IjInsertion function of site j. I−1 jInverse of insertion function. Pj a,na Projection over Tj a∪Tj na. Pf,j a,na Projection over Tj a∪Tj na ∪Tf. ΦjK-corruption intermittent attack function of site j. ∆jAttack automaton of site j. UcComplete attack graph. Pj a,na Projection over T∪Tj a∪Tj na of site j. Pf a,na Projection over T∪Ta∪Tna. lAj(t)Set of observations when tfires with respect to Aj. I. INTRODUCTION Cyber physical systems (CPSs) integrate sensing, control and networking into physical processes, in which network communication makes the system vulnerable to various network attacks, such as sensor reading corruption and actuator command alteration [1]–[4]. Such attack scenarios of CPSs 2 have attracted much attention in the community of discrete event systems (DESs): mainly concerning the problems of attack detection [5]–[7], attack synthesis [8]–[13], state estimation [14], [15]. This work focuses on the attack synthesis problem for violating the codiagnosability in DESs. Diagnosability is a system property determining whether the occurrence of a fault can be detected within finite steps, and has been studied in the framework of automata [16]– [18] and Petri nets [19]–[24]. In practice, many large complex systems are monitored by a set of sites that consider variable communication delays and errors when transmitting diagnostic information from different sites to a coordinator. It is impossible or very costly to collect all data at a central station. Thus, the information structure of the system is naturally considered to be decentralized, and in practice, there exist two main aspects for the decentralized setting. One is about the notion of decentralized diagnosis involving communication among sites, such as [25]–[27]. The other is the concept of decentralized diagnosis, which does not involve communication among sites. The notion of codiagnosability requires that the occurrence of any fault can be detected by at least one site using its own observations of the system execution within a bounded delay [28]–[31]. To investigate the codiagnosability of the system, this work considers the Protocol 3 in [32] that does not require any coordination between sites. The idea of this work is inspired by recent studies [29], [33] that deal with the codiagnosability analysis or opacity enforcement problem by relabeling transitions or inserting transition labels when no active attack exists. Meanwhile, some studies [34], [35] tackle the problem of robust codiagnosability against sensor failures, guaranteeing the safety and reliability of the systems. Here, we investigate the contrary aspects to codiagnosability enforcement [29] and robust codiagnosability [34]–[36] from an attacker viewpoint. It is motivated by the necessity of design with an attack policy for violating the codiagnosability, which conceals the occurrence of critical faults to compromise the systems. For instance, an intruder attempts to disrupt the bank security system by manipulating the sensor readings in the network communication components. This manipulation is intended to evade the system’s ability to detect faults or trigger alerts, thus rendering the system nondiagnosable under such an attack. As we know, other works investigating the attack synthesis problem focus on different attack objectives. For example, the violation of safety, i.e., all internal strings generated by the system are legal, is considered in [8], [12], while the violation of opacity is studied in [13]. In the aforementioned attack studies, the system observation may be corrupted by the attackers continuously to compromise the system, where the problem of intermittent corruption is not considered in DESs. In fact, intermittent attacks [37] require lower energy cost compared to continuous attacks. On the other hand, attackers exploit intermittent vulnerabilities of the systems, like camera downtime during security personnel shifts or maintenance periods. These intermittent vulnerabilities result in disruptions in the digital trail, making detection more challenging. In this work, we formulate intermittent attack synthesis problem in DESs under the decentralized framework, where the considered attack could last for at most a certain period of time. To do so, we assume that after a bounded number of consecutive corrupted observations under the intermittent attacks, the replaced transition label must be recovered, which leads to a new notion of K-corruption intermittent attack. Particularly, in a decentralized structure, given a transition sequence and a site j, if the transitions have been replaced a given certain Kjtimes consecutively under the attacks, then the next occurrence of a transition that can be attacked should hold its original label. Note that our intermittent setting is inspired by the work [35] that focuses on the robust codiagnosability verification against intermittent or transient sensor failures. However, two main differences exist between our study and the work [35]: i) in terms of problem formulation and solution, we aim to synthesize an intermittent attack strategy for violating the codiagnosability, while paper [35] investigates the problem of robust codiagnosability verification, thus yielding to different solutions; ii) in terms of formalism, the proposed problem is newly addressed in the labeled Petri net (LPN) formalism, where the techniques of basis marking and linear algebra are used to avoid an exhaustive computation of all markings. In addition, work [36] proposes a uniform approach for diagnosis in DESs subject to unreliable sensors, employing linear temporal logic techniques. Such a framework allows for the formulation and inclusion of diagnosability verification problems in terms of K-loss observation setting, but it is not applied for the enforcement or violation of diagnosability. It is noteworthy that the considered attack scenario may compromise observations by inserting, replacing, or removing partial observations within the system. Sensor failure typically results in incorrect or missing observations. Our work complements existing research on attack synthesis problems in DESs, with a particular emphasis on addressing intermittent attacks. By devising such an attack strategy, our aim is to enable engineers to detect potential vulnerabilities from the perspective of an attacker. To tackle the attack synthesis problem, there are mainly several approaches in the literature. The first type of approaches [12], [13] employs a discrete structure to model the game-like interaction between the supervisor and the attacker. Such a game structure incorporates all possible attacks. The second type of approaches transforms the attack synthesis problem into the supervisor synthesis problem [8], [9]. Unlike existing approaches, we introduce a labeling function to model an attack, for making a system non-codiagnosable by using an ε-unfolded verifier structure. Specifically, an attack synthesis requires the existence of a type of path called elementary unsound path that violates the codiagnosability. The classic verifier [29] can only update states when consecutive transition pairs have the same observation, thus it is unable to generate elementary unsound paths. In addition, the classic verifier cannot be applied to intermittent attack synthesis. To solve these issues, we develop a new structure called complete attack graph with the following advantages: (i) it removes the same observation condition of the consecutive transition pair; (ii) it integrates the proposed attack automaton, such that all the potential attacked paths limited to Kconsecutive corruptions are listed. Moreover, unlike the approach in [12], 3 which achieves stealthiness through state pruning, this study identifies stealthy attacks by analyzing the corrupted behavior. Later on, to apply the concept of codiagnosability without deadlock-freeness assumption, we add a self-loop labeled with the empty string εto each determined dead marking. The origin of this concept is derived from the research [31] where a verifier structure is proposed to determine the diagnosability of a system with deadlocks. However, unlike the work in [31], this study primarily focuses on the design of an attack strategy violating the codiagnosability. The main contribution of this paper is summarized as follows: •We first formulate the K-corruption intermittent attack synthesis problem of a system modeled by LPN in the decentralized framework. To our knowledge, this issue has not been previously considered in DESs. •We develop a new structure called a complete attack graph that contains all the attacked paths limited to Kconsecutive corruptions, based on the notion of extended basis marking and attack automaton. Then some conditions are given to determine the potential attacked path that could be attacked into a predefined elementary unsound path leading to the violation of codiagnosability. •We propose an algorithm to obtain K-corruption intermittent attacks for violating the codiagnosability. Particularly, a coordination between attackers separately effected on different sites holds the same corrupted observation for each common transition. Moreover, we guarantee the stealthiness of attacks, i.e., its occurrence cannot be distinguished from the system behavior. To this aim, it is required that the set of corrupted observations is contained in the set of observations without attacks. The remainder of this work is organized as follows. Section II presents basic definitions of LPNs as well as the notion of extended basis reachability graph. In Section III, we propose an extended unfolded verifier for codiagnosability analysis, and then define the stealthy replacement and intermittent (in terms of Kconsecutive corrupted observations) attack. The addressed codiagnosability analysis problem is formulated in the LPNs under the K-intermittent attack. Section IV proposes an approach to obtain attacks for violating the codiagnosability. Finally, conclusions are summarized in Section V. II. PRELIMINARIES A. Petri net Let Nbe the set of non-negative integers. A Petri net is defined as a four-tuple N= (P, T, Pre, Post), where P= {p1, ..., pm}is a set of m∈Nplaces, T={t1, ..., tn}is a set of n∈Ntransitions with P∪T=∅and P∩T=∅, Pre :P×T→Nand Post :P×T→Nare the preand post-incidence matrices, respectively, denoting the weights of the arcs from places to transitions and transitions to places, which fix the structure of a net and are represented as matrices in Nm×n. The incidence matrix of a net is defined by C= Post −Pre. A Petri net is said to be acyclic if there is no directed cycle. A marking is a mapping M:P→Nthat assigns to a place of a Petri net a non-negative integer of tokens, graphically denoted by black dots. M(pi)is the number of tokens in place piat a marking M. A Petri net system ⟨N, M0⟩is a net N with an initial marking M0. A transition t∈Tis enabled at a marking Mif M≥Pre(·, t)and may fire yielding a marking M′=M+C(·, t). We write M[σ⟩to denote that a transition sequence σ=t1t2· · · ti∈T∗is enabled at M, and M[σ⟩M′to denote that the firing of σyields M′. When σand σ′are two sequences, σσ′stands for the concatenation of σand σ′. The Parikh vector of σis denoted by π(σ)and maps a transition t∈Tto the number of occurrences of tin σ. The cardinality of the set (·)is denoted by |(·)|. A marking Mis reachable in ⟨N, M0⟩if there exists a firing sequence σ∈T∗such that M0[σ⟩M. The set of all markings reachable from M0, denoted by R(N, M0), defines the reachability set of ⟨N, M0⟩, i.e., R(N, M0) = {M∈Nm| M0[σ⟩M}. The set of transition sequences enabled at the initial marking M0is defined as L(N, M0) = {σ∈T∗|M0[σ⟩}. Given a transition sequence set H⊆L(N, M0),we denote by H/σ the post transition sequence of a sequence σ∈H, i.e., H/σ ={σ′∈L(N, M0)|σσ′∈H}. A marking Mis dead if there is no any transition enabled at M. A net system ⟨N, M0⟩ is said to be: bounded if there exists an integer k∈Nsuch that for all M∈R(N, M0)and for all pi∈P, M(pi)≤k holds; deadlock-free if for all M∈R(N, M0),Mis not dead. Given a Petri net N= (P, T, Pre, Post)and a subset of transitions T′⊆T, the T′-induced subnet of Nis a Petri net N′= (P, T′, Pre′, Post′), where Pre′and Post′are the restrictions of Pre and Post to P×T′, respectively, i.e., the net N′is obtained by removing all the transitions in T\T′ from N. B. Labeled Petri net Given a Petri net N= (P, T, Pre, Post)and an event set Σ, a labeling function l:T→Σ∪ {ε}= Σεassigns to a transition either a symbol from the event set Σor the empty string symbol ε. A labeled Petri net (LPN) system S=⟨N, Σ, l, M0⟩is a Petri net system ⟨N, M0⟩with a labeling function land an event set Σ. A transition tis said to be unobservable or silent if it is associated with the empty string ε, i.e., l(t) = ε. The set of unobservable transitions is denoted by Tu={t∈T|l(t) = ε}. The other transitions labeled with events from Σare called observable transitions, denoted as To={t∈T|l(t)∈Σ}. Hence, the set of transitions Tcan be divided into two disjoint sets Toand Tu with T=To∪Tu. Furthermore, the set Tucan be divided into two disjoint sets Tfand Treg with Tu=Tf∪Treg, where Tfand Treg denote the sets of fault transitions and regular unobservable transitions, respectively. The set Tfcan be further partitioned into rclasses Ti f, where i= 1, . . . , r. For simplicity, this work considers an LPN with a single fault class, i.e., Tf=T1 f. Nevertheless, the proposed approach could be easily extended to the nets with multiple fault classes as presented in [29]. In addition, from a practical point of view, we partition the set Treg into two disjoint sets Tr,a and Tr,u with Treg =Tr,a ∪Tr,u, where Tr,a (resp., Tr,u) denotes the set of regular unobservable transitions that can (resp. cannot) be attacked. 4 The labeling function could be extended to a transition sequence σ=t1t2. . . tisuch that ω=l(σ) = l(t1)l(t2) . . . l(ti),which is called an observation corresponding to the sequence σ. Given an LPN system ⟨N, Σ, l, M0⟩, we define l−1(ω)as the set of all transition sequences consistent with ω∈Σ∗ ε,i.e., l−1(ω) = {σ∈L(N, M0)|l(σ) = ω}. Note that the observation ω=ε·εh=ε, h ∈N. The language generated by an LPN system Sis defined as L(N, M0) = {ω∈Σ∗ ε| ∃σ∈L(N, M0) : ω=l(σ)},i.e., the language L(N, M0)is a set of observations corresponding to the transition sequences in L(N, M0). C. Extended basis reachability graph In this subsection, we recall necessary notions of the extended basis markings in [38]. Give a transition sequence σ∈T∗, we denote by Pr,u(σ)the projection of σover Tr,u. Moreover, the restriction of incidence matrix Cof an LPN system to Tr,u is denoted by Cr,u. Definition 2.1 ( [38]): Given a marking M∈R(N, M0) and a transition t∈To∪Tf∪Tr,a of an LPN system S=⟨N, Σ, l, M0⟩, the set of explanations of tat Mis defined by Σ(M, t) = {σ∈T∗ r,u |M[σ⟩M′, M′[t⟩},and the set of explanation vectors of tat Mis denoted as Y(M, t) = {π(σ)∈N|Tr,u||σ∈Σ(M, t)}. In addition, the minimal explanation vector is defined as Ymin(M, t) = {π(σ)∈Y(M, t)|∄π(σ′)∈Y(M, t) : π(σ′)⪇π(σ)}.♢ The set of extended basis markings, denoted as Xe, is recursively computed as follows: •M0∈Xe; •If M∈Xe, then for each t∈To∪Tr,a ∪Tf, y =π(σ)∈ Ymin(M, t), (M′=M+Cr,u ·y+C(·, t)) ⇒(M′∈Xe). Given an LPN system S=⟨N, Σ, l, M0⟩, the extended basis reachability graph (EBRG) of Sis a nondeterministic finite state automaton Ge= (Xe, E, δ, M0), where Xeis the set of states (i.e., extended basis markings); E⊆(To×Σ) ∪[(Tf∪ Tr,a)×ε]is the set of event labels; δ⊆Xe×Σε×Xeis the transition relation; and M0is the initial state. In particular, the transition relation (M, e, M′)∈δwhere e=t(l(t)) ∈ To×Σor e=t(ε)∈(Tf∪Tr,a)×εif and only if ∃y∈ Ymin(M, t), M′=M+Cr,u ·y+C(·, t). III. CODIAGNOSABILITY ANALYSIS PROBLEM UNDER MALICIOUS ATTACKS In this work, we consider that the system is monitored by a set of sites J={1,2, . . . , ξ}associated with their own observable event sets, where ξis equal to the number of sites. Each transition in Tois assumed to be observable by at least one site, i.e., To=Sj∈J Tj o, where Tj o⊆Tois the set of transitions that are observable by site j. The event set of site jis Σj⊆Σ, and lj(t) = l(t)if l(t)∈Σj, εotherwise.(1) denotes the labeling function of site j. A. Codiagnosability analysis based on ε-unfolded verifier The codiagnosability analysis approach proposed in [29] relies on the assumption that the net system is deadlockfree when using the unfolded verifier. Nevertheless, this work eliminates the assumption by introducing a self-loop encoded with an additional unobservable transition tu(labeled by the empty string εand cannot be attacked) to each dead marking. Consequently, the resulting transition sequence set could be defined as Lω(N, M0) = L(N, M0)∪ {σt∗ u| ∃Md∈ R(N, M0),∄t∈T, Md[t⟩, M0[σ⟩Md}. In the following it is assumed that tuis included in the set T, i.e., tu∈T. The definition of codiagnosability in LPN systems without the deadlock-freeness assumption can be given in the following part. Here, we denote by ψ(Tf) = {σt ∈Lω(N, M0)| σ∈T∗, t ∈Tf}the set of firing transition sequences in Lω(N, M0)that end with a fault transition t∈Tf. Definition 3.1 (Codiagnosability): An LPN system ⟨N, Σ, l, M0⟩, that is monitored by a set of sites J={1,2, . . . , ξ}, is codiagnosable with respect to the set of fault transitions Tf if and only if ∀σ′∈ψ(Tf),∃h∈N,∀σ′′ ∈Lω(N, M0)/σ′,|σ′′| ≥ h =⇒ ∃j∈ J ,∀σ∈l−1 j(lj(σ′σ′′)),∃tf∈Tf:tf∈σ. ♢ This definition implies that an LPN system is codiagnosable concerning Tfif each fault in Tfcan be detected by at least one site j∈ J . To determine the dead markings of the LPN system based on EBRG, we should first verify if each extended basis marking is dead or each marking subset, reached by firing the unobservable transitions t∈Tr,u from an extended basis marking, contains dead markings. This verification method is similar to the one stated by proposition in [39] via replacing the Treg as Tr,u. Here we denote by Rr,u(M) = {M′| M[σr,u⟩M′, σr,u ∈T∗ r,u}as the set of markings obtained by firing unobservable sequences whose transitions belong to Tr,u. Proposition 3.2 ( [39]): Given an LPN system ⟨N, Σ, l, M0⟩ and a marking M, there exists at least one dead marking in Rr,u(M)if and only if the following linear integer constraint D(M)is feasible: D(M) =    Md=M+Cr,u ·y≥0, y∈NTr,u , ρ(Md). (2) where ρ(Md) : Vt∈T(Wp∈•tMd(p)≤Pre(p, t)−1).♢ In plain words, ρ(Md)is used to denote the set of dead markings that can be described by a set of linear equalities characterizing the enabling conditions of transitions. Moreover, remark that the dead markings in Rr,u(Mi)may not be unique. Subsequently, we present a new structure called εBRG that is an augmented basis reachability graph where a self-loop labeled with tu(ε)is added to each marking Md at which some unobservable transitions can fire such that a dead marking is reached. We denote by ⟨N′,Σ, l′, M0⟩ the nonfailure subset of ⟨N, Σ, l, M0⟩(or T′-induced subnet of N), where T′=T\Tf.L(N′, M0)is the transition 5 sequences formed with the sequences of L(N, M0)without fault transitions, and l′is equal to lrestricted to T\Tf. Then two reachability graphs are illustrated using the notion of extended basis markings. Definition 3.3: Given an LPN system S=⟨N, Σ, l, M0⟩, let Ge= (Xe, E, δ, M0)be the EBRG. The ε-BRG of Sis a nondeterministic finite state automaton Gε= (Xε, Eε, δε, M0), where: •Xε=Xeis the set of states. •Eε⊆E∪ {tu(ε)}is the event labels. •the transition relation δεis defined as follows: δε=δ∪ {(Mi, tu(ε), Mi)|D(Mi)is feasible}. •M0is the initial state. ♢ A nonfailure ε-BRG with respect to site j∈ J , denoted by Gj ε,n = (Xj ε,n, Ej ε,n, δj ε,n, M0), is the ε-BRG derived from ⟨N′,Σ, l′, M0⟩following the assumption that the set of observable transitions is equal to Tj o∪Tr,a. Remark 3.4: With a slight modification of q-BRG definition in [39] that introduces an observable quiescent event qto characterize the existence of deadlocks in the system, we use unobservable string εto represent that the system may reach a dead marking without any output observation. Based on the εBRG structure, an attack strategy is then developed to violate the codiagnosability. Example 1: Given an LPN system Sas depicted in Fig. 1, its extended basis markings are listed in Table I. Particularly, there exists a dead marking Md=M3, where the token enters place p7such that no transition is enabled. !1" #2 %1 !2!3!4 #( #1 ) #* + #, #- #. #// #/0 #1 #/2 #/* #/( " 3" !11 !12 !. !1 #4 !4 !/0 !, !- Fig. 1. LPN system S=⟨N, Σ, l, M0⟩with a dead marking. TABLE I THE EXTENDED BASIS MARKING OF LPN SYSTEM IN FIG.1. M0[100000000000]T M1[001000000000]T M2[000010000000]T M3[000000100000]T M4[000000010000]T M5[000000001000]T M6[000000000100]T M7[000000000010]T M8[000000000001]T Assume that the LPN system Sis monitored by two sites with Σ1={a, b, d}and Σ2={a, c, d}. By Definition 3.3, its ε-BRG and the nonfailure ε-BRGs are shown in Fig. 2. As depicted in Fig.2, once a dead marking M3is reached, we add a self-loop encoded with an unobservable transition tuthat is labeled with ε.♢ !" !# !$ !% &%(() &*(+) !,!* &#%(-) &##(.) &/(.) &0(() !1 !2!/ &#$(() &#*(.) &3(.) &*(+) &%(() &2(4) (a) !" !# !$ %$(') %)(*) !) %+(,) %-(') !. %)(*) %$(') %+(,) !/ %0(,) %1(2) %1(2) (b) !" !# !$ !% &'()) &+(,) &-()) &.(/) &0(,) &0(,) &.(/) !1 &'()) (c) Fig. 2. (a) ε-BRG of LPN system as shown in Fig. 1. (b) nonfailure ε-BRG for site 1. (c) nonfailure ε-BRG for site 2. The unfolded verifier proposed in [29] is used for codiagnosability analysis in a decentralized framework, which is constructed by the parallel composition [40] of the EBRG and all the nonfailure EBRGs. In the following, an extended unfolded verifier applying for a more general net that contains deadlocks is defined based on the notion of the ε-BRGs. Definition 3.5: Given an LPN system Sthat is monitored by a set of sites J={1,2, . . . , ξ}, its ε-BRG is Gεand the j-th nonfailure ε-BRG is Gj ε,n. The ε-unfolded verifier (ε-UV) Uε= (XU ε, EU ε, δU ε, MU 0)is a finite state automaton constructed by the parallel composition of the ε-BRG and all the nonfailure ε-BRGs. ♢ For the sake of simplicity, only two local sites monitoring the LPN system are considered in the following discussion. In detail, a node (M, α;M′, M′′)in the ε-UV is called an α-state, in which αcan be either Nto represent the normal behavior of system without the occurrence of fault from the initial state to this one, or Fto denote the occurrence of faulty behavior of system. Furthermore, in a path of Uε, the state is tagged as “duplicate” if it already exists from the root of Uε, and it is called a duplicate α-state. The transitions of ε-UV are tuples (γ, γ1, γ2)where: (1) γeither corresponds to a transition in the ε-BRG Gεor to ε(i.e., εrepresents the empty string); (2) γ1(γ2) either corresponds to a transition in the nonfailure ε-BRG G1 ε,n (G2 ε,n) or to ε. The following definition presents the notion of elementary 6 unsound path that leads to the violation of codiagnosability. Precisely, the existence of this type of path shows that, for each site, two arbitrarily long transition sequences of LPN system have the same observation and one of them contains the fault transition, such that the occurrence of the fault cannot be detected in a finite number of steps. Given an automaton G, we write Mσ −→ GM′to denote that M′is reached in G from Mwith a sequence σ. Definition 3.6: Given an ε-unfolded verifier Uε= (XU ε, EU ε, δU ε, MU 0), a sequence eσ= (γ1, γ1 1, γ2 1)(γ2, γ1 2, γ2 2)· · · (γθ, γ1 θ, γ2 θ)with σ′ α=γ1· · · γq, σ′ β=γq+1 · · · γθ, σj α=γj 1· · · γj q, and σj β=γj q+1 · · · γj θwith j= 1,2, is said to be elementary unsound path if there exists M, Mj∈Xεsatisfying the following conditions: 1) M0 σ′ α −−→ G′ e Mσ′ β −−→ G′ e M; 2) M0 σj α −−−→ G′ e,n Mjσj β −−−→ G′ e,n Mj,∀j∈ J ; 3) tf∈σ′ ασ′ β; 4) lj(σ′ α,k) = lj(σj α,k) and lj(σj β,k) = lj(σ′ β,k); 5) no prefix of eσsatisfies conditions (1)–(4). Proposition 3.7: An LPN system ⟨N, Σ, l, M0⟩is codiagnosable if and only if there exist no elementary unsound paths in the corresponding ε-UV. Proof: If the LPN system is deadlock-free, the proof procedure is same as the one in [29]. Once the LPN system contains the deadlock, a self-loop encoded with an unobservable transition tu(that is not observed by system and labeled with the empty string ε) is added to each dead marking, then the net system becomes deadlock-free. Example 2: The ε-UV, as displayed in Fig. 3, is constructed by the parallel composition of all the ε-BRGs. We deduce that the LPN system is codiagnosable since its site 2 with event set Σ2={a, c, d}is codiagnosable with respect to fault transition t11. Precisely, the occurrence of fault t11 can be detected by observing the event label cat site 2. In other words, at this site we cannot find two arbitrarily long sequences that hold same observation, and one contains fault while the other not, i.e., there is no elementary unsound path in the ε-UV. ♢ !", $; !"; !" ('(, '(, '() !*, $; !*; !* ('+, '+, ,) !-, .; !*; !* ('**, ,, ,) !/, $; !*; !/ F-state ('0, ,, '0) !/, $; !*; !/ ('1, ,, '1) Duplicate N-state !+, $; !+; !+ ('2, '2, '2) !3, $; !3; !+ ('4, '4, ,) !*, $; !*; !* ('(, '(, '() Duplicate N-state Fig. 3. Part of the ε-UV. B. Replacement and stealthy attack The architecture of codiagnosability analysis under attacks is presented in Fig. 4. To investigate the codiagnosability of the LPN system, we consider the Protocol 3 in [32] that does not require any coordination between sites, i.e., each site has its own event set, such that a net is said to be codiagnosable with respect to a fault if at least one site could deduce the occurrence of the fault within finite steps. In terms of attack process for compromising the codiagnosability of LPN systems in this decentralized setting, attackers are designed to execute their corruption actions separately at each site such that no site can detect any fault in the system. Specifically, we focus on the following case: i) an attacker corrupts the system observation based on the labeling function of its located site; ii) a coordination between attackers is applied to achieve the attacker’s goal. Elaborately, for any common transition that belongs to different sites, once its transition label is replaced by one attacker in a site, it has the same corrupted observation at other sites when existing. LPN system ! = ⟨ $, Σ, ', ()⟩ Labeling function '+ Attacker 1 Attacker 2 Coordinator Codiagnosbility Labeling function ', -+= '+(/) -,= ',(/) -′+= '2 +(/) -′,= '2 ,(/) Fig. 4. Decentralized architecture for codiagnosability under attackers. To characterize the capability of an attacker or intruder that masks the transition labels at each site, a replacement attack structure (attack structure for short) is presented as follows. To make the exposition clear, we denote by Σj ε= Σj∪ {ε} the event set of site jcontaining empty string. Definition 3.8 (Attack structure): Let S=⟨N, Σ, l, M0⟩ be an LPN system monitored by a set of sites J={1, 2, . . . , ξ}. An attack structure is defined as the set A ∈ 2((To∪Tr,a)×Σε)×((To∪Tr,a)×Σε), i.e., Ais a set of transition pairs, each associated to its label: the first transition is associated to the original label while the second one is associated to the replaced label. For each site jand for any transition t∈Tj o∪Tr,a with l(t) = e∈Σj ε, the corresponding attack structure of site jis Aj={(t(e), t(e′)) |(t(e), t(e′)) ∈ A, e′∈Σj ε} {(t(e), t(ε)) |(t(e), t(e′)) ∈ A, e′/∈Σj ε}. ♢ In plain words, concerning each pair (t(e), t(e′)) ∈ A, if the replaced transition label e′belongs to the event set Σj εof site j, then it holds the label e′in the attack structure of site j as (t(e), t(e′)) ∈ Aj. Otherwise, it holds the empty string εas (t(e), t(ε)) ∈ Ajsince the site jcannot observe the replaced 7 transition label e′, i.e, e′/∈Σj ε. Remark that each transition with respect to the attack structure may be replaced with one or several different labels or empty string. For instance, an attack structure is Aj={(tk(a), tk(b)),(tk(a), tk(ε)),(ti(c), ti(d))}, with respect to site j∈ J , that assigns to transition tkeither a label bor εfrom the original label a, and transition tia label dfrom the original label cunder the corresponding attacks. For the sake of clarity, we denote by Tj as ={t∈ Tj o∪Tr,a | ∃e′∈Σj ε,(t(e), t(e′)) ∈ Aj}the set of attackable transitions with respect to the attack structure Aj, and denote by ΣAj(t) = {e′∈Σj ε|(t(e), t(e′)) ∈ Aj, t ∈Tj as, e =lj(t)} the set of replaced labels associated with transition twhile taking into account the attack structure Aj. In this work, an attack is modeled by a function that associates a transition with a unique observation, i.e., original or replaced label, which is formally defined in the following part. Particularly, at each site j, after the occurrence of a transition in Tj as, it is possible to observe its original label or a replaced label, such that the given attack structure Aj may cause multiple attack options. Definition 3.9 (Replacement attack tuple): Let S=⟨N, Σ, l, M0⟩be an LPN system that is monitored by sites J= {1,2, . . . , ξ}and Abe an attack structure. A replacement attack tuple is denoted by A= (A1, A2, . . . , Aξ), where a replacement attack Aj(attack for short) is a modified labeling function that is the mapping lj a:T∗→Σj ε ∗where lj a(ε) = ε, lj a(t) = lj(t)if t∈T\Tj as, lj(t)or e′∈ΣAj(t)if t∈Tj as, lj a(σt) = lj a(σ)lj a(t), σ ∈T∗, t ∈T. ♢ Note that each transition t∈Tj as, under the attack Aj, is either associated with the original label lj(t)or a replaced label e′∈ΣAj(t)in term of attack structure Aj. One remark is that the considered replacement attack contains some particular insertion and removal cases. For instance, if an unobservable transition is associated to a label under the attack, it is an insertion attack; If an observable transition is associated with an empty string, this replacement could be regarded as a removal attack. Definition 3.10 (Stealthy attack): Given an LPN system ⟨N, Σ, l, M0⟩that is monitored by a set of sites J={1,2, . . . , ξ} under a replacement attack tuple A, the attack tuple Ais said to be stealthy if for any transition sequence σ, its corrupted observations are contained in the language of LPN system, i.e., ∀σ∈Lω(N, M0),∀j∈ J , lj a(σ)∈ L(N, M0).♢ Precisely, stealthiness requires that, for each site, the set of corrupted observations is contained in the set of observations without attacks. This guarantees that the occurrence of attacks cannot be distinguished from the system behavior. C. K-corruption intermittent attack Compared with continuous or permanent attacks, intermittent attacks are more practical as they consider limited attack energy and limited attack period. Here we consider a scenario that attack could last for at most a certain period of time. To do so, we assume that after a bounded number of consecutive corrupted observations under the attacks, the replaced transition label must be recovered, which leads to a new notion of K-corruption intermittent attack. More precisely, in a decentralized structure, given a transition sequence σ∈T∗ and site j∈ J ={1,2, . . . , ξ}, if the transitions t∈Tj as have been replaced Kj∈Ntimes consecutively in σunder the attacks, then their (Kj+1)th occurrence must hold its original label. Here we define a vector K= [K1, . . . , Kj, . . . , Kξ] where ξis the number of sites that monitor the system. The following example is used to illustrate a scenario about Kcorruption intermittent attack. Example 3: Let us consider again the LPN system as depicted in Fig. 1 that is vulnerable to the given attack structure A={(t8(ε), t8(d)),(t12(c), t12(ε)),(t13(a), t13(ε)),(t13(a), t13(d)),(t14(ε), t14(d))}and is monitored by two sites, where Σ1={a, b, d}and Σ2={a, c, d}. By Definition 3.8, it holds A1={(t8(ε), t8(d)),(t13(a), t13(ε)),(t13(a), t13(d)), (t14(ε), t14(d))}, and A2={(t8(ε), t8(d)),(t12(c), t12(ε)), (t13(a), t13(ε)),(t13(a), t13(d)),(t14(ε), t14(d))}. In addition, we get the sets of attackable transitions with respect to A1 and A2as T1 as ={t8, t13, t14}and T2 as ={t8, t12, t13, t14}, respectively. The LPN system executes a sequence σ= t1t2t11t12t13t14. We assume that the maximum consecutive corruption vector is K= [1 2] where K1= 1 and K2= 2. For site j= 1 with Σ1={a, b, d}, and it has the original observation l1(σ) = aa and all the possible corrupted observations are {a, ad, add}. Specifically, the unobservable transitions t1,t11 and the observable transitions t2, t12 cannot be attacked since t1, t2, t11, t12 /∈T1 as and holds l1(t1) = l1(t11) = l1(t12) = ε, l1(t2) = a. The word “aa”is observed if there is no any attack; “a”is observed if the label of transition t13 is replaced by the empty string ε. In particular, the observation “add”is obtained if both labels of transitions t13 and t14 are replaced by d. However, the consecutive corruption K1′= 2 exceeds the maximum one K1= 1, thus this case with the observation add cannot exist in the K-corruption intermittent attack setting but could exist in the permanent attack setting. ♢ At each site j, to distinguish the occurrence of a transition t∈Tj as that is associated with its original label from the replaced one, we denote by tathe transition twhose label is replaced under an attack, and by tna the transition tthat holds its original observation, respectively. Given an LPN system and a site j, under an attack Aj, let Tj a={ta i:ti∈Tj as | lj a(ti)=lj(ti)}be the set of attackable transitions that are associated with other labels, and let Tj na ={tna i:ti∈Tj as | lj a(ti) = lj(ti)}be the set of attackable transitions that hold their original labels. Inspired from the approach in [35], to obtain all the corrupted possibilities of a transition sequence under an attack for each site j, we define an insertion function Ij:T∗→ 2(T∪Tj a∪Tj na)∗ , where Ij(ε) = ε, Ij(t) = {tta, ttna}, if t∈ Tj as, otherwise Ij(t) = t. Moreover, Ij(σt) = Ij(σ)Ij(t)for all σ∈T∗and t∈T. The inverse of insert function is defined as I−1 j: (T∪Tj a∪Tj na)∗→T∗, where I−1 j(ε) = ε, I−1 j(tta) = t, I−1 j(ttna) = t, if t∈Tj as, otherwise I−1 j(t) = t. Moreover, I−1 j(σt) = I−1 j(σ)I−1 j(t)for all σ∈(T∪Tj a∪Tj na)∗and t∈(T∪Tj a∪Tj na). We denote by Pj a,na : (T∪Tj a∪Tj na)∗→ 8 (Tj a∪Tj na)∗the projection over Tj a∪Tj na, and denote by Pf,j a,na : (T∪Tj a∪Tj na)∗→(Tj a∪Tj na ∪Tf)∗the projection over Tj a∪Tj na ∪Tf. In the following, we formally present K-corruption intermittent attacks in the LPN system. Definition 3.11 (K-corruption intermittent attack): Let ⟨N, Σ, l, M0⟩be an LPN system that is monitored by a set of sites J={1,2, . . . , ξ}and is vulnerable to the attack structure A. Given a transition sequence σ∈T∗and a site j, a function that models the intermittent attack, such that the maximum number of consecutive corrupted observations is Kj, is a mapping Φj:T∗→2(T∪Tj a∪Tj na)∗ where a sequence σ+∈Φj(σ), if σ+satisfies the following conditions: (i) σ+∈Ij(σ); (ii) for all µ′, µ′′′ ∈(Tj a∪Tj na)∗and µ′′ ∈Tj a ∗, such that Pj a,na(σ+) = µ′µ′′µ′′′, then |µ′′| ≤ Kj.♢ Condition (i) ensures that the sequence σ+is obtained from the insertion function Ij(σ). Condition (ii) guarantees that the maximum number of consecutive corrupted observations of σ is Kjin the site j. Remark 3.12: For scenarios where attacks can only last for a limited period, such as camera downtime during security personnel shifts or maintenance periods, or due to limited attack energy, the intermittent attack model with a specified Kvalue can be used. This Kvalue represents the maximum number of consecutive corrupted labels allowed during an attack. If K→+∞, the attack model resembles a continuous or permanent attack, as it removes constraints on the maximum consecutive corrupted labels. Conversely, if K= 0, it indicates a safe environment for the systems where no transition labels can be attacked. Remark 3.13: The work [35] touches upon the K-loss observation that could be regarded as a special case in this work, i.e., the loss observations implies that some observable transitions are replaced into empty string under attacks. However, the proposed attack model is more flexible to characterize different attack cases, for instance, the first case is the transition label could be replaced into different labels not only the empty string; the second case is that an unobservable transition associated with a candidate sensor could also be attacked, such as restarting the sensor to obtain a new observation. Example 4: Let the LPN system Sbe monitored by two sites and the event sets be Σ1={a, b, d}and Σ2={a, c, d}. Assume that the system executes a transition sequence σ= t1t2t11t12t13t14 and K= [1 2], according to Definition 3.11, the following sequences can be generated since K-corruption intermittent attacks. •For site j= 1, it has Φ1(σ) = {t1t2t11t12t13tna 13 t14tna 14 , t1t2t11t12t13ta 13t14tna 14 , t1t2t11t12t13tna 13 t14ta 14}whose projection over (T1 a∪T1 na)∗is P1 a,na(σ+) = {tna 13 tna 14 , ta 13tna 14 , tna 13 ta 14}. •For site j= 2, it has Φ2(σ) = {t1t2t11t12ta 12t13ta 13 t14tna 14 , . . . , t1t2t11t12tna 12 t13ta 13t14tna 14 }whose projection over (T2 a∪T2 na)∗is P2 a,na(σ+) = {ta 12ta 13tna 14 ,..., tna 12 ta 13tna 14 }.♢ D. Problem statement In practice, many cyber physical systems can be efficiently modeled by Petri nets or LPN, such as automated manufacturing processes [41], resource allocation systems [42], and intelligent transportation networks [43], [44]. From an attacker viewpoint, the violation of system security properties, such as opacity and diagnosability, can lead to potential damage in pursuit of the attacker’s objectives. Meanwhile, the K-corruption intermittent attack is considered in this paper to address attack scenarios with constraints such as limited attack energy or limited attack periods. In the following, we formulate the addressed problem in this work. Problem 1: Given an LPN system ⟨N, Σ, l, M0⟩that is monitored by a set of sites J={1,2, . . . , ξ}and vulnerable to an attack structure A, the aim is to design the stealthy Kcorruption intermittent attacks such that the codiagnosability of the system is violated. The following assumptions hold for the codiagnosability analysis under the attacks in the LPN systems. (A1) The LPN system is bounded. (A2) The (T\Tj o)-induced subnet is acyclic for all j∈ J . The two assumptions are common for the diagnosability or codiagnosability analysis in the LPN systems, as the works in [20], [29], [39]. Specifically, assumption (A1) ensures that εBRG of the LPN system is always finite while assumption (A2) allows to use the state equation to characterize the markings that are reached by firing unobservable transitions from an extended basis marking, and guarantees that an ε-BRG contains a correct abstract representation of a net reachability set. IV. K-CORRUPTION INTERMITTENT ATTACKS FOR VIOLATING THE CODIAGNOSABILITY A. K-corruption Intermittent attack automaton In this part, we present an algorithm to construct a Kjcorruption intermittent attack automaton for each site j∈ J , which models the attacked behavior considering the maximum consecutive number of Kjcorrupted observations. Algorithm 1 lists all the possible attacked sequences within Kjconsecutive corrupted observations in the attack automaton, where Qjis the set of states, T∪Tj a∪Tj na is the set of transitions, δjis the transition relation, and Qj 0is the initial state. Each state of Qjis a tuple formed by the occurrence of attacked transition ta(or the occurrence of each transition t∈Tj as) and a counter with the number of corrupted observations of t, i.e., (ta, i)∈Qjand (t, i)∈Qj. More precisely, line 1initializes the state set, the initial state, and two indexes. The initial state Qj 0= (ta,0) implies that the number of consecutive corrupted observations tais 0. In the lines 2– 11, the occurrence of a transition t∈Tj as generates a new state (t, i)and a transition from (ta, i)to state (t, i), while the occurrence of a transition t∈T\Tj as remains the state (ta, i) and displays as a self-loop transition. If a transition tin the state (t, i)is not attacked, i.e., t∈Tj na, the state (t, i)reaches (ta,0). In other words, the occurrence of tna resets the counter as 0. Lines 12–15 present that the occurrence of transition ta (the label of transition tis replaced by others under the attack) 9 Algorithm 1: Construction of an attack automaton ∆j for a site j Input: Kj,⟨N, Σ, l, M0⟩, Tj a,Tj na Output: ∆j= (Qj, T ∪Tj a∪Tj na, δj, Qj 0) 1Let Qj 0= (ta,0), Qj=∅, i = 0, q = 0; 2while i≤Kjdo 3Qj=Qj∪ {(ta, i)}; 4for t∈Tdo 5if t∈Tj as then 6Qj=Qj∪ {(t, i)}; 7δj((ta, i), t)=(t, i); 8δj((t, i), tna)=(ta,0); 9if t∈T\Tj as then 10 δj((ta, i), t)=(ta, i); 11 i=i+ 1; 12 while q < Kjdo 13 for t∈Tj as do 14 δj((t, q), ta) = (ta, q + 1); 15 q=q+ 1; increases the counter and creates the transition from state (ta, q)to state (ta, q+1). Consequently, the maximum number of consecutive occurrences of tta, without the occurrence of ttna, is equal to Kj. Example 5: Consider the LPN system Sin Example 3 and K= [1 2], by using Algorithm 1, the K-corruption intermittent attack automaton ∆jfor each site jis given as shown in Fig. 5. For the sake of simplicity, we denote by Tj r,u =T\Tj as for j= 1,2.♢ !" (!$, 0) (!", 0) !" ($ !" $ (!", 1) !" (!$, 1) !" ($ *+,, -*+,, - (a) !",$ % &' (&), 0) (&', 0) &' ,) &' ) (&', 1) &' (&), 1) &' ,) (&', 2) &'(&), 2) &' ) &' ,) !",$ % !",$ % (b) Fig. 5. (a) Attack automaton ∆1with ti∈T1 as and K1= 1. (b) Attack automaton ∆2with ti∈T2 as and K2= 2. For any site j, the LPN system under Kj-corruption intermittent attacks can be characterized by the parallel composition of the ε-BRG Geand all the automata ∆jor the nonfailure ε-BRG Gj e,n and the automaton ∆j, such that G′ e=Ge||∆1||...||∆ξand Gj′ e,n =Gj e,n||∆j. Note that “||”denotes the operation of parallel composition. To make the exposition clear, in the following let us denote by L(Ge), L(G′ e), L(Gj′ e,n), L(Gj e,n)the languages generated by the graphs Ge, G′ e, Gj′ e,n, Gj e,n that contain the set of firing transition sequences, respectively. Lemma 4.1: For all transition sequences σ∈L(G′ e)(resp., σ∈L(Gj′ e,n)), it holds I−1 j(σ)∈L(Ge)(resp., I−1 j(σ)∈ L(Gj e,n)), and that their maximum consecutive corruption is equal to or less than Kj. Proof: Consider a sequence σ∈L(G′ e), where G′ e is obtained by the parallel composition of Geand all the attack automata with respect to different sites ∆1, ..., ∆ξ. By using the inverse of insert function I−1 j, all the transitions belonging to Tj a∪Tj na will be removed, such that it holds I−1 j(σ)∈L(Ge). Similarly, for a sequence σ∈L(Gj′ e,n), it holds I−1 j(σ)∈L(Gj e,n). The part of that their maximum consecutive corruption is equal to or less than Kjfor each sequence in G′ eand Gj′ e,n is similar to the proof in [35] without the consideration of the communication channel. Example 6: Continue the Example 3, the partial parts of G′ e=Ge||∆1||∆2and Gj′ e,n =Gj e,n||∆jfor site j=1, 2, are generated as shown in Figs. 6 and 7. In detail, the state of G′ eand G′ e,n is a tuple formed by the extended basis marking and its corresponding state of attack automaton. ♢ B. Complete attack graph In this part, we present an approach for the construction of a complete attack graph that generates all the potential paths to be attacked, possibly leading to an elementary unsound path that violates the codiagnosability in the system, which is shown in the following algorithm. Algorithm 2 outputs a complete attack graph Uc= (Xu c, Eu c, δu c, xu 0), where Xu cis the set of states, Eu cis the event set, δu cis the transition relation, and xu 0is the initial state. In contrast to the classic verifier approaches in [29], [31] that are obtained by using the parallel composition of failure graph and nonfailure graphs, a state of the proposed complete attack graph is updated even though for a transition (t, t1, t2), it holds l(t)=l1(t1)and l(t)=l2(t2). In addition, such a complete attack graph integrates the proposed attack automaton, such that all the potential attacked paths limited to Kconsecutive corruptions are listed. Given the attack structure with respect to each site, it is possible either to associate transition t with a label e∈Σor to replace the label of transition t as empty string ε. Then the observation of transitions in the tuple (t, t1, t2)becomes same or the transition sequence in the consecutive tuples has the same observation, such that the path containing (t, t1, t2)is possible to be attacked into an elementary unsound path. Precisely, line 1 initializes the state set, the initial state and four indices q, k, β, γ. The initial state xu 0= [M0, (ta,0),(ta,0), N;M1 0,(ta,0); M2 0,(ta,0)] implies that there is no fault at initial state with Nsymbol and the number of consecutive corrupted observations tais 0 with (ta,0). Lines 2–23, at each untagged state, iteratively generate all the other states by enumerating the consecutive transition pairs whatever the observation of transitions in the pair is same or not. In details, lines 4–18 consider all the possibilities of