Probabilistic System Opacity in Discrete Event Systems

In many emerging security applications, a system designer frequently needs to ensure that a certain property of a given system (that may reveal important details about the system's operation) be kept secret (opaque) to outside observers (eavesdroppers or intruders). Motivated by such applications, several researchers have formalized, analyzed, and described methods to verify notions of opacity in discrete event systems of interest. This paper introduces and analyzes a notion of opacity in systems that can be modeled as probabilistic finite automata or hidden Markov models. We consider a setting where a user needs to choose a specific hidden Markov model (HMM) out of m possible (different) HMMs, but would like to "hide" the true system from intruders, by not allowing them to have an arbitrary level certainty as to which system has been chosen. We describe necessary and sufficient conditions (that can be checked with polynomial complexity), under which the intruder cannot distinguish the true HMM, namely, the intruder cannot achieve a level of certainty about its decision that is above a certain threshold that we can a priori compute.