Opacity Enforcement Using Nondeterministic Publicly Known Edit Functions

Abstract

This note investigates enforcement of opacity by nondeterministic edit functions. The edit functions alter the system's output by inserting fictitious events or erasing observed events. The edit decisions are randomly made while not known by the outside environment a priori. There is an intruder characterized as a passive observer with malicious goals to infer the secrets of the system. We require that opacity be enforced when the intruder may or may not know the implementation of edit functions. This requirement is termed as private and public safety. We also restrict the operation of edit functions by defining edit constraints. Then, the opacity enforcement problem is transformed to a three-player game among the edit function, the environment, and a dummy player, which helps to determine edit decisions. A game structure called the all edit structure (AES) is introduced to characterize the interaction among those players. It embeds all privately safe edit functions and may also embed publicly safe edit functions. Based on the AES, we present an algorithm that provably synthesizes nondeterministic edit functions that satisfy both private safety and public safety.