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

https://hal.inria.fr/hal-00987985
Contributor : Hervé Marchand <>
Submitted on : Wednesday, May 7, 2014 - 9:55:30 AM
Last modification on : Thursday, January 7, 2021 - 4:34:28 PM
Long-term archiving on: : Thursday, August 7, 2014 - 11:00:45 AM

File

main.pdf
Files produced by the author(s)

Identifiers

Citation

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⟩

Share

Metrics

Record views

951

Files downloads

581