In security-typed programming languages, types statically enforce noninterference between potentially conspiring values, such as the arguments and results of functions. But to adopt static security types, like other advanced type disciplines, programmers face a steep wholesale transition, often forcing them to refactor working code just to satisfy their type checker. To provide a gentler path to security typing that supports safe and stylish but hard-to-verify programming idioms, researchers have designed languages that blend static and dynamic checking of security types. Unfortunately most of the resulting languages only support static, type-based reasoning about noninterference if a program is entirely statically secured. This limitation substantially weakens the bene ts that dynamic enforcement brings to static security typing. Additionally, current proposals are focused on languages with explicit casts, and therefore do not ful ll the vision of gradual typing according to which the boundaries between static and dynamic checking only arise from the (im)precision of type annotations, and are transparently mediated by implicit checks.
In this paper we present GSLRef, a gradual security-typed higher-order language with references. As a gradual language, GSLRef supports the range of static-to-dynamic security checking exclusively driven by type annotations, without resorting to explicit casts. Additionally, GSLRef lets programmers use types to reason statically about termination-insensitive noninterference in all programs, even those that enforce security dynamically. We prove that GSLRef satis es all but one of Siek et al.’s criteria for gradually-typed languages, which ensure that programs can seamlessly transition between simple typing and security typing. A notable exception regards the dynamic gradual guarantee, which some speci c programs need to violate if they are required to satisfy noninterference; it remains an open question whether such a language could fully satisfy the dynamic gradual guarantee. To realize this design, we were led to draw a sharp distinction between syntactic type safety and semantic type soundness, each of which constrains the design of the gradual language.
Conference DayThu 17 JanDisplayed time zone: Belfast change
10:36 - 12:04
|Type-Driven Gradual Security with ReferencesTOPLAS|
Matías ToroUniversity of Chile, Ronald GarciaUniversity of British Columbia, Éric TanterUniversity of Chile & Inria ParisDOI Media Attached File Attached
|Gradual Type Theory|
Max NewNortheastern University, Dan LicataWesleyan University, Amal AhmedNortheastern University, USALink to publication DOI Media Attached File Attached
|Gradual Parametricity, RevisitedDistinguished Paper|
Matías ToroUniversity of Chile, Elizabeth LabradaUniversity of Chile, Éric TanterUniversity of Chile & Inria ParisLink to publication DOI Pre-print Media Attached File Attached
|Live Functional Programming with Typed Holes|
Cyrus OmarUniversity of Chicago, Ian VoyseyCarnegie Mellon University, Ravi ChughUniversity of Chicago, Matthew HammerNoneLink to publication DOI Pre-print Media Attached File Attached