Enforcement of opacity properties using insertion functions
Yi-Chin Wu, Stéphane Lafortune · 2012
Opacity is a confidentiality property that arises in the analysis of security properties in networked systems. It characterizes whether a “secret” of a system can be inferred by an outside observer called an “intruder.” We consider the problem of enforcing opacity in partially-observed discrete event systems modeled as 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. The insertion function must respond to the full system's output behavior. Also, the insertion function should not create new observed behavior but only replicate existing observable strings. We define the property of “i-enforceability,” when there exists an insertion function that renders a non-opaque system opaque. To synthesize insertion functions that ensure opacity, we define and construct a new structure called the “All Insertion Structure” (AIS). The AIS can be used to verify if a given opacity property is i-enforceable. The AIS enumerates all i-enforcing insertion functions in a compact state transition structure. If a given opacity property has been verified to be i-enforceable, we show how to use the AIS to synthesize an i-enforcing insertion function.