Programming Principles and
Abstractions for Privacy
The world of software has changed a lot in the past decade. Today, broad platforms like mobile phones and web browsers allow users to download software from a variety of sources. In many cases, the software wants access to the user’s private information. With such access comes the risk that the software may leak the private information or misuse it in ways that the user does not expect. Currently, a privacy-conscious user can only deny software access to private information, e.g., by using the “incognito mode” in web browsers and by explicitly denying permissions on mobile platforms like Android. However, this can cause applications to malfunction since they are expecting the private information to be available.
Our overall goal in this project was to enable the design of adaptive applications that react to allowed permissions by gracefully adjusting the level of functionality.1 Our technical approach is based on advancing the area of information flow control, a language-based paradigm for enforcing privacy policies. The key idea is to allow data to come with policies that specify how it can be used (i.e., its confidentiality requirements), and application modules to dually specify what policies they require of input data to provide specific functionality. While our focus is on theoretical foundations, we also make progress on practical deployment of this idea in various settings.
Specifically, we 1) examined the foundations of policy specification that balances the privacy needs of data and the access requirement of program modules, 2) advanced the state of the art in fundamental techniques for enforcing information flow policies in higher-order stateful languages and in low-level languages, and 3) worked on developing our overall idea in the context of Android applications. Overall, our work in this project layed the foundations for achieving the goal we set out with. In executing the project, we made several fundamental contributions to information flow analysis. First, we resolved an open problem in information flow analysis by showing that two different styles of specifying policies – at fine-granularity and at coarse-granularity – are actually equally expressive. Second, we develop semantic models of information flow types that support higher-order state; these models enable showing that enforcement techniques are sound. Third, we develop a technique for enforcing information flow policies in low-level languages like C, where even control flow integrity is not a given.
Role Within the Collaborative Research Center