Integrating Obfuscation and Control for Privacy

Networked systems must often balance privacy in avoiding leaking sensitive information, with utility in communicating the information that is needed by components to operate correctly. We consider the problem of enforcing privacy and utility with both <italic xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">obfuscation</i> (altering communications to mislead eavesdroppers) and <italic xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">control</i> (restricting system behavior to avoid information leakage). We present a formulation of this problem which models components of the networked system as interconnected reactive processes. Tools from distributed reactive synthesis are then used to automatically design obfuscators and controllers which coordinate to enforce requirements. In particular we develop formal specifications capturing privacy using the information flow property of <italic xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">opacity</i> and utility ensuring availability of information or imposing constraints on the closed-loop system. This synthesis approach is applicable to a large class of network architectures which we demonstrate on three representative problems over a building access control system.