An inference and checking framework for context-sensitive pluggable types.

摘要

Pluggable types enforce many important program properties. Programmers can use different pluggable type systems to prevent unforeseen runtime errors, facilitate parallelism, program understanding, model checking, and more. With the addition of JSR 308 to Java 8 released in March 2014, pluggable types become part of standard Java.;This thesis presents a framework for specifying, inferring and checking of context- sensitive pluggable types. By supplying a few framework parameters programmers can instantiate the framework's unified typing rules into concrete rules for a specific type system. The framework then takes as input an unannotated or a partially annotated program, infers the most desirable typing (according to the input parameters), and verifies the correctness of the typing. Programmers can use the framework to infer and plug existing type systems, as well as build new type systems.;This thesis presents several instantiations of interesting pluggable type systems: (1) a context-sensitive type system ReIm for reference immutability and an efficient quadratic type inference analysis, (2) the first effective type inference analysis for the classical Ownership Types, (3) a novel quadratic type inference analysis for Universe Types, (4) a context-sensitive type system SFlow/Integrity for detecting information flow vulnerabilities in Java web applications and a novel, worst-case cubic inference analysis, and (5) the dual type system SFlow/Confidentiality for detecting privacy leaks in Android apps and the corresponding inference analysis; the analysis scales well and detects leaks in apps from the Google Play Store and in known malware.