Reconciling noninterference and gradual typing
| Autor: | Matt Fredrikson, Limin Jia, Arthur Azevedo de Amorim |
|---|---|
| Rok vydání: | 2020 |
| Předmět: |
Correctness
Programming language Computer science Semantics (computer science) 020207 software engineering Gradual typing 0102 computer and information sciences 02 engineering and technology Type (model theory) computer.software_genre 01 natural sciences Feature (linguistics) Ascription 010201 computation theory & mathematics Secrecy 0202 electrical engineering electronic engineering information engineering Control (linguistics) computer |
| Zdroj: | LICS |
| Popis: | One of the standard correctness criteria for gradual typing is the dynamic gradual guarantee, which ensures that loosening type annotations in a program does not affect its behavior in arbitrary ways. Though natural, prior work has pointed out that the guarantee does not hold of any gradual type system for information-flow control. Toro et al.'s GSLRef language, for example, had to abandon it to validate noninterference. We show that we can solve this conflict by avoiding a feature of prior proposals: type-guided classification, or the use of type ascription to classify data. Gradual languages require run-time secrecy labels to enforce security dynamically; if type ascription merely checks these labels without modifying them (that is, without classifying data), it cannot violate the dynamic gradual guarantee. We demonstrate this idea with GLIO, a gradual type system based on the LIO library that enforces both the gradual guarantee and noninterference, featuring higher-order functions, general references, coarsegrained information-flow control, security subtyping and first-class labels. We give the language a domain-theoretic semantics, using Pitts' framework of relational structures to prove noninterference and the dynamic gradual guarantee. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|