Privacy and Utility in Dynamic Systems: Verification and Enforcement

PASSCODE: 171515

Cyber-physical systems, which integrate physical processes across cyber-networks, have had a profound impact on society. From location-based services on our phones to the Internet of Things in our homes, these systems have demonstrated immense utility. However, they often communicate sensitive information which is vulnerable to eavesdropping. Because leaking information like your current location can result in physical harm, privacy is of critical importance. This presents a challenge as eavesdroppers can use knowledge of the system’s dynamics to refine their estimates of the system’s state. Furthermore, existing tools for designing privacy-preserving systems are limited by computational tractability and their ability to capture complex privacy and utility requirements.

Motivated by the success of formal methods to provide provable safety guarantees for cyber-physical systems, we develop methods to provide formal guarantees of privacy and utility. We propose a framework expressing and verifying privacy as the information flow property of opacity over automata. Finally, we present obfuscation as a mechanism for enforcing privacy: selectively editing the outputs of a system to confuse or mislead eavesdroppers. Using tools from distributed reactive synthesis, we show how networked controllers and obfuscators can be automatically designed to satisfy a variety of privacy and utility specifications.

CO-CHAIRS: Professors Stéphane Lafortune & Necmiye Ozay