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

可插拔类型允许程序员扩展语言的类型系统，以增强程序的正确性和程序的安全性。不幸的是，可插拔类型需要在程序中使用注释，因此给程序员带来了负担。这种注释负担是可插入类型在实践中没有被广泛采用的原因之一。该项目将开发一些技术，使程序员能够在不招致注释负担的情况下实现可插入类型的好处。一个具体的应用程序(也是该项目的主旨)解决了Android应用程序的安全和隐私问题。随着JSR 308(类型注释规范)在2014年成为Java 8的一部分，可推送类型将变得更加重要。PI已经开发了一个框架，用于推断和检查上下文相关的可插拔类型。该框架被实例化为重要的系统，并以模块化和组合的方式推断和检查了近一百万行Java代码。该框架中的关键创新是(I)支持上下文敏感，这允许实例化到精确的类型系统，如纯净度和所有权，以及(Ii)可伸缩的推理引擎，允许使用零个或非常少的程序员注释进行类型推理。关键的洞察是，视点适应，一个来自宇宙类型的概念，在类型系统的规范和类型推理分析中都优雅地使上下文敏感。该项目将推动该框架在并发、可持续计算和安全方面的应用。值得注意的是，该项目将利用该框架对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.