Privacy and Utility in Dynamic Systems: Verification and Enforcement

Abstract

The development of cyber-physical systems, which integrate physical processes across cyber-networks, has had a profound impact on our society. Many of these systems, ranging from location-based services on our phones to devices on the Internet of Things in our homes, rely on the communication of sensitive information which may be vulnerable to eavesdropping. The physical harm that can result from leaking this information, like your current location or the occupancy of your home, is well documented. This has lead to strict privacy and security requirements which are often difficult to implement in practice. Motivated by the success of formal methods in developing provable guarantees for cyber-physical systems with strict safety requirements, in this dissertation we focus on the following problems: (1) How can we verify that a system maintains privacy? and (2) How can we enforce privacy upon a system while maintaining its original purpose or utility? Verification is used to analyze vulnerabilities in existing systems and provide feedback to guide the design of new systems. Existing approaches to verification are limited by their ability to express complex privacy requirements and by their high computational burden. We propose a general framework expressing privacy as the formal information flow property of opacity. Over discrete state models (automata), we show how this framework unifies many of the existing notions of opacity studied in the area of discrete event systems. Within this framework, we develop approaches to verification based upon elementary automata constructions that exhibit competitive performance to existing techniques. Additionally, to overcome the inherent computational complexity of verification, we propose a relaxation of opacity that captures bounds on the ability of observers to reason about the system. We develop a corresponding verification approach based on an encoding to the Boolean satisfiability problem. These approaches are demonstrated on randomly generated systems alongside a novel server-load hiding problem. Enforcement is used when a given system cannot be verified to maintain privacy, or when the design of systems by hand is impractical. We focus on the enforcement of privacy with obfuscation, altering communication on the network to shape the beliefs of observers. Over systems modeled by automata, obfuscation takes the form of edit functions which dynamically delete certain outputs and insert fictitious ones. We first show how to apply existing methods for designing such obfuscators within our general framework for opacity. To generalize the limited notion of utility guaranteed by these methods, we then propose a new approach to obfuscation which explicitly models the information flow from the system to its authorized users as a distributed system. Finally, we integrate control into this approach over a variety of network architectures. These approaches use a blend of techniques from supervisory control for DES and reactive synthesis, and are demonstrated on a contact-tracing problem as well as a smart building access-control system.