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

现代个人计算的定义特征是朝向可扩展平台的趋势（例如，智能手机和平板电脑），运行大量的专业应用程序，许多质量或出处不确定。这些平台上可用的常见安全机制是应用程序隔离和权限系统。 不幸的是，事实一再表明，这些机制无法防止一系列不当行为，包括恶意升级攻击和信息流泄漏。 研究人员已经提出了对这些平台的信息流保护。然而，这样的机制很少被采用在实践中，部分原因是抽象的水平，他们允许政策被指定。我们开发了一个正式的，案例研究驱动的方法，将利用信息流研究的进展，开发新的政策规范语言和执法机制，为今天的可扩展环境。 首先，我们开发适当的策略规范语言，允许在抽象的中间级别指定策略。 策略规范将足够容易理解和制定，以便于大多数开发人员访问，同时具有足够的表达能力来支持丰富的策略。 第二，我们开发混合执行机制，以支持在抽象级别上指定的策略，这些抽象级别不会整齐地重叠平台提供的隔离边界。 第三，机制的正确性将得到形式化模型和证明的支持。 为了保持基础并确保实际相关性，我们将工作重点放在两个应用领域：Android操作系统和Chromium Web浏览器。

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.