# Dynamic observers for the synthesis of opaque systems

## Authors

Franck Cassez, Jérémy Dubreil and Hervé Marchand

NICTA

CNRS

Irisa

## Abstract

In this paper, we address the problem of synthesizing \emph{opaque} systems. A secret predicate $S$ over the runs of a system $G$ is \emph{opaque} to an external user having partial observability over $G$, if s/he can never infer from the partial observation of a run of $G$ that the run satisfies $S$. We first investigate the case of \emph{static} partial observability where the set of events the user can observe is fixed a priori. In this context, we show that checking whether a system is opaque is PSPACE-complete, which implies that computing an optimal static observer ensuring opacity is also PSPACE-complete. % Next, we introduce \emph{dynamic} partial observability where the set of events the user can observe changes over time. % We show how to check that a system is opaque wrt a dynamic observer and also address the corresponding synthesis problem: given a system $G$ and secret states $S$, compute the set of dynamic observers under which $S$ is opaque. Our main result is that the synthesis problem can be solved in EXPTIME.

## BibTeX Entry

  @inproceedings{Cassez_DM_09,
publisher        = {Lecture Notes in Computer Science},
author           = {Cassez, Franck and Dubreil, J\'er\'emy and Marchand, Herv\'e},
month            = oct,
editor           = {{Zhiming Liu and Anders P. Ravn}},
year             = {2009},
keywords         = {security, opacity, synthesis},
title            = {Dynamic Observers for the Synthesis of Opaque Systems},
booktitle        = {7th International Symposium on Automated Technology for Verification and Analysis (ATVA'09)},
pages            = {352--367},
}