Quest Complete: the Holy Grail of Gradual Security
Fuente:
arXiv
Salvato in:
| Autori principali: | , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2023
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866913306581663744 |
|---|---|
| author | Chen, Tianyu Siek, Jeremy G. |
| author_facet | Chen, Tianyu Siek, Jeremy G. |
| contents | 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 $\mathrm{GSL}_\mathsf{Ref}$ 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, $λ_{\mathtt{IFC}}^\star$, that satisfies both noninterference and the gradual guarantee without making any sacrifices. We keep the type-guided classification of $\mathrm{GSL}_\mathsf{Ref}$ and use the standard no-sensitive-upgrade mechanism to prevent implicit flows through mutable references. The key to the design of $λ_{\mathtt{IFC}}^\star$ is to walk back the decision in $\mathrm{GSL}_\mathsf{Ref}$ to include the unknown label $\star$ among the runtime security labels. We give a formal definition of $λ_{\mathtt{IFC}}^\star$, prove the gradual guarantee, and prove noninterference. Of technical note, the semantics of $λ_{\mathtt{IFC}}^\star$ 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2312_02359 |
| institution | arXiv |
| publishDate | 2023 |
| record_format | arxiv |
| spellingShingle | Quest Complete: the Holy Grail of Gradual Security Chen, Tianyu Siek, Jeremy G. Programming Languages 68N15 D.3 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 $\mathrm{GSL}_\mathsf{Ref}$ 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, $λ_{\mathtt{IFC}}^\star$, that satisfies both noninterference and the gradual guarantee without making any sacrifices. We keep the type-guided classification of $\mathrm{GSL}_\mathsf{Ref}$ and use the standard no-sensitive-upgrade mechanism to prevent implicit flows through mutable references. The key to the design of $λ_{\mathtt{IFC}}^\star$ is to walk back the decision in $\mathrm{GSL}_\mathsf{Ref}$ to include the unknown label $\star$ among the runtime security labels. We give a formal definition of $λ_{\mathtt{IFC}}^\star$, prove the gradual guarantee, and prove noninterference. Of technical note, the semantics of $λ_{\mathtt{IFC}}^\star$ 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. |
| title | Quest Complete: the Holy Grail of Gradual Security |
| topic | Programming Languages 68N15 D.3 |
| url | https://arxiv.org/abs/2312.02359 |