Enforcement and validation (at runtime) of various notions of opacity

• DOI: 10.1007/s10626-014-0196-4
• Publication Date: 2014-07-03T21:49:10Z
• Authors: Yliès Falcone; Hervé Marchand
• Keywords: Opacity; Impossibility

We are interested in the validation of opacity. Opacity models the impossibility for an attacker to retrieve the value of a secret in a system of interest. Roughly speaking, ensuring opacity provides confidentiality of a secret on the system that must not leak to an attacker. More specically, we study how we can model-check, verify and enforce at system runtime, several levels of opacity. Besides existing notions of opacity, we also introduce K-step strong opacity, a more practical notion of opacity that provides a stronger level of confidentiality.