Obfuscator Synthesis for Privacy and Utility
Yi-Chin Wu, Vasu Raman, Stephane Lafortune, Sanjit Seshia

Citation
Yi-Chin Wu, Vasu Raman, Stephane Lafortune, Sanjit Seshia. "Obfuscator Synthesis for Privacy and Utility". 8th NASA Formal Methods Symposium, June 2016.

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 state 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 (BDDs). We present experimental results demonstrating the performance of our algorithms on illustrative examples. This is the first work, to our knowledge, to successfully synthesize controllers satisfying both privacy and utility requirements.

Electronic downloads

Internal. This publication has been marked by the author for TerraSwarm-only distribution, so electronic downloads are not available without logging in.

Citation formats

• HTML

  Yi-Chin Wu, Vasu Raman, Stephane Lafortune, Sanjit Seshia.
  <a
  href="http://www.terraswarm.org/pubs/750.html"
  >Obfuscator Synthesis for Privacy and Utility</a>,
  <i>8th NASA Formal Methods Symposium</i>, June
  2016.

• Plain text

  Yi-Chin Wu, Vasu Raman, Stephane Lafortune, Sanjit Seshia.
  "Obfuscator Synthesis for Privacy and Utility".
  <i>8th NASA Formal Methods Symposium</i>, June
  2016.

• BibTeX

  @article{WuRamanLafortuneSeshia16_ObfuscatorSynthesisForPrivacyUtility,
      author = {Yi-Chin Wu and Vasu Raman and Stephane Lafortune
                and Sanjit Seshia},
      title = {Obfuscator Synthesis for Privacy and Utility},
      journal = {8th NASA Formal Methods Symposium},
      month = {June},
      year = {2016},
      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
                state 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 (BDDs). We present experimental
                results demonstrating the performance of our
                algorithms on illustrative examples. This is the
                first work, to our knowledge, to successfully
                synthesize controllers satisfying both privacy and
                utility requirements.},
      URL = {http://terraswarm.org/pubs/750.html}
  }
  

Posted by Elizabeth Coyne on 2 Mar 2016.
Groups: services