Opacity Enforcement in Discrete Event Systems Using Modification Functions
Xiaoyan Li, Christoforos N. Hadjicostis, Zhiwu Li · IEEE Transactions on Automation Science and Engineering · 2024
Opacity of a discrete event system is a confidentiality property that characterizes instances when the secret behavior of the system cannot be revealed. This paper considers current-state opacity with respect to a set of secret states, and addresses the opacity enforcement problem via modification functions that are capable of replacing in real-time the output of the underlying system with another output, aiming to prevent the intruder from inferring the secret. We study modification functions that are constrained, i.e., they may not be able to modify certain outputs or they may have restrictions in how they modify a particular output. A system is said to be emc-enforceable if opacity can be enforced via modification functions under the given event modification constraints (emc). To verify whether a system is emc-enforceable, we construct a verifier, based on which a necessary and sufficient condition is obtained. If a system is emc-enforceable, an algorithm is developed to compute a modification strategy based on the verifier to enforce opacity. For m-enforceability, a special case of emc-enforceability without constraints, two necessary and sufficient conditions to verify and enforce opacity with reduced complexity are presented, one based on a system estimator and the other based on a detector. Note to Practitioners—Discrete event systems provide appropriate mathematical models for analysing information-flow properties of cyber-physical systems, such as intelligent transportation systems, command-control systems, and networked communication systems, in dynamically changing environments. Opacity is a general property capable of capturing safe information-flow in a cyber-physical system. This article targets the enforcement of opacity using modification functions that mask the output of the system into another output in a manner that appears consistent to an external observer as the system evolves. The designed modification function can be realized via triggers equipped with digital logic and storage functionality. As an output is generated by a system, a trigger displays a fake output based on the stored real and fake states.