Skip to main content


Synthesis of opaque systems with static and dynamic masks


Franck Cassez, Jeremy Dubreil and Herve Marchand


Ecole Polytechnique



Opacity is a security property that formalizes the absence of secret information leakage. In this paper we address the problem of synthesizing opaque systems. A secret predicate S over the runs of a system G is opaque to an external user having partial observability over G, if s/he can never infer from the observation of a run of G that the run belongs to S. We choose to control the observability of events by adding a device, called a mask, between the system G and the users. We first investigate the case of static partial observability where the set of events the user can observe is fixed a priori by a static mask. In this context, we show that checking whether a system is opaque is PSPACE-complete, which implies that computing an optimal static mask ensuring opacity is also a PSPACE-complete problem. Next, we introduce dynamic partial observability where the set of events the user can observe changes over time and is chosen by a dynamic mask. We show how to check that a system is opaque w.r.t. to a dynamic mask and also address the corresponding synthesis problem: given a system G and secret states S, compute the set of dynamic masks under which S is opaque. Our main result is that the set of such masks can be finitely represented and can be computed in EXPTIME and this is a lower bound. Finally we also address the problem of computing an optimal mask.

BibTeX Entry

    journal          = {Formal Methods in System Design},
    author           = {Cassez, Franck and Dubreil, Jeremy and Marchand, Herve},
    number           = {1},
    month            = feb,
    volume           = {40},
    year             = {2012},
    keywords         = {security · confidentiality property · opacity · synthesis · dynamic observation},
    title            = {Synthesis of Opaque Systems with Static and Dynamic Masks},
    pages            = {88--115}


Served by Apache on Linux on seL4.