@COMMENT This file was generated by bib2html.pl <https://sourceforge.net/projects/bib2html/> version 0.94
@COMMENT written by Patrick Riley <http://sourceforge.net/users/patstg/>
@COMMENT This file came from Sanjit Seshia's publication pages at http://www.eecs.berkeley.edu/~sseshia
@inproceedings{wu-nfm16,
  author    = {Yi-Chin Wu and Vasumathi Raman and St{\'{e}}phane Lafortune and Sanjit A. Seshia},
  title     = {Obfuscator Synthesis for Privacy and Utility},
 booktitle = {Proceedings of the 8th NASA Formal Methods Symposium (NFM)},
 month = "June",
 year = {2016},
 pages = {133--149},
 abstract = {We consider the problem of synthesizing an obfuscation policy that 
enforces privacy while preserving utility with formal guarantees. Specifically, we 
consider plants modeled as finite automata with pre-defined secret behaviors. A 
given plant generates event strings for some useful computation, but meanwhile 
wants to hide its secret behaviors from any outside observer.We formally capture 
the privacy and utility specifications using the automaton model of the plant. To 
enforce both specifications, we propose an obfuscation mechanism where an edit 
function "edits" the plant's output in a reactive manner. We develop algorithmic 
procedures that synthesize a correct-by-construction edit function satisfying both 
privacy and utility specifications. To address the state explosion problem, we encode 
the synthesis algorithm symbolically using Binary Decision Diagrams. We 
present EdiSyn, an implementation of our algorithms, along with experimental 
results demonstrating its performance on illustrative examples. This is the first 
work, to our knowledge, to successfully synthesize controllers satisfying both 
privacy and utility requirements.},
}