Synthesis of Insertion Functions to Enforce Decentralized and Joint Opacity Properties of Discrete-event Systems

TL;DR

This paper develops methods to enforce opacity in discrete-event systems with multiple intruders, using insertion functions to manipulate outputs and ensure confidentiality even under coordination.

Contribution

It introduces novel enforcement mechanisms for opacity using insertion functions, addressing both coordinated and non-coordinated intruder scenarios in discrete-event systems.

Findings

Effective enforcement of opacity demonstrated through examples

Insertion functions successfully manipulate outputs to prevent information leakage

Coordination protocols enhance the enforcement capabilities

Abstract

Opacity is a confidentiality property that characterizes the non-disclosure of specified secret information of a system to an outside observer. In this paper, we consider the enforcement of opacity within the discrete-event system formalism in the presence of multiple intruders. We study two cases, one without coordination among the intruders and the other with coordination. We propose appropriate notions of opacity corresponding to the two cases, respectively, and propose enforcement mechanisms for these opacity properties based on the implementation of insertion functions, which manipulates the output of the system by inserting fictitious observable events whenever necessary. The insertion mechanism is adapted to the decentralized framework to enforce opacity when no coordination exists. Furthermore, we present a coordination and refinement procedure to synthesize appropriate insertion functions to enforce opacity when intruders may coordinate with each other by following an intersection-based coordination protocol. The effectiveness of the proposed opacity-enforcement approaches is validated through illustrative examples.