2 options
Automating program analysis for differential privacy / Hengchu Zhang.
- Format:
- Book
- Thesis/Dissertation
- Author/Creator:
- Zhang, Hengchu, author.
- Language:
- English
- Subjects (All):
- Computer science.
- Grammar.
- Language.
- Programming languages.
- Syntax.
- Logic.
- Optimization.
- Design.
- Noise.
- Algorithms.
- Privacy.
- Queries.
- Semantics.
- Computer and Information Science--Penn dissertations.
- Penn dissertations--Computer and Information Science.
- Local Subjects:
- Computer science.
- Grammar.
- Language.
- Programming languages.
- Syntax.
- Logic.
- Optimization.
- Design.
- Noise.
- Algorithms.
- Privacy.
- Queries.
- Semantics.
- Computer and Information Science--Penn dissertations.
- Penn dissertations--Computer and Information Science.
- Genre:
- Academic theses.
- Physical Description:
- 1 online resource (212 pages)
- Contained In:
- Dissertations Abstracts International 83-03A.
- Place of Publication:
- [Philadelphia, Pennsylvania] : University of Pennsylvania ; Ann Arbor : ProQuest Dissertations & Theses, 2021.
- Language Note:
- English
- System Details:
- Mode of access: World Wide Web.
- text file
- Summary:
- This dissertation explores techniques for automating program analysis, with a focus on validating and securely executing differentially private programs. Differential privacy allows analysts to study general patterns among individuals, while providing strong protections against identity leakage. To automatically check differential privacy for programs, we develop Fuzzi: a three-level logic for differential privacy. Fuzzi's lowest level is a general-purpose logic; its middle level is apRHL, a program logic for mechanical construction of differential privacy proofs; and its top level is a novel sensitivity logic for tracking sensitivity bounds, a fundamental building block of differential privacy. Some differentially private algorithms have sophisticated proofs that cannot be derived by a compositional typechecking process. To detect incorrect implementations for these algorithms, we develop DPCheck for testing differential privacy automatically. Adapting a well-known "pointwise" proof technique for differential privacy, DPCheck observes runtime program behaviors, and derives formulas that constrain potential privacy proofs. Once we are convinced that a program is differentially private, we often still have to trust that the machine executing the program does not misbehave and leak sensitive results. For analytics at scale, computation is often delegated to networked computers that may become compromised. To securely run differentially private analytics at scale, we develop Orchard, a system that can answer many differentially private queries over data distributed among millions of user devices. Orchard leverages cryptographic primitives to employ untrusted computers, while preventing untrusted computers from observing sensitive results.
- Notes:
- Source: Dissertations Abstracts International, Volume: 83-03, Section: A.
- Advisors: Pierce, Benjamin C.; Committee members: Zdancewic, Steve; Roth, Aaron; Haeberlen, Andreas; Hsu, Justin.
- Department: Computer and Information Science.
- Ph.D. University of Pennsylvania 2021.
- Local Notes:
- School code: 0175
- ISBN:
- 9798535591117
- Access Restriction:
- Restricted for use by site license.
- This item must not be sold to any third party vendors.
The Penn Libraries is committed to describing library materials using current, accurate, and responsible language. If you discover outdated or inaccurate language, please fill out this feedback form to report it and suggest alternative language.