Computing That Serves

Automated and Provable Privacy in Android applications


Thursday, May 17, 2018 - 11:00am


Peter Aldous


Eric Mercer

Colloquium Presented by Peter Aldous
Thursday, May 17th, 2018
Location: 1170 TMCB

A malicious information flow occurs when a program accesses information and relays it without a user's knowledge or intent. Such flows are especially problematic in military or critical infrastructure installations where security matters since people in these settings frequently carry smartphones with cameras, microphones, GPS information, etc. By combining a dynamic information flow tracking technique with abstract interpretation, it is possible to create a static analysis that provably identifies all possible information flows, making it possible to prove that an information flow is impossible under any circumstances. This analysis seems at first blush to be exponential in the size of the program but can be restructured in a way that makes it both more general and polynomial in the size of the program. This analysis proved to be effective on the majority of applications from a suite of Android applications specifically designed to be difficult to analyze.

Ongoing work seeks to further improve the efficiency and precision of the analysis, to apply the same methodology to proving the correctness of concurrent programs, and to prove the safety of security software by showing that it correctly implements its specification


Peter Aldous completed a BS in computer science in 2010 at Brigham Young University and a PhD in computer science in 2017 at the University of Utah. He is currently a postdoctoral fellow in the computer science department at Brigham Young University. His research focuses on answering practical questions about software, especially those questions that are relevant to software reliability and security.