Opacity-Enforcing Supervisory Strategies via State Estimator Constructions

State-based notions of opacity, such as initial-state opacity and infinite-step opacity, emerge as key properties in numerous security applications of discrete event systems. We consider systems that are modeled as partially observed nondeterministic finite automata and tackle the problem of constructing a minimally restrictive opacity-enforcing supervisor (MOES), which limits the system's behavior within some prespecified legal behavior while enforcing initial-state opacity or infinite-step opacity requirements. We characterize the solution to MOES, under some mild assumptions, in terms of the supremal element of certain controllable, normal, and opaque languages. We also show that this supremal element always exists and that it can be implemented using state estimators. The result is a supervisor that achieves conformance to the pre-specified legal behavior while enforcing initial-state opacity by disabling, at any given time, a subset of the controllable system events, in a way that minimally restricts the range of allowable system behavior. Although infinite-step opacity cannot be easily translated to language-based opacity, we show that, by using a finite bank of supervisors, the aforementioned approach can be extended to enforce infinite-step opacity in a minimally restrictive way.