Pluggable types allow programmers to extend a language's type system to enhance program correctness and program security. Unfortunately, pluggable types require annotations in the program, and therefore, place a burden on programmers. This annotation burden is one reason why pluggable types have not been widely adopted in practice. This project will develop techniques that will allow programmers to realize the benefits of pluggable types without incurring the annotation burden. One concrete application (and thrust of the project) tackles security and privacy of Android apps. Pluggable types will become more important, as JSR 308 (Type Annotation Specification) becomes part of Java 8 in 2014. The PI has developed a framework for inference and checking of context-sensitive pluggable types. The framework is instantiated to nontrivial systems and has inferred and checked close to a million lines of Java code in a modular and compositional manner. The key innovations in the framework are (i) support for context sensitivity, which allows instantiation to precise type systems such as Purity and Ownership, and (ii) a scalable inference engine, which allows type inference with zero or very small number of programmer annotations. The key insight is that viewpoint adaptation, a concept from Universe types, elegantly enables context sensitivity, both in the specification of the type system and in the type inference analysis. The project will advance the framework towards applications in concurrency, sustainable computing and security. Notably, the project will leverage the framework towards modular and compositional information flow analysis for Android; this will help address standing issues such as (i) the large Android library, and (ii) implicit information flow.
SHF: Small: Inference and Checking of Context-sensitive Pluggable Types