Typing under Incomplete Information

The aim of this project is to improve the ability of type systems to detect certain classes of error, improving the correctness of code. Correctness focuses on information security, and within string manipulating programs. We have two sub-aims in this project: increasing the usability of security typing and creating an in-language subtype relation for strings. Both sub-aims are intended to make the task for the developer easier: we will use search-based and information-theoretic means to suggest annotations locations and contents. The student will use core lambda calculi to study optional security type systems.
This is appropriate to the novelty of the approach and current research standards. String subtyping will focus on theoretical approaches and implementation of these approaches in popular programming languages, such as Java and TypeScript. This work is part of programming language design and use.

Gradual typing is an existing approach to making security typing easier to use.
Gradual typing mixes static typing (done at compile time) with dynamic typing (done while a program is running). Gradual security typing suffers from the problem that correctly inferring a security policy from partial information is undecidable. We approach these problems with an optional type system, coupled with QIF (Quantified Information Flow) to address the undecidability. We measure the leakage of information from unannotated regions and use it to rank investigation zones: those parts of the unannotated code that most require policy appropriate security labelling.

Typing for strings is difficult because a string is a "black box" to a type checker, even though most strings used in computer programs are highly structured. Our solution to this problem uses embedded grammars to expose this latent structure to the type checker. We have developed an expressive approach to string type checking, SafeStrings, that uses only the native mechanisms of a target programming language to bring increased type safety, and testing efficiency, to string-controlled programs. We used search-based methods to assist the developer in knowing where to annotate, maximising the impact of the annotation on the overall correctness of a program.

Our novel contributions are: the first optional security type system for the polymorphic lambda calculus (System F). We are the first to use information theory to suggest placements for type annotations. We make a novel use of information flow ranking (RIF) to reduce the cost of exact QIF calculation.
SafeStrings is the first approach to use grammars as a means of generating an in-language, type-based, subsumption relation for strings. We also show that this approach is realistic by performing a large-scale study of how strings are used in programming languages.