First-order Gradual Information Flow Types with Gradual Guarantees

Abhishek Bichhawat, McKenna McCall, Limin Jia

Information flow type systems enforce the security property of noninterference by detecting unauthorized data flows at compile-time. However, they require precise type annotations,…