東華大學圖書館 |

語系: 繁體中文

說明(常見問題)

回圖書館首頁

手機版館藏查詢

登入

回首頁

切換: 標籤 | MARC模式 | ISBD

FindBook

Google Book

Amazon

博客來

Automating Program Analysis for Differential Privacy.

紀錄類型:	書目-電子資源 : Monograph/item
正題名/作者:	Automating Program Analysis for Differential Privacy./
作者:	Zhang, Hengchu.
出版者:	Ann Arbor : ProQuest Dissertations & Theses, : 2021,
面頁冊數:	212 p.
附註:	Source: Dissertations Abstracts International, Volume: 83-03, Section: A.
Contained By:	Dissertations Abstracts International83-03A.
標題:	Computer science. -
電子資源:	http://pqdd.sinica.edu.tw/twdaoapp/servlet/advanced?query=28649799
ISBN:	9798535591117

Automating Program Analysis for Differential Privacy.
Zhang, Hengchu.

Automating Program Analysis for Differential Privacy. - Ann Arbor : ProQuest Dissertations & Theses, 2021 - 212 p.

Source: Dissertations Abstracts International, Volume: 83-03, Section: A.

Thesis (Ph.D.)--University of Pennsylvania, 2021.

This item must not be sold to any third party vendors.

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.

ISBN: 9798535591117Subjects--Topical Terms:

523869
Computer science.
Subjects--Index Terms:

Differential privacy

Automating Program Analysis for Differential Privacy.
LDR:02905nmm a2200373 4500 001 2344840
005 20220531062154.5
008 241004s2021 ||||||||||||||||| ||eng d
020 $a 9798535591117
035 $a (MiAaPQ)AAI28649799
035 $a AAI28649799
040 $a MiAaPQ $c MiAaPQ
100 1 $a Zhang, Hengchu. $3 3683657
245 1 0 $a Automating Program Analysis for Differential Privacy.
260 1 $a Ann Arbor : $b ProQuest Dissertations & Theses, $c 2021
300 $a 212 p.
500 $a Source: Dissertations Abstracts International, Volume: 83-03, Section: A.
500 $a Advisor: Pierce, Benjamin C.
502 $a Thesis (Ph.D.)--University of Pennsylvania, 2021.
506 $a This item must not be sold to any third party vendors.
520 $a 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.
590 $a School code: 0175.
650 4 $a Computer science. $3 523869
650 4 $a Grammar. $3 899712
650 4 $a Language. $3 643551
650 4 $a Programming languages. $3 3683658
650 4 $a Syntax. $3 897045
650 4 $a Logic. $3 529544
650 4 $a Optimization. $3 891104
650 4 $a Design. $3 518875
650 4 $a Noise. $3 598816
650 4 $a Algorithms. $3 536374
650 4 $a Privacy. $3 528582
650 4 $a Queries. $3 3564462
650 4 $a Semantics. $3 520060
653 $a Differential privacy
653 $a Distributed computation
653 $a Symbolic execution
653 $a Type system
690 $a 0984
690 $a 0395
690 $a 0389
690 $a 0679
710 2 $a University of Pennsylvania. $b Computer and Information Science. $3 2092564
773 0 $t Dissertations Abstracts International $g 83-03A.
790 $a 0175
791 $a Ph.D.
792 $a 2021
793 $a English
856 4 0 $u http://pqdd.sinica.edu.tw/twdaoapp/servlet/advanced?query=28649799