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.

Supervisory enforcement of current-state opacity with uncomparable observations

SEATZU, CARLA;GIUA, ALESSANDRO
2016

Abstract

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.
Discrete event systems; Finite automata; Observers; Current-state opacity; Current-state opaque controlled system; Finite automaton; Maximally permissive supervisor; Supervisory control; Uncomparable observations; Control theory
File in questo prodotto:
File Dimensione Formato  
16wodes_draft.pdf

Solo gestori archivio

Tipologia: versione post-print
Dimensione 460.89 kB
Formato Adobe PDF
460.89 kB Adobe PDF   Visualizza/Apri   Richiedi una copia

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: http://hdl.handle.net/11584/178028
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 5
  • ???jsp.display-item.citation.isi??? 3
social impact