A defining characteristic of modern personal computing is the trend towards extensible platforms (e.g., smartphones and tablets) that run a large number of specialized applications, many of uncertain quality or provenance. The common security mechanisms available on these platforms are application isolation and permission systems. Unfortunately, it has been repeatedly shown that these mechanisms fail to prevent a range of misbehaviors, including privilege-escalation attacks and information-flow leakage. Researchers have proposed information-flow protections for these platforms. However, such mechanisms have rarely been adopted in practice, partly due to the level of abstraction at which they allow policies to be specified.
We develop a formal, case-study-driven approach that will leverage advances in information-flow research to develop new policy-specification languages and enforcement mechanisms for today's extensible environments. First, we develop appropriate policy-specification languages that allow policies to be specified at an intermediate level of abstraction. Policy specification will be easy enough to understand and formulate to be accessible to most developers, yet sufficiently expressive to support rich policies. Second, we develop hybrid enforcement mechanisms to support policy that is specified at levels of abstraction that do not neatly overlap isolation boundaries provided by the platform. Third, the correctness of the mechanisms will be supported by formal models and proofs. To remain grounded and ensure practical relevance, we focus our work on two application domains: the Android operating system, and, secondarily, the Chromium web browser.
