TWC: Small: Provably Enforcing Practical Multi-Layer Policies in Today's Extensible Software Platforms

现代个人计算的一个决定性特征是朝着可扩展平台(例如，智能手机和平板电脑)的趋势发展，这些平台运行大量专门的应用程序，其中许多应用程序的质量或来源不确定。这些平台上可用的常见安全机制是应用程序隔离和权限系统。不幸的是，事实一再表明，这些机制无法防止一系列不当行为，包括特权提升攻击和信息流泄漏。研究人员提出了对这些平台的信息流保护措施。然而，这种机制很少在实践中被采用，部分原因是它们允许指定策略的抽象级别。我们开发了一种正式的、案例研究驱动的方法，该方法将利用信息流研究的进展来为当今可扩展的环境开发新的策略规范语言和执行机制。首先，我们开发适当的策略规范语言，允许在中间抽象级别指定策略。策略规范将非常容易理解和制定，以便大多数开发人员能够访问，但又具有足够的表现力来支持丰富的策略。其次，我们开发混合实施机制来支持在抽象级别指定的策略，这些抽象级别不会整齐地重叠平台提供的隔离边界。第三，这些机制的正确性将得到正式模型和证明的支持。为了保持脚踏实地并确保实用性，我们将工作重点放在两个应用领域：Android操作系统，以及第二个领域，Chromium网络浏览器。

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.