Skip to main content
main-content

Tipp

Weitere Artikel dieser Ausgabe durch Wischen aufrufen

22.07.2017 | Ausgabe 1/2018

Journal of Automated Reasoning 1/2018

Synthesis of Obfuscation Policies to Ensure Privacy and Utility

Zeitschrift:
Journal of Automated Reasoning > Ausgabe 1/2018
Autoren:
Yi-Chin Wu, Vasumathi Raman, Blake C. Rawlings, Stéphane Lafortune, Sanjit A. Seshia
Wichtige Hinweise
This work was supported in part by TerraSwarm, one of six centers of STARnet, a Semiconductor Research Corporation program sponsored by MARCO and DARPA, in part by the National Science Foundation under Grants CCF-1138860 and CCF-1139138 (NSF Expeditions in Computing Project ExCAPE: Expeditions in Computer Augmented Program Engineering) and CNS-1421122, and in part by Industrial Learning Systems, Inc.

Abstract

We consider the problem of privacy enforcement for dynamic systems using the technique of obfuscation. Our approach captures the trade-off between privacy and utility, in a formal reactive framework. Specifically, we model a dynamic system as an automaton or labeled transition system with predefined secret behaviors. The system generates event strings for some useful computation (utility). At the same time, it must hide its secret behaviors from any outside observer of its behavior (privacy). We formally capture both privacy and utility specifications within the model of the system. We propose as obfuscation mechanism for privacy enforcement the use of edit functions that suitably alter the output behavior of the system by inserting, deleting, or replacing events in its output strings. The edit function must hide secret behaviors by making them observationally equivalent to non-secret behaviors, while at the same time satisfying the utility requirement on the output strings. We develop algorithmic procedures that synthesize a correct-by-construction edit function satisfying both privacy and utility specifications. The synthesis procedure is based on the solution of a game where the edit function must react to the system moves by suitable output editing. After presenting an explicit algorithm for solving for the winning strategies of the game, we present two complementary symbolic implementations to address scalability of our methodology. The first symbolic implementation uses a direct encoding of the explicit algorithm using binary decision diagrams (BDDs). The second symbolic implementation reframes the synthesis of edit functions as a supervisory control problem and then applies a recently-developed tool for solving supervisory control problems using BDDs. Experimental results comparing the two symbolic implementations are provided.

Bitte loggen Sie sich ein, um Zugang zu diesem Inhalt zu erhalten

Sie möchten Zugang zu diesem Inhalt erhalten? Dann informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 69.000 Bücher
  • über 500 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Umwelt
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Testen Sie jetzt 30 Tage kostenlos.

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 58.000 Bücher
  • über 300 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Testen Sie jetzt 30 Tage kostenlos.

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 50.000 Bücher
  • über 380 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Umwelt
  • Maschinenbau + Werkstoffe




Testen Sie jetzt 30 Tage kostenlos.

Literatur
Über diesen Artikel

Weitere Artikel der Ausgabe 1/2018

Journal of Automated Reasoning 1/2018 Zur Ausgabe

Premium Partner

    Bildnachweise