Visible to the public Gradual Security Types and Gradual Guarantees

TitleGradual Security Types and Gradual Guarantees
Publication TypeConference Paper
Year of Publication2021
AuthorsBichhawat, Abhishek, McCall, McKenna, Jia, Limin
Conference Name2021 IEEE 34th Computer Security Foundations Symposium (CSF)
Date Publishedjun
Keywordsannotations, compiler security, composability, computer security, gradual guarantees, gradual typing, Information Flow Control, Metrics, Monitoring, noninterference, pubcrawl, Refining, Resiliency, Runtime, Semantics
AbstractInformation flow type systems enforce the security property of noninterference by detecting unauthorized data flows at compile-time. However, they require precise type annotations, making them difficult to use in practice as much of the legacy infrastructure is written in untyped or dynamically-typed languages. Gradual typing seamlessly integrates static and dynamic typing, providing the best of both approaches, and has been applied to information flow control, where information flow monitors are derived from gradual security types. Prior work on gradual information flow typing uncovered tensions between noninterference and the dynamic gradual guarantee- the property that less precise security type annotations in a program should not cause more runtime errors.This paper re-examines the connection between gradual information flow types and information flow monitors to identify the root cause of the tension between the gradual guarantees and noninterference. We develop runtime semantics for a simple imperative language with gradual information flow types that provides both noninterference and gradual guarantees. We leverage a proof technique developed for FlowML and reduce noninterference proofs to preservation proofs.
DOI10.1109/CSF51468.2021.00015
Citation Keybichhawat_gradual_2021