Synthesis of opaque systems with static and dynamic masks

DOI10.1007/S10703-012-0141-9zbMath1247.68161OpenAlexW2001653139MaRDI QIDQ453510

Franck Cassez, Jérémy Dubreil, Hervé Marchand

Publication date: 27 September 2012

Published in: Formal Methods in System Design (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10703-012-0141-9

zbMATH Keywords

synthesissecurityopacityconfidentiality propertydynamic observation

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Reliability, testing and fault tolerance of networks and computer systems (68M15)

Related Items (25)

Enforcement for infinite-step opacity and K-step opacity via insertion mechanism ⋮ A framework for current-state opacity under dynamic information release mechanism ⋮ \(k\)-memory-embedded insertion mechanism for opacity enforcement ⋮ Verification of opacity and diagnosability for pushdown systems ⋮ Decidability of opacity verification problems in labeled Petri net systems ⋮ A new approach for the verification of infinite-step and \(K\)-step opacity using two-way observers ⋮ Verification and enforcement of current-state opacity based on a state space approach ⋮ Privacy-preserving co-synthesis against sensor-actuator eavesdropping intruder ⋮ Matrix approach for verification of opacity of partially observed discrete event systems ⋮ Information control in networked discrete event systems and its application to battery management systems ⋮ Enforcing opacity by insertion functions under multiple energy constraints ⋮ Infinite-step opacity and \(K\)-step opacity of stochastic discrete-event systems ⋮ Probabilistic opacity for Markov decision processes ⋮ Synthesis of insertion functions for enforcement of opacity security properties ⋮ Complexity of detectability, opacity and A-diagnosability for modular discrete event systems ⋮ Synthesis of sensor deception attacks at the supervisory layer of cyber-physical systems ⋮ A general approach for optimizing dynamic sensor activation for discrete event systems ⋮ Current-state opacity enforcement in discrete event systems under incomparable observations ⋮ Enforcement of opacity by public and private insertion functions ⋮ Comparing the notions of opacity for discrete-event systems ⋮ Enhancement of opacity for distributed state estimation in cyber-physical systems ⋮ Enforcing current-state opacity through shuffle and deletions of event observations ⋮ Online verification of \(K\)-step opacity by Petri nets in centralized and decentralized structures ⋮ Diagnosis and opacity problems for infinite state systems modeled by recursive tile systems ⋮ Control and synthesis of non-interferent timed systems

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Borel determinacy
• A characterization of the minimum cycle mean in a digraph
• The complexity of mean payoff games on graphs
• Concurrent secrets
• Automated verification of selected equivalences for security protocols
• Test Generation for Network Security Rules
• Preserving Secrecy Under Refinement
• Dynamic Observers for the Synthesis of Opaque Systems
• On the synthesis of strategies in infinite games
• Supervisory Control for Opacity
• Characterizing intransitive noninterference for 3-domain security policies with observability

This page was built for publication: Synthesis of opaque systems with static and dynamic masks