Office: 9105 Gates & Hillman Centers
In my research, I design novel programming languages and verification techniques that enable software developers to create programs that are provably efficient, safe, and secure.
I am particularly interested in quantitative properties of programs and their dependencies on the surrounding software and hardware environments. Examples include energy usage, execution time, stack-space usage, and amount of leaked information or privacy. Such properties are inextricably linked with every program and should serve as objective quality measures and guiding principles in programming. Despite their importance, there are still few practical tools that help programmers to reason about quantitative properties of their code.
My research mission is to develop techniques and tools for quantitative analysis and verification that are compositional, efficient, and simple enough to be used by software developers without excessive training. This is a challenging problem that involves diverse areas such as formal methods, programming languages, constraint solving, analysis of algorithms, and design and implementation of systems.
Resource-Usage AnalysisQuantitative resource-usage analysis of software has inspired some of the most exciting research in computer science, which ranges from systems (e.g., non-blocking algorithms and real-time operating systems) to theory (e.g., complexity theory and analysis of algorithms). Nevertheless, it is still challenging for software developers to understand the quantitative performance characteristics of their code: On the one hand, software systems are increasingly complex, concurrent, and distributed. On the other hand, developers rely more and more on off-the-shelf software libraries and software is executed using cloud services that are black boxes with respect to resource usage. The failure of having a precise understanding of the resource usage of programs is at the root of many problems of software:
- Performance bugs, as seen for example at the healthcare.gov website of the US government in fall 2013, are common and expensive.
- Increasing complexity makes it difficult to correctly predict the timing of safety-critical real-time systems.
- Stack overflow continues to be a serious and common problem in embedded systems.
- Energy bugs regularly drain the battery of mobile devices and autonomous systems.
To address these problems, I work on new ways to model and analyze resource usage. For instance, I developed an automatic resource analysis system that derives tight worst-case bounds for functional programs. It is the first automatic analysis system that finds bounds for classical examples such as quick sort and insertion sort for lists of lists, longest common subsequence via dynamic programming, or Dijkstra's single-source shortest-path algorithm. The analysis is type-based and uses a novel polynomial amortized resource analysis that is highly compositional and can efficiently derive precise polynomial bounds for complex and realistic programs. This analysis system is implemented in the programming language Resource Aware ML.
Security and PrivacyCybersecurity is a major concern of governments and companies around the world and the privacy of individuals is hard to protect in the presence of big data and surveillance programs of government agencies. Software vulnerabilities and backdoors pose a threat to our security and privacy. Unfortunately, it is impossible in many applications to prove that software does not leak secret or private information. For example, a failed login attempt leaks information about the secure password. As a result, security and privacy often need to be expressed by quantitative properties — such as differential privacy and quantitative information flow — that express how much private or secret information is leaked.
From a technical perspective, quantitative security and privacyproperties are closely related to quantitative performance characteristics. For instance, we need bounds on the number of loop iterations and recursion depths to provide quantitative, static guarantees. I am developing new ways of reasoning about quantitative security and privacy properties. For instance, I work with collaborators from industry and academia on applying quantitative analysis to find space or time-based side channels in Java bytecode.