Enforcement of opacity properties using insertion functions

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.