SHF: Small: Inference and Checking of Context-sensitive Pluggable Types

可插入类型允许程序员扩展语言的类型系统，以增强程序的正确性和安全性。不幸的是，可插入类型需要在程序中进行注释，因此给程序员带来了负担。这种注释负担是可插类型在实践中没有被广泛采用的原因之一。该项目将开发一些技术，使程序员能够在不增加注释负担的情况下实现可插拔类型的好处。一个具体的应用程序（也是这个项目的重点）解决了Android应用程序的安全和隐私问题。随着JSR 308（类型注释规范）在2014年成为Java 8的一部分，可插拔类型将变得更加重要。PI开发了一个框架，用于推断和检查上下文敏感的可插拔类型。该框架被实例化为重要的系统，并以模块化和组合的方式推断和检查了近一百万行Java代码。该框架的关键创新是(i)支持上下文敏感性，它允许实例化精确的类型系统，如Purity和Ownership，以及（ii）一个可扩展的推理引擎，它允许在没有或非常少的程序员注释的情况下进行类型推理。关键的见解是，视点适应（来自Universe类型的一个概念）在类型系统的规范和类型推断分析中都很好地实现了上下文敏感性。该项目将推进该框架在并发、可持续计算和安全性方面的应用。值得注意的是，该项目将利用框架实现Android的模块化和组合信息流分析；这将有助于解决诸如(i)大型Android库和（ii）隐式信息流等问题。

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.