Opacity Enforcing Supervisory Control using Non-deterministic Supervisors

TL;DR

This paper introduces a novel method for enforcing opacity in discrete-event systems using non-deterministic supervisors, which enhance system privacy by making control decisions less predictable and more difficult for intruders to infer secret states.

Contribution

The paper proposes a new non-deterministic supervisory control approach for opacity enforcement, with a complete synthesis algorithm and proof of its superiority over deterministic supervisors.

Findings

Non-deterministic supervisors can enforce opacity where deterministic ones cannot.

A sound and complete algorithm for synthesizing non-deterministic supervisors is provided.

Non-deterministic supervisors increase system privacy through probabilistic decision-making.

Abstract

In this paper, we investigate the enforcement of opacity via supervisory control in the context of discrete-event systems. A system is said to be opaque if the intruder, which is modeled as a passive observer, can never infer confidently that the system is at a secret state. The design objective is to synthesize a supervisor such that the closed-loop system is opaque even when the control policy is publicly known. In this paper, we propose a new approach for enforcing opacity using non-deterministic supervisors. A non-deterministic supervisor is a decision mechanism that provides a set of control decisions at each instant, and randomly picks a specific control decision from the decision set to actually control the plant. Compared with the standard deterministic control mechanism, such a non-deterministic control mechanism can enhance the plausible deniability of the controlled system as the online control decision is a random realization and cannot be implicitly inferred from the control policy. We provide a sound and complete algorithm for synthesizing a non-deterministic opacity-enforcing supervisor. Furthermore, we show that non-deterministic supervisors are strictly more powerful than deterministic supervisors in the sense that there may exist a non-deterministic opacity-enforcing supervisor even when deterministic supervisors cannot enforce opacity.