Synthesis of insertion functions for enforcement of opacity security properties

Opacity is a confidentiality property that characterizes whether a “secret” of a system can be inferred by an outside observer called an “intruder”. In this paper, we consider the problem of enforcing opacity in systems modeled as partially-observed finite-state automata. We propose a novel enforcement mechanism based on the use of insertion functions. An insertion function is a monitoring interface at the output of the system that changes the system’s output behavior by inserting additional observable events. We define the property of “i-enforceability” that an insertion function needs to satisfy in order to enforce opacity. I-enforceability captures an insertion function’s ability to respond to every system’s observed behavior and to output only modified behaviors that look like existing non-secret behaviors. Given an insertion function, we provide an algorithm that verifies whether it is i-enforcing. More generally, given an opacity notion, we determine whether it is i-enforceable or not by constructing a structure called the “All Insertion Structure” (AIS). The AIS enumerates all i-enforcing insertion functions in a compact state transition structure. If a given opacity notion has been verified to be i-enforceable, we show how to use the AIS to synthesize an i-enforcing insertion function.