Jonathan Aldrich
Using Capability-Based Modules to Enforce Secure Resource Usage
August 23, 2016 at 12:00pm
CSE 305
Abstract
Many security properties concern how resources such as the network or file system are used. Unfortunately, today’s programming languages provide approaches to controlling resource use that are difficult to use and error-prone. We propose controlling access to resources via capabilities, and then integrating capabilities into the language and module system in order to control how different code modules can use various resources. Through a formal effect system, we elucidate a key technical benefit of capabilities: the ability to reason about the effect of a body of code without analyzing its implementation. We discuss design issues in capability-safe languages and show several security-related applications of capability-based modules.
Bio
Jonathan Aldrich is Associate Professor of Computer Science at Carnegie Mellon University. He has a Ph.D. from the University of Washington, is the director of CMU’s Software Engineering Ph.D. program and the program chair of OOPSLA 2017. His research centers on programming languages, type systems, and tools that are motivated by and evaluated according to software engineering principles. With his students, Jonathan is currently developing the programming language Wyvern, which features extensible syntax, a capability-based module system, and a gradual verification system. He has also worked on typestate checking, empirical analysis of the benefits of type systems, and novel object-oriented language models.