Person: Dimoulas, Christos
Loading...
Email Address
AA Acceptance Date
Birth Date
Research Projects
Organizational Units
Job Title
Last Name
Dimoulas
First Name
Christos
Name
Dimoulas, Christos
5 results
Search Results
Now showing 1 - 5 of 5
Publication Declarative Policies for Capability Control(Institute of Electrical and Electronics Engineers, 2014) Dimoulas, Christos; Moore, Scott David; Askarov, Aslan; Chong, StephenIn 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.Publication SHILL: A Secure Shell Scripting Language(USENIX Association, 2014) Moore, Scott David; Dimoulas, Christos; King, Daniel; Chong, StephenThe 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.Publication Cryptographic Enforcement of Language-Based Information Erasure(2015) Askarov, Aslan; Moore, Scott; Dimoulas, Christos; Chong, StephenInformation erasure is a formal security requirement that stipulates when sensitive data must be removed from computer systems. In a system that correctly enforces erasure requirements, an attacker who observes the system after sensitive data is required to have been erased cannot deduce anything about the data. Practical obstacles to enforcing information erasure include: (1) correctly determining which data requires erasure; and (2) reliably deleting potentially large volumes of data, despite untrustworthy storage services. In this paper, we present a novel formalization of language-based information erasure that supports cryptographic enforcement of erasure requirements: sensitive data is encrypted before storage, and upon erasure, only a relatively small set of decryption keys needs to be deleted. This cryptographic technique has been used by a number of systems that implement data deletion to allow the use of untrustworthy storage services. However, these systems provide no support to correctly determine which data requires erasure, nor have the formal semantic properties of these systems been explained or proven to hold. We address these shortcomings. Specifically, we study a programming language extended with primitives for public-key cryptography, and demonstrate how information-flow control mechanisms can automatically track data that requires erasure and provably enforce erasure requirements even when programs employ cryptographic techniques for erasure.Publication Higher-order Behavioral Contracts for Distributed Components(2015) Waye, Lucas Reed; Dimoulas, Christos; Chong, StephenInspired by the Design by Contract paradigm, we introduce CONSUL, a contract system for distributed components. CONSUL monitors distributed components at run time with higher-order behavioral contracts. Contract monitoring is local to a component, and the component is treated as a black box. Thus it does not disturb the highly decoupled nature of distributed components and allows heterogeneous implementation languages and platforms without modifications to a component’s code. We describe the design, semantics and properties of CONSUL (adapter transparency and correct blame), and show that its contracts can capture and enforce precise and useful properties of a variety of off-the-shelf components.Publication Extensible Access Control with Authorization Contracts(2016-09-27) Scott Moore, Christos; Chong, Stephen; Moore, Scott David; Dimoulas, Christos; Findler, Robert Bruce; Flatt, MatthewExisting 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.