Synthesis of obfuscation policies to ensure privacy and utility

DOI10.1007/S10817-017-9420-XzbMath1426.68085OpenAlexW2736690356MaRDI QIDQ682359

Stéphane Lafortune, Vasumathi Raman, Sanjit A. Seshia, Yi-Chin Wu, Blake C. Rawlings

Publication date: 2 February 2018

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://escholarship.org/uc/item/0p21098v

zbMATH Keywords

supervisory controlprivacyobfuscationedit functionsformal synthesis

Mathematics Subject Classification ID

Applications of game theory (91A80) Formal languages and automata (68Q45) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Privacy of data (68P27)

Related Items (7)

Enforcement for infinite-step opacity and K-step opacity via insertion mechanism ⋮ \(k\)-memory-embedded insertion mechanism for opacity enforcement ⋮ A general language-based framework for specifying and verifying notions of opacity ⋮ State-based opacity of labeled real-time automata ⋮ Active opacity of discrete-event systems ⋮ Synthesis of sensor deception attacks at the supervisory layer of cyber-physical systems ⋮ Enforcement of opacity by public and private insertion functions

Uses Software

• NuSMV
• CUDD
• UMDES
• PrivateLR

Cites Work

• Unnamed Item
• Unnamed Item
• Synthesis of insertion functions for enforcement of opacity security properties
• Results on the propositional \(\mu\)-calculus
• Enforcement and validation (at runtime) of various notions of opacity
• Symbolic model checking: \(10^{20}\) states and beyond
• Supervisory control and reactive synthesis: a comparative introduction
• Concurrent secrets
• Coping with Selfish On-Going Behaviors
• Introduction to Discrete Event Systems
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• Graph-Based Algorithms for Boolean Function Manipulation
• Supervisory Control of a Class of Discrete Event Processes
• Logic in Computer Science
• Supervisory Control for Opacity
• Opacity-Enforcing Supervisory Strategies via State Estimator Constructions
• Differential Privacy

This page was built for publication: Synthesis of obfuscation policies to ensure privacy and utility