STP-based verification and synthesis of state opacity for logical finite state machines

Finite-state machines are among the most important models for studying the logical dynamic behavior of cyber–physical systems, and their security and privacy are urgent problems to be solved at present. This paper explores the state-opacity-based privacy verification and synthesis problems for finite-state machines from an algebraic perspective. First, the dynamics of a finite-state machine can be established as an algebraic expression using the semi-tensor product of matrices. Beginning with this novel representation, we propose an algebraic criterion to verify whether the privacy state is opaque to intruders. Subsequently, we investigate the opacity-enhancement synthesis problem from two perspectives. On one hand, we design a feedback supervisory controller by disabling controllable events such that the closed-loop system is opaque with respect to privacy states; on the other hand, we investigate the editing of an observable function simply by assigning specific events in the observation channel instead of changing the transition behavior of the system. We observe that these synthesis problems can be addressed by calculating a system of algebraic equations, and we further develop two algorithms to obtain the controller or function. Finally, an interesting example is presented to demonstrate the validity of the proposed algebraic method. Taken together, these results are conducive to a systematic understanding of privacy enhancement problems.