Person:
Moore, Scott David

Profile Picture

Email Address

AA Acceptance Date

Birth Date

Research Projects

Organizational Units

Job Title

Last Name

Moore

First Name

Scott David

Name

Moore, Scott David
Author's Publications: search.filters.isAuthorOfPublication.6c548628-3e8a-4bfe-83c9-78706524c188

Search Results

Now showing 1 - 8 of 8
  • No Thumbnail Available
    Publication
    Software Contracts for Security
    (2016-08-11) Moore, Scott David; Chong, Stephen; Kohler, Eddie; Mickens, James
    Component-based software engineering facilitates the design of complex systems by subdividing the programming task into separate components that interact via clearly defined interfaces. A component-based system is correct only when each component satisfies its specification and the interactions between different components satisfy their respective interfaces. "Design by Contract" is a programming methodology that enforces these requirements by attaching executable specifications to components. These contracts monitor the system's execution and interfere when a specification would be violated. Designing a program this way gives assurance that the program is correct. It eliminates defensive programming by separating code that validates the correct use of a component from the component's implementation. It also simplifies debugging by localizing program errors within the component that violated its specification. However, existing work on software contracts focuses almost exclusively on contracts for functional correctness. This dissertation argues that higher-order software contracts are an effective mechanism to specify and enforce composable, easy-to-understand security properties. Whereas traditional software contracts describe what a component requires from its clients and provides in return, software contracts for security enforce limits on the contexts in which components can be used. The first part of this dissertation shows how existing software contracts can be combined with language restrictions to write and enforce declarative security specifications. Based on this design, I develop a secure shell scripting language. The second part introduces authorization contracts, a new type of software contract that can implement a wide range of commonly used security mechanisms without requiring language modifications.
  • Thumbnail Image
    Publication
    Declarative Policies for Capability Control
    (Institute of Electrical and Electronics Engineers, 2014) Dimoulas, Christos; Moore, Scott David; Askarov, Aslan; Chong, Stephen
    In capability-safe languages, components can access a resource only if they possess a capability for that resource. As a result, a programmer can prevent an untrusted component from accessing a sensitive resource by ensuring that the component never acquires the corresponding capability. In order to reason about which components may use a sensitive resource it is necessary to reason about how capabilities propagate through a system. This may be difficult, or, in the case of dynamically composed code, impossible to do before running the system. To counter this situation, we propose extensions to capability-safe languages that restrict the use of capabilities according to declarative policies. We introduce two independently useful semantic security policies to regulate capabilities and describe language-based mechanisms that enforce them. Access control policies restrict which components may use a capability and are enforced using higher-order contracts. Integrity policies restrict which components may influence (directly or indirectly) the use of a capability and are enforced using an information-flow type system. Finally, we describe how programmers can dynamically and soundly combine components that enforce access control or integrity policies with components that enforce different policies or even no policy at all.
  • Thumbnail Image
    Publication
    SHILL: A Secure Shell Scripting Language
    (USENIX Association, 2014) Moore, Scott David; Dimoulas, Christos; King, Daniel; Chong, Stephen
    The Principle of Least Privilege suggests that software should be executed with no more authority than it requires to accomplish its task. Current security tools make it difficult to apply this principle: they either require significant modifications to applications or do not facilitate reasoning about combining untrustworthy components. We propose SHILL, a secure shell scripting language. SHILL scripts enable compositional reasoning about security through contracts that limit the effects of script execution, including the effects of programs invoked by the script. SHILL contracts are declarative security policies that act as documentation for consumers of SHILL scripts, and are enforced through a combination of language design and sandboxing. We have implemented a prototype of SHILL for FreeBSD and used it for several case studies including a grading script and a script to download, compile, and install software. Our experience indicates that SHILL is a practical and useful system security tool, and can provide fine-grained security guarantees.
  • Thumbnail Image
    Publication
    Precise Enforcement of Progress-Sensitive Security
    (ACM Press, 2012) Moore, Scott David; Askarov, Aslan; Chong, Stephen
    Program progress (or termination) is a covert channel that may leak sensitive information. To control information leakage on this channel, semantic definitions of security should be progress sensitive and enforcement mechanisms should restrict the channel's capacity. However, most state-of-the-art language-based information-flow mechanisms are progress insensitive---allowing arbitrary information leakage through this channel---and current progress-sensitive enforcement techniques are overly restrictive. We propose a type system and instrumented semantics that together enforce progress-sensitive security more precisely than existing approaches. Our system is permissive in that it is able to accept programs in which the termination behavior depends only on low-security (e.g., public or trusted) information. Our system is parameterized on a termination oracle, and controls the progress channel precisely, modulo the ability of the oracle to determine the termination behavior of a program based on low-security information. We have instantiated the oracle for a simple imperative language with a logical abstract interpretation that uses an SMT solver to synthesize linear rank functions. In addition, we extend the system to permit controlled leakage through the progress channel, with the leakage bound by an explicit budget. We empirically analyze progress channels in existing Jif code. Our evaluation suggests that security-critical programs appear to satisfy progress-sensitive security.
  • Thumbnail Image
    Publication
    Exploring and enforcing security guarantees via program dependence graphs
    (ACM Press, 2015) Johnson, Andrew Arthur; Wayne, Lucas; Moore, Scott David; Chong, Stephen
    We present PIDGIN, a program analysis and understanding tool that enables the specification and enforcement of precise application-specific information security guarantees. PIDGIN also allows developers to interactively explore the information flows in their applications to develop policies and investigate counter-examples. PIDGIN combines program dependence graphs (PDGs), which precisely capture the information flows in a whole application, with a custom PDG query language. Queries express properties about the paths in the PDG; because paths in the PDG correspond to information flows in the application, queries can be used to specify global security policies. PIDGIN is scalable. Generating a PDG for a 330k line Java application takes 90 seconds, and checking a policy on that PDG takes under 14 seconds. The query language is expressive, supporting a large class of precise, application-specific security guarantees. Policies are separate from the code and do not interfere with testing or development, and can be used for security regression testing. We describe the design and implementation of PIDGIN and report on using it: (1) to explore information security guarantees in legacy programs; (2) to develop and modify security policies concurrently with application development;and (3) to develop policies based on known vulnerabilities.
  • Thumbnail Image
    Publication
    Extensible Access Control with Authorization Contracts
    (2016-09-27) Scott Moore, Christos; Chong, Stephen; Moore, Scott David; Dimoulas, Christos; Findler, Robert Bruce; Flatt, Matthew
    Existing programming language access control frameworks do not meet the needs of all software components.We propose an expressive framework for implementing access control monitors for components. The basis of the framework is a novel concept: the authority environment. An authority environment associates rights with an execution context. The building blocks of access control monitors in our framework are authorization contracts: software contracts that manage authority environments. We demonstrate the expressiveness of our framework by implementing a diverse set of existing access control mechanisms and writing custom access control monitors for three realistic case studies.
  • Thumbnail Image
    Publication
    Exploring and Enforcing Application Security Guarantees vis Program Dependence
    (2014) Johnson, Andrew; Waye, Lucas Reed; Moore, Scott David; Chong, Stephen
    We present Pidgin, a program analysis and understanding tool that allows developers to explore the information flows that exist in programs and specify and enforce security policies that restrict these information flows. Pidgin uses program-dependence graphs (PDGs) to precisely capture the information flows within a program. PDGs can be queried using a custom query language to explore and describe information flows in programs. A developer can specify strong information security policies by asserting that specific queries return no results (i.e., asserting the absence of certain information flows in the program). To check whether a program satisfies a security policy, a developer can simply evaluate the query against a program’s dependence graph. The query language is expressive, supporting a large class of precise, application-specific security guarantees. Pidgin can be used to explore information security guarantees in legacy programs, or to support the specification, enforcement, and modification of information security requirements during program development. We describe the design and implementation of Pidgin and report on using Pidgin both to explore security guarantees in existing open-source applications, and to specify and enforce security guarantees during application development.
  • Thumbnail Image
    Publication
    Static Analysis for Efficient Hybrid Information-Flow Control
    (IEEE Computer Society, 2011) Moore, Scott David; Chong, Stephen
    Hybrid information-flow monitors use a combination of static analysis and dynamic mechanisms to provide precise strong information security guarantees. However, unlike purely static mechanisms for information security, hybrid information-flow monitors incur run-time overhead. We show how static analyses can be used to make hybrid information- flow monitors more efficient, in two ways. First, a simple static analysis can determine when it is sound for a monitor to stop tracking the security level of certain variables. This potentially reduces run-time overhead of the monitor, particularly in applications where sensitive (i.e., confidential or untrusted) data is infrequently introduced to the system. Second, we derive sufficient conditions for soundly incorporating a wide range of memory abstractions into information- flow monitors. This allows the selection of a memory abstraction that gives an appropriate tradeoff between efficiency and precision. It also facilitates the development of innovative and sound memory abstractions that use run-time security information maintained by the monitor. We present and prove our results by extending the information-flow monitor of Russo and Sabelfeld (2010). These results bring us closer to efficient, sound, and precise enforcement of information security.