Supervisory enforcement of current-state opacity with uncomparable observations

Current-state opacity is a key security property in discrete event systems. A system is said to be current-state opaque if the intruder, who only has partial observations on the system's evolution, is never able to infer that the current state of the system is within a set of secret states. In this work, we address the problem of enforcing current-state opacity by supervisory control. Given a system that is modeled with a finite automaton and that is not current-state opaque with respect to a given secret, the enforcement problem consists in designing a supervisor so that the controlled system is current-state opaque. We assume that the supervisor can only observe and control a subset of events. To be more general, we assume no specific containment relationship exists between the sets of events that can be observed by the intruder and the supervisor, respectively. We call this general setting uncomparable observations. We show that the maximally permissive supervisor always exists and propose a novel approach for its design.