Privacy and Utility in Dynamic Systems: Verification and Enforcement
Wintenberg, Andrew
2024
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.Deep Blue DOI
Subjects
Security and Privacy Cyber-Physical Systems Formal Methods Discrete Event Systems Automata
Types
Thesis
Metadata
Show full item recordCollections
Remediation of Harmful Language
The University of Michigan Library aims to describe library materials in a way that respects the people and communities who create, use, and are represented in our collections. Report harmful or offensive language in catalog records, finding aids, or elsewhere in our collections anonymously through our metadata feedback form. More information at Remediation of Harmful Language.
Accessibility
If you are unable to use this file in its current format, please select the Contact Us link and we can modify it to make it more accessible to you.