Synthesis of opaque systems with static and dynamic masksReportar como inadecuado

Synthesis of opaque systems with static and dynamic masks - Descarga este documento en PDF. Documentación en PDF para descargar gratis. Disponible también para leer online.

1 NICTA - National ICT Australia Sydney 2 COMETE - Concurrency, Mobility and Transactions LIX - Laboratoire d-informatique de l-École polytechnique Palaiseau, Inria Saclay - Ile de France, Polytechnique - X, CNRS - Centre National de la Recherche Scientifique : UMR7161 3 VERTECS - Verification models and techniques applied to testing and control of reactive systems Inria Rennes – Bretagne Atlantique

Abstract : Opacity is a security property formalizing the absence of secret information leakage and we address in this paper 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.

Autor: Franck Cassez - Jérémy Dubreil - Hervé Marchand -



Documentos relacionados