Synthesis of Obfuscation Policies to Ensure Privacy and Utility

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.