Gradual Security Typing with References
Luminous Fennell, Peter J. Thiemann · 2013
Type systems for information-flow control (IFC) are often inflexible and too conservative. On the other hand, dynamic run-time monitoring of information flow is flexible and permissive but it is difficult to guarantee robust behavior of a program. Gradual typing for IFC enables the programmer to choose between permissive dynamic checking and a predictable, conservative static type system, where needed. We propose ML-GS, a monomorphic ML core language with references and higher-order functions that implements gradual typing for IFC. This language contains security casts, which enable the programmer to transition back and forth between static and dynamic checking. In particular, ML-GS enables non-trivial casts on reference types so that a reference can be safely used everywhere in a program regardless of whether it was created in a dynamically or statically checked part of the program. The reference can be shared between dynamically and statically checked parts. We prove the soundness of the gradual security type system along with termination insensitive non-interference.