The security of a software system relies on the principle of least privilege, which says that each software component must have only the privilege necessary for its execution and nothing else. Current programming languages do not provide adequate control over the privilege of untrusted software modules. To fill this gap, we designed and implemented a capability-based module system that facilitates controlling what resources each software module accesses. Then, we augmented our module system with an effect system that facilitates controlling how resources are used, i.e., authority over resources. Our approach simplifies the process of ensuring that a software system maintains the principle of least privilege. We implemented our solution as part of the Wyvern programming language.

In Wyvern, modules representing or using system resources, such as the file system and network, are considered to be security-critical and are designated as resource modules. References to resource modules are capability-protected, i.e., to access a resource module, the accessing module must have the appropriate capability. Using this feature, we designed our module system in such a way that it is obvious at compile time what capabilities a module have from looking at modules' interfaces and not their code. This property significantly simplifies the task of checking what capabilities a module holds. From a theoretical viewpoint, our capability analysis uses a novel, non-transitive notion of capabilities, which allows estimating the capabilities each module holds more precisely than in previous formal systems.

Further, leveraging the fact that effects are a good proxy for operations performed on a resource, we designed Wyvern's effect system that can account for the effects a module has on each resource. Our effect system is capability-based and allows specifying and enforcing what operations a module can perform on a resource it accesses, i.e., allows controlling the module's authority. Similarly to our modulesystem design, effect annotations that convey information about module authority are located in modules' interfaces, thus simplifying the task of checking resource usage.

We formalized both Wyvern's module system and effect system, and proved Wyvern to be capability- and authority-safe. We also assessed the effectiveness of the module system and the effect system that we designed in terms of how they would be used in practice and how they benefit a security-minded software developer writing an application. To do that, we implemented an extensible text-editor application in Wyvern and performed a security analysis on it.

129 pages

Thesis Committee:
Jonathan Aldrich (Chair)
Lujo Bauer
Limin Jia
Alex Potanin (University of Wellington)
Robert Biddle (Carleton University)

James D. Herbsleb, Director, Institute for Software Research
Martial Hebert, Dean, School of Computer Science

Return to: SCS Technical Report Collection
School of Computer Science

This page maintained by reports@cs.cmu.edu