Software Engineering Thesis Defense

  • DARYA MELICHER
  • Ph.D. Student
  • Ph.D. Program in Software Engineering, Institute for Software Research
  • Carnegie Mellon University
Thesis Orals

Controlling Module Privilege Using Programming Language Design

Security of a software system relies on the fact that each software component must have only the authority necessary for its execution and nothing else. Current programming languages do not provide adequate control over the authority of untrusted modules. To fill this gap, we designed and implemented a capability-based module system that facilitates controlling the security capabilities of software modules and then augmented our module system with an effect system to make our design authority-safe. Our approach, implemented as part of the Wyvern programming language, simplifies the process of ensuring that a software system maintains the principle of least privilege and also allows for attenuation of module authority.

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. Due to its design, Wyvern's module system allows a software developer to verify modules' capabilities at compile time by looking only at modules' interfaces and not at their code, thus significantly simplifying the task of controlling the capabilities a module holds. In addition, 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.

To be able to verify and control what exactly a module can do with a resource it accesses, i.e., the module's authority, we developed Wyvern's effect system, which can account for the effects a module has on each resource. Notably, an effect system is a good compromise, as it models authority rather than capabilities, but does so more precisely than by simply taking the transitive closure of capabilities. Similarly to our module system design, effect annotations that convey information about module authority located in modules' interfaces, thus simplifying the task of controlling resource usage.

Finally, we assessed the effectiveness of the two proposed language designs in terms of how they would be used in practice and how they benefit a security-minded software developer writing an application. To answer these questions, we implemented an extensible text-editor application in Wyvern and performed its security analysis.

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

For More Information, Please Contact: 
Keywords: