Project B1

Privacy Enforcement for Third-Party Software

Principal Investigators

Project Summary

When running software on a device, the user rightfully expects that sensitive information remains private. Unfortunately, this expectation is often violated. Incidents with mobile applications that silently transferred the complete address book (e.g. Twitter or Facebook) and other personal information to their servers, and a study showing that many of the top web sites on the Internet leak personal data in an unintended way.
We see the need for a mechanism that allows the user to enforce precise restrictions on the flow of information in an application, even if these restrictions are not offered as an option in the application, or may in fact run contrary to the objectives of the potentially disingenuous developer of the application. Our approach builds on recent advances in the property oriented approach to IT-security.
Requirements on information-flow, such as non-interference, and the changes these requirements go through over time, such as declassifying certain information, can be characterized using logics for temporal hyperproperties, such as the temporal logic HyperLTL [B01-17]. A uniform algorithmic framework for the verification (model checking) of such properties already exists. In this project, we 1) extended this algorithmic framework to the automatic monitoring and enforcement of temporal hyperproperties at runtime and 2) studied how enforcement on programs containing both first- and third-party code can be reduced to the verification of first-party code only via sandboxing. To achieve this goal, we had to overcome substantial theoretical and practical challenges. First, not every property can be monitored at runtime, let alone enforced. We identified the monitorable and enforcible sublogic of HyperLTL. Second, efficiency is a prime concern, as the enforcement mechanism should not substantially slow down the main application. We investigated a spectrum of monitoring and enforcement algorithms and developed many optimization techniques. With our specification analysis that reduces the algorithmic work by exploiting symmetry, transitivity or reflexivity of the HyperLTL formula. With our trace analysis, we minimized space consumption. Third, in practice, first-party code is often linked with arbitrary, unverifiable code such as that from third-party libraries, but we still want to verify that the entire program has certain properties. To facilitate this, we examined how verification of an entire program can be reduced to the verification of the first-party code only, by sandboxing the third-party code.

Role Within the Collaborative Research Center