TWC: Small: Language-level Control of Authority

现代计算机应用程序通常由不同的软件组件组成，这些软件组件由相互不信任的实体创建，或者可以代表相互不信任的实体起作用。为了确保计算机系统的安全，重要的是限制组件在计算机系统内执行操作的能力。最小权限原则规定，组件应该只被赋予执行其任务所需的能力(或权限)，而不应被赋予更多。如果遵循这一原则，并且组件是恶意的或有错误，则该组件对计算机系统的损害是有限的。然而，现有的构建计算机应用程序的技术使得执行最小权威原则变得困难。本项目旨在发展规范、推理和约束软件组件权限的基本思想和技术，以便更容易地遵循最小权限原则，从而提高计算机系统的安全性。项目期间开发的所有软件和工具都将公开发布，该项目将吸引研究生和本科生参与这项研究。该项目将调查和扩展语言级别的权限控制理论，并将使用该理论提供实用的工具和技术来推理和执行特定于应用程序的权限控制。这个项目试图探索三个研究方向。首先，开发一个基于语言的框架，用于设计和实现权限控制机制。该框架将提供可扩展和可组合的权限控制机制。其次，研究了基于语言的授权机制(包括可扩展授权机制)的理论。第三，研究授权机制和信息流控制之间的相互作用，以简化表达和精确的信息安全保证的执行。对于前两个方向，研究方法是：(1)开发能够捕捉被研究机制本质的形式语言模型；(2)形式化地描述模型的期望的语义属性；(3)开发可证明强制执行期望的语义属性的机制；(4)通过原型实现来验证模型和机制。对于第三个研究方向，研究方法是用信息流控制机制扩展形式语言模型和原型实现，并建立权限控制机制可以提供的信息安全保障。

Modern computer applications are typically made up of different software components that are created by, or may act on behalf of, mutually distrustful entities. To ensure the security of computer systems, it is important to restrict the ability of the components to perform actions within the computer system. The Principle of Least Authority states that a component should be given only the ability (or authority) it needs to perform its task, and no more. If this principle is followed, and a component is malicious or has errors, then the component is limited in the damage it can do to the computer system. However, existing techniques for building computer applications make it difficult to enforce the Principle of Least Authority. This project aims to develop the foundational ideas and technology to specify, reason about, and restrict the authority of software components, in order to make it easier to follow the Principle of Least Authority, and thereby improve the security of computer systems. All software and tools developed during the project will be publicly released, and the project will engage graduate and undergraduate students with this research.The project will investigate and extend the theory of language-level control of authority, and will use this theory to provide practical tools and techniques to reason about and enforce application-specific authority control. There are three research directions that this project seeks to explore. First, develop a language-based framework for the design and implementation of authority control mechanisms. The framework will provide extensible and composable authority control mechanisms. Second, investigate the theory of language-based authorization mechanisms (including extensible authorization mechanisms). Third, investigate the interaction between authorization mechanisms and information-flow control in order to simplify enforcement of expressive and precise information security guarantees. For the first two directions, the research approach is to: (1) develop formal language models that capture the essence of the mechanisms being investigated; (2) formally state desirable semantic properties of the models; (3) develop mechanisms that provably enforce the desirable semantic properties; (4) validate the models and mechanisms through prototype implementations. For the third research direction, the research approach is to extend the formal language models and prototype implementations with information-flow control mechanisms, and establish guarantees that authority control mechanisms can provide regarding information security.