Papers › Quest Complete: the Holy Grail of Gradual Security
Quest Complete: the Holy Grail of Gradual Security
Tianyu Chen, Jeremy G. Siek
The archive published only this paper's code-link row. Authors, date and abstract are from arXiv's metadata (CC0), read from the Kaggle arXiv metadata snapshot of 2026-09-12 where its title matched the archive's; the title is the archive's.
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_(𝖱𝖾𝖿) 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_(𝖱𝖾𝖿) 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_(𝖱𝖾𝖿) 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.
Code
Repository list and official/mentioned flags are the archive's, frozen 2025-07-28. Reachability, where shown, is from one Syntology probe window (2026-09-16 to 2026-09-18); repositories not probed show nothing. GitHub stars are not tracked.
Code Syntology ran Syntology
Not run by Syntology. Nothing on this page verifies that the listed code works.
Results from the paper archive 2025-07-28
No leaderboard rows for this paper in the archive.
Report a problem or propose a change · a person checks every report against the paper or source before anything changes; decisions are listed on /corrections