A Type System to Ensure Non-Interference in ReScript
Fuente:
arXiv
Guardado en:
| Autores principales: | , , , , , |
|---|---|
| Formato: | Preprint |
| Publicado: |
2024
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866909361647910912 |
|---|---|
| author | Bennetzen, Benjamin Kleist, Daniel Vang Steinmann, Emilie Sonne Walsted, Loke Kristensen, Nikolaj Rossander Steffensen, Peter Buus |
| author_facet | Bennetzen, Benjamin Kleist, Daniel Vang Steinmann, Emilie Sonne Walsted, Loke Kristensen, Nikolaj Rossander Steffensen, Peter Buus |
| contents | Protecting confidential data from leaking is a critical challenge in computer systems, particularly given the growing number of observers on the internet. Therefore, limiting information flow using robust security policies becomes increasingly vital. We focus on the non-interference policy, where the goal is to ensure that confidential data can not impact public data. This paper presents a type system, for a subset of the ReScript syntax, designed to enforce non-interference. We conclude with a proof of soundness for the type system, demonstrating that if an expression is type-able, it is inherently non-interferent. In addition, we provide a brief overview of a type checker that implements the previously mentioned type system. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2410_18157 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | A Type System to Ensure Non-Interference in ReScript Bennetzen, Benjamin Kleist, Daniel Vang Steinmann, Emilie Sonne Walsted, Loke Kristensen, Nikolaj Rossander Steffensen, Peter Buus Cryptography and Security Programming Languages Protecting confidential data from leaking is a critical challenge in computer systems, particularly given the growing number of observers on the internet. Therefore, limiting information flow using robust security policies becomes increasingly vital. We focus on the non-interference policy, where the goal is to ensure that confidential data can not impact public data. This paper presents a type system, for a subset of the ReScript syntax, designed to enforce non-interference. We conclude with a proof of soundness for the type system, demonstrating that if an expression is type-able, it is inherently non-interferent. In addition, we provide a brief overview of a type checker that implements the previously mentioned type system. |
| title | A Type System to Ensure Non-Interference in ReScript |
| topic | Cryptography and Security Programming Languages |
| url | https://arxiv.org/abs/2410.18157 |