The Holy Grail of Gradual Security

Abstract

Ensuring the security and privacy of personal data typically involves tracking and checking the flow of information, which can be performed either statically using a type system or dynamically using runtime monitoring. The dynamic approach of information-flow control (IFC) requires less effort from the programmer while the static approach provides stronger guarantees and less runtime overhead. Languages with gradual IFC combine static and dynamic techniques to prevent security leaks, so the programmer is free to choose when it is appropriate to increase the precision of type annotations and put in the effort to pass the static checks, versus when it is appropriate to reduce the precision of type annotations, thereby deferring the enforcement to runtime. Gradual programming languages should satisfy the gradual guarantee: programs that only differ in the precision of their type annotations should behave the same modulo cast errors. Unfortunately, Toro et al. [2018] identify a tension between the gradual guarantee and information security. They conjecture that it is not possible to enforce noninterference and satisfy the gradual guarantee.

In my PhD dissertation, I harmoniously combine static and dynamic enforcement of IFC in one programming language, λ^*_IFC, which satisfies both noninterference and the gradual guarantee at the same time without making any sacrifices. λ^*_IFC (1) enforces information flow security, (2) satisfies the gradual guarantee, (3) supports type-based reasoning, and (4) requires no extra static analysis prior to program execution. The key to the design of λ^*_IFC is to exclude the unknown label from runtime security labels. On the technical side, the semantics of λ^*_IFC is the first gradual information-flow control language to be specified using coercion calculi (a la Henglein). Casts in λ^*_IFC are represented by security coercions, which enforce the flow of information while satisfying the gradual guarantee.

I mechanize the proofs of type safety and the gradual guarantee for λ^*_IFC in the Agda proof assistant. I prove noninterference for λ^*_IFC by simulating λ^*_IFC with its dynamic extreme.

In summary, my thesis is that it is possible to design a gradual IFC programming language that satisfies noninterference and the gradual guarantee while supporting type-based reasoning, by excluding the unknown label from run-time security labels and using security coercions to represent casts.