國立虎尾科技大學 |

Privacy and Utility in Dynamic Systems : = Verification and Enforcement.

Record Type:	Language materials, manuscript : Monograph/item
Title/Author:	Privacy and Utility in Dynamic Systems :/
Reminder of title:	Verification and Enforcement.
Author:	Wintenberg, Andrew.
Description:	1 online resource (155 pages)
Notes:	Source: Dissertations Abstracts International, Volume: 85-12, Section: B.
Contained By:	Dissertations Abstracts International85-12B.
Subject:	Electrical engineering. -
Online resource:	click for full text (PQDT)
ISBN:	9798382739588

Privacy and Utility in Dynamic Systems : = Verification and Enforcement.
Wintenberg, Andrew.

Privacy and Utility in Dynamic Systems :Verification and Enforcement. - 1 online resource (155 pages)

Source: Dissertations Abstracts International, Volume: 85-12, Section: B.

Thesis (Ph.D.)--University of Michigan, 2024.

Includes bibliographical references

The development of cyber-physical systems, which integrate physical processes across cybernetworks, 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.

Electronic reproduction.
Ann Arbor, Mich. :
ProQuest,
2024

Mode of access: World Wide Web

ISBN: 9798382739588Subjects--Topical Terms:

596380
Electrical engineering.
Subjects--Index Terms:

Security and PrivacyIndex Terms--Genre/Form:

554714
Electronic books.

Privacy and Utility in Dynamic Systems : = Verification and Enforcement.
LDR:04559ntm a22004097 4500 001 1151772
005 20241118085757.5
006 m o d
007 cr mn ---uuuuu
008 250605s2024 xx obm 000 0 eng d
020 $a 9798382739588
035 $a (MiAaPQ)AAI31349013
035 $a (MiAaPQ)umichrackham005374
035 $a AAI31349013
040 $a MiAaPQ $b eng $c MiAaPQ $d NTU
100 1 $a Wintenberg, Andrew. $3 1478598
245 1 0 $a Privacy and Utility in Dynamic Systems : $b Verification and Enforcement.
264 0 $c 2024
300 $a 1 online resource (155 pages)
336 $a text $b txt $2 rdacontent
337 $a computer $b c $2 rdamedia
338 $a online resource $b cr $2 rdacarrier
500 $a Source: Dissertations Abstracts International, Volume: 85-12, Section: B.
500 $a Advisor: Lafortune, Stephane;Ozay, Necmiye.
502 $a Thesis (Ph.D.)--University of Michigan, 2024.
504 $a Includes bibliographical references
520 $a The development of cyber-physical systems, which integrate physical processes across cybernetworks, 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.
533 $a Electronic reproduction. $b Ann Arbor, Mich. : $c ProQuest, $d 2024
538 $a Mode of access: World Wide Web
650 4 $a Electrical engineering. $3 596380
650 4 $a Computer engineering. $3 569006
650 4 $a Information technology. $3 559429
653 $a Security and Privacy
653 $a Cyber-physical systems
653 $a Access control
653 $a Discrete event systems
653 $a Automata
655 7 $a Electronic books. $2 local $3 554714
690 $a 0544
690 $a 0489
690 $a 0464
710 2 $a ProQuest Information and Learning Co. $3 1178819
710 2 $a University of Michigan. $b Electrical and Computer Engineering. $3 1372805
773 0 $t Dissertations Abstracts International $g 85-12B.
856 4 0 $u http://pqdd.sinica.edu.tw/twdaoapp/servlet/advanced?query=31349013 $z click for full text (PQDT)