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

SHF：小：上下文相关可插拔类型的推理和检查

• 批准号: 1319384
• 负责人: Ana Milanova
• 金额: $ 31.51万
• 依托单位: Rensselaer Polytechnic Institute
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2013
• 资助国家: 美国
• 起止时间: 2013-09-01 至 2019-08-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1319384&HistoricalAwards=false
• 关键词: SHF; Small; Inference; Checking; Context

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.

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