Skip to Main content Skip to Navigation
Journal articles

Enforcement and Validation (at runtime) of Various Notions of Opacity

yliès Falcone 1 Hervé Marchand 2 
1 CORSE - Compiler Optimization and Run-time Systems
Inria Grenoble - Rhône-Alpes, LIG - Laboratoire d'Informatique de Grenoble
2 SUMO - SUpervision of large MOdular and distributed systems
Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL
Abstract : 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.
Document type :
Journal articles
Complete list of metadata

Cited literature [27 references]  Display  Hide  Download
Contributor : Hervé Marchand Connect in order to contact the contributor
Submitted on : Wednesday, May 7, 2014 - 9:55:30 AM
Last modification on : Sunday, June 26, 2022 - 4:59:42 AM
Long-term archiving on: : Thursday, August 7, 2014 - 11:00:45 AM


Files produced by the author(s)



yliès Falcone, Hervé Marchand. Enforcement and Validation (at runtime) of Various Notions of Opacity. Discrete Event Dynamic Systems, Springer Verlag, 2015, 25 (4), pp.531-570. ⟨10.1007/s10626-014-0196-4⟩. ⟨hal-00987985⟩



Record views


Files downloads