Available, Reliable, and Secure Software: Still Going!

My research focuses on developing programming language technology to help programmers build software that is available, reliable, and secure. In this talk I will present an overview of my interests and general approach, and details on two research directions in particular.
The first half of the talk will present my work on dynamic software updating (DSU). For systems that require (or would prefer) continuous operation, software updates to fix bugs and vulnerabilities or upgrade functionality must be applied on-the-fly, without shutting the system down. I have spent the past decade developing a practical, general-purpose approach for achieving this goal. Our approach works for real software: we have dynamically applied years' worth of upgrades, corresponding to actual releases, of more than a dozen real servers written in C and Java. Our approach is well-founded: we have developed means to reason about, and tools to automatically verify, the correctness of dynamic updates. And our approach is non-intrusive: retrofitting an application to work with our system requires only a few changes, and its use imposes very little performance overhead.
The second half of the talk will describe my research on tool and language support for helping programmers avoid important classes of software errors. I will present an overview of three projects that illustrate interesting tradeoffs between static and dynamic program analysis: (1) Rubydust is an extension to the Ruby programming language that is able to infer general types for Ruby functions based on a few observed executions; these types can be used to help identify and debug errors before deployment. (2) Dynamic ownership checking is a technique I developed for dynamically checking lightweight concurrency specifications; specifications are very general and checking is low overhead. (3) Quantitative information flow tracking is a means of reasoning about secret information that might be revealed by the visible outputs of a program execution; our approach determines whether too much information may be revealed according to simple policies.
My talk will conclude with plans for future research.