Quest Complete: The Holy Grail of Gradual Security

Languages with gradual information-flow control combine static and dynamic techniques to prevent security leaks. Gradual 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 were unable to satisfy both properties in the language GSL Ref and had to settle for only satisfying information-flow security. Azevedo de Amorim et al. [ 2020 ] show that by sacrificing type-guided classification, one obtains a language that satisfies both noninterference and the gradual guarantee. Bichhawat et al. [ 2021 ] show that both properties can be satisfied by sacrificing the no-sensitive-upgrade mechanism, replacing it with a static analysis. In this paper we present a language design, λ IFC ★ , that satisfies both noninterference and the gradual guarantee without making any sacrifices. We keep the type-guided classification of GSL Ref and use the standard no-sensitive-upgrade mechanism to prevent implicit flows through mutable references. The key to the design of λ IFC ★ is to walk back the decision in GSL Ref to include the unknown label ★ among the runtime security labels. We give a formal definition of λ IFC ★ , prove the gradual guarantee, and prove noninterference. Of technical note, the semantics of λ IFC ★ is the first gradual information-flow control language to be specified using coercion calculi (a la Henglein), thereby expanding the coercion-based theory of gradual typing.