2023/12/04 by Tianyu Chen, Chen, Tianyu, Jeremy G. Siek +1 · 1 citation
Computer Science · Materials Science · #68N15 #Advanced Malware Detection Techniques #D.3 #Diamond and Carbon-based Materials Research #FOS: Computer and information sciences #Programming Languages (cs.PL) #Security and Verification in Computing
paper · pdf · doi:10.48550/arxiv.2312.02359
openalex publication_date 2023/12/04 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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 GSLRef 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, λ_\mathttIFC^⋆, that satisfies both noninterference and the gradual guarantee without making any sacrifices. We keep the type-guided classification of GSLRef and use the standard no-sensitive-upgrade mechanism to prevent implicit flows through mutable references. The key to the design of λ_\mathttIFC^⋆ is to walk back the decision in GSLRef to include the unknown label ⋆ among the runtime security labels. We give a formal definition of λ_\mathttIFC^⋆, prove the gradual guarantee, and prove noninterference. Of technical note, the semantics of λ_\mathttIFC^⋆ 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.