Secret inference and attacktability analysis of discrete event systems

In the discrete event systems literature, the studies addressing opacity usually assume a passive intruder, who has full knowledge of the structure of a system but with only a partial observation ability. This work touches upon the opacity problem in discrete event systems modeled with labeled Petri nets, by assuming the existence of an active intruder. Herein, an active intruder, whose abilities exceed passive observations, is assumed to be able to manipulate the behavior of a system through sensor attacks in a practical manner, i.e., in an embedded way, in order to compromise the opacity of a system. In this setting, a framework for opacity verification is first proposed from the intruder's viewpoint, where opacity is referred to as language-based opacity. A verification algorithm is then derived to identify opaque secret words. Two stealthy attack models named sensor-failure-making strategy and sensor-injection-making strategy are introduced, allowing the intruder to implant/damage some sensors, i.e., add/delete some events, in line with the original behavior of a system, in order to infer the secret information. An algorithmic procedure for attractability analysis is provided for each attack strategy. Once a system is proved to be attackable, a stealthy attack structure that synthesizes different sensor-failure-making (resp. sensor-injection-making) attacks is constructed. Furthermore, we demonstrate the validity and efficiency of the proposed approaches by implementing the presented algorithms and running experiments on a manufacturing system example. (c) 2022 Elsevier Inc. All rights reserved.

Automated summary

This paper addresses the opacity problem in discrete event systems modeled with labeled Petri nets, assuming the existence of an active intruder who can manipulate the system behavior through sensor attacks. The paper proposes a framework for opacity verification and derives algorithms for identifying opaque secret words and analyzing attacks. The validity and efficiency of the proposed approaches are demonstrated through experiments.