TWC: Small: Language-level Control of Authority

点击翻译按钮获取中文摘要

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.