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

DOI10.1007/S10626-014-0196-4zbMath1400.94143OpenAlexW1976202267MaRDI QIDQ896497

Yliès Falcone, Hervé Marchand

Publication date: 9 December 2015

Published in: Discrete Event Dynamic Systems (Search for Journal in Brave)

Full work available at URL: https://hal.inria.fr/hal-00987985/file/main.pdf

zbMATH Keywords

opacityruntime verificationruntime enforcement\(K\)-step opacity

Mathematics Subject Classification ID

Cryptography (94A60)

Related Items (19)

A framework for current-state opacity under dynamic information release mechanism ⋮ Decidability of opacity verification problems in labeled Petri net systems ⋮ A novel approach for supervisor synthesis to enforce opacity of discrete event systems ⋮ A general language-based framework for specifying and verifying notions of opacity ⋮ Privacy-preserving co-synthesis against sensor-actuator eavesdropping intruder ⋮ Enforcement and validation (at runtime) of various notions of opacity ⋮ Strong current-state and initial-state opacity of discrete-event systems ⋮ Game current-state opacity formulation in probabilistic resource automata ⋮ Active opacity of discrete-event systems ⋮ Matrix approach for verification of opacity of partially observed discrete event systems ⋮ Verifying weak and strong \(k\)-step opacity in discrete-event systems ⋮ Enforcing opacity by insertion functions under multiple energy constraints ⋮ Infinite-step opacity and \(K\)-step opacity of stochastic discrete-event systems ⋮ Synthesis of insertion functions for enforcement of opacity security properties ⋮ Synthesis of obfuscation policies to ensure privacy and utility ⋮ Current-state opacity enforcement in discrete event systems under incomparable observations ⋮ Enforcement of opacity by public and private insertion functions ⋮ Enhancement of opacity for distributed state estimation in cyber-physical systems ⋮ Verification and enforcement of strong infinite- and \(k\)-step opacity using state recognizers

Uses Software

• UMDES
• TAKOS

Cites Work

• Unnamed Item
• Verification of initial-state opacity in security applications of discrete event systems
• Runtime enforcement monitors: Composition, synthesis, and enforcement abilities
• Enforcement and validation (at runtime) of various notions of opacity
• A brief account of runtime verification
• Concurrent secrets
• Preserving Secrecy Under Refinement
• Dynamic Observers for the Synthesis of Opaque Systems
• Supervisory Control for Opacity
• Opacity-Enforcing Supervisory Strategies via State Estimator Constructions
• Verification of Infinite-Step Opacity and Complexity Considerations
• Enforcing Non-safety Security Policies with Program Monitors

This page was built for publication: Enforcement and validation (at runtime) of various notions of opacity