Guardado en:
| Autores principales: | , |
|---|---|
| Formato: | Preprint |
| Publicado: |
2024
|
| Materias: | |
| Acceso en línea: | https://arxiv.org/abs/2410.01981 |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866909333748449280 |
|---|---|
| author | Blanc, Alex Le Lam, Patrick |
| author_facet | Blanc, Alex Le Lam, Patrick |
| contents | Rust aims to be a safe programming language applicable to systems programming applications. In particular, its type system has strong guardrails to prevent a variety of issues, such as memory safety bugs and data races. However, these guardrails can be sidestepped via the unsafe keyword. unsafe allows certain otherwise-prohibited operations, but shifts the onus of preventing undefined behaviour from the Rust language's compile-time checks to the developer. We believe that tools have a role to play in ensuring the absence of undefined behaviour in the presence of unsafe code. Moreover, safety aside, programs would also benefit from being verified for functional correctness, ensuring that they meet their specifications.
In this research proposal, we explore what it means to do Rust verification. Specifically, we explore which properties are worth verifying for Rust; what techniques exist to verify them; and which code is worth verifying. In doing so, we motivate an effort to verify safety properties of the Rust standard library, presenting the relevant challenges along with ideas to address them. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2410_01981 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Surveying the Rust Verification Landscape Blanc, Alex Le Lam, Patrick Programming Languages Rust aims to be a safe programming language applicable to systems programming applications. In particular, its type system has strong guardrails to prevent a variety of issues, such as memory safety bugs and data races. However, these guardrails can be sidestepped via the unsafe keyword. unsafe allows certain otherwise-prohibited operations, but shifts the onus of preventing undefined behaviour from the Rust language's compile-time checks to the developer. We believe that tools have a role to play in ensuring the absence of undefined behaviour in the presence of unsafe code. Moreover, safety aside, programs would also benefit from being verified for functional correctness, ensuring that they meet their specifications. In this research proposal, we explore what it means to do Rust verification. Specifically, we explore which properties are worth verifying for Rust; what techniques exist to verify them; and which code is worth verifying. In doing so, we motivate an effort to verify safety properties of the Rust standard library, presenting the relevant challenges along with ideas to address them. |
| title | Surveying the Rust Verification Landscape |
| topic | Programming Languages |
| url | https://arxiv.org/abs/2410.01981 |