City Research Online

New Program Abstractions for Privacy

Hunt, S. & Sands, D. (2020). New Program Abstractions for Privacy. In: Di Pierro, A., Malacaria, A. & Nagarajan, P. (Eds.), From Lambda Calculus to Cybersecurity Through Program Analysis. . Springer. doi: 10.1007/978-3-030-41103-9_10


Static program analysis, once seen primarily as a tool for optimising programs, is now increasingly important as a means to provide quality guarantees about programs. One measure of quality is the extent to which programs respect the privacy of user data. Differential privacy is a rigorous quantified definition of privacy which guarantees a bound on the loss of privacy due to the release of statistical queries. Among the benefits enjoyed by the definition of differential privacy are compositionality properties that allow differentially private analyses to be built from pieces and combined in various ways. This has led to the development of frameworks for the construction of differentially private program analyses which are private-by-construction. Past frameworks assume that the sensitive data is collected centrally, and processed by a trusted curator. However, the main examples of differential privacy applied in practice - for example in the use of differential privacy in Google Chrome’s collection of browsing statistics, or Apple’s training of predictive messaging in iOS 10 -use a purely local mechanism applied at the data source, thus avoiding the collection of sensitive data altogether. While this is a benefit of the local approach, with systems like Apple’s, users are required to completely trust that the analysis running on their system has the claimed privacy properties.

In this position paper we outline some key challenges in developing static analyses for analysing differential privacy, and propose novel abstractions for describing the behaviour of probabilistic programs not previously used in static analyses.

Publication Type: Book Section
Additional Information: This is a post-peer-review, pre-copyedit version of a chapter published in From Lambda Calculus to Cybersecurity Through Program Analysis. The final authenticated version is available online at:
Subjects: Q Science > QA Mathematics > QA75 Electronic computers. Computer science
Departments: School of Science & Technology > Computer Science
[thumbnail of _495073_1_En_10_Chapter_Author.pdf]
Text - Accepted Version
Download (845kB) | Preview


Add to AnyAdd to TwitterAdd to FacebookAdd to LinkedinAdd to PinterestAdd to Email


Downloads per month over past year

View more statistics

Actions (login required)

Admin Login Admin Login