Standard

RustBelt: securing the foundations of the rust programming language. / Jung, Ralf; Jourdan, Jacques-Henri; Krebbers, Robbert; Dreyer, Derek.

In: Proceedings of the ACM on Programming Languages, Vol. 2, No. POPL, 66, 01.2018, p. 66:1-66:34.

Research output: Contribution to journalArticleScientificpeer-review

Harvard

Jung, R, Jourdan, J-H, Krebbers, R & Dreyer, D 2018, 'RustBelt: securing the foundations of the rust programming language', Proceedings of the ACM on Programming Languages, vol. 2, no. POPL, 66, pp. 66:1-66:34. https://doi.org/10.1145/3158154

APA

Jung, R., Jourdan, J-H., Krebbers, R., & Dreyer, D. (2018). RustBelt: securing the foundations of the rust programming language. Proceedings of the ACM on Programming Languages, 2(POPL), 66:1-66:34. [66]. https://doi.org/10.1145/3158154

Vancouver

Jung R, Jourdan J-H, Krebbers R, Dreyer D. RustBelt: securing the foundations of the rust programming language. Proceedings of the ACM on Programming Languages. 2018 Jan;2(POPL):66:1-66:34. 66. https://doi.org/10.1145/3158154

Author

Jung, Ralf ; Jourdan, Jacques-Henri ; Krebbers, Robbert ; Dreyer, Derek. / RustBelt: securing the foundations of the rust programming language. In: Proceedings of the ACM on Programming Languages. 2018 ; Vol. 2, No. POPL. pp. 66:1-66:34.

BibTeX

@article{c948c5fb568149639317b13ad7ff98bb,
title = "RustBelt: securing the foundations of the rust programming language",
abstract = "Rust is a new systems programming language that promises to overcome the seemingly fundamental tradeoff between high-level safety guarantees and low-level control over resource management. Unfortunately, none of Rust's safety claims have been formally proven, and there is good reason to question whether they actually hold. Specifically, Rust employs a strong, ownership-based type system, but then extends the expressive power of this core type system through libraries that internally use unsafe features. In this paper, we give the first formal (and machine-checked) safety proof for a language representing a realistic subset of Rust. Our proof is extensible in the sense that, for each new Rust library that uses unsafe features, we can say what verification condition it must satisfy in order for it to be deemed a safe extension to the language. We have carried out this verification for some of the most important libraries that are used throughout the Rust ecosystem.",
author = "Ralf Jung and Jacques-Henri Jourdan and Robbert Krebbers and Derek Dreyer",
year = "2018",
month = jan,
doi = "10.1145/3158154",
language = "English",
volume = "2",
pages = "66:1--66:34",
journal = "Proceedings of the ACM on Programming Languages",
issn = "2475-1421",
number = "POPL",

}

RIS

TY - JOUR

T1 - RustBelt: securing the foundations of the rust programming language

AU - Jung, Ralf

AU - Jourdan, Jacques-Henri

AU - Krebbers, Robbert

AU - Dreyer, Derek

PY - 2018/1

Y1 - 2018/1

N2 - Rust is a new systems programming language that promises to overcome the seemingly fundamental tradeoff between high-level safety guarantees and low-level control over resource management. Unfortunately, none of Rust's safety claims have been formally proven, and there is good reason to question whether they actually hold. Specifically, Rust employs a strong, ownership-based type system, but then extends the expressive power of this core type system through libraries that internally use unsafe features. In this paper, we give the first formal (and machine-checked) safety proof for a language representing a realistic subset of Rust. Our proof is extensible in the sense that, for each new Rust library that uses unsafe features, we can say what verification condition it must satisfy in order for it to be deemed a safe extension to the language. We have carried out this verification for some of the most important libraries that are used throughout the Rust ecosystem.

AB - Rust is a new systems programming language that promises to overcome the seemingly fundamental tradeoff between high-level safety guarantees and low-level control over resource management. Unfortunately, none of Rust's safety claims have been formally proven, and there is good reason to question whether they actually hold. Specifically, Rust employs a strong, ownership-based type system, but then extends the expressive power of this core type system through libraries that internally use unsafe features. In this paper, we give the first formal (and machine-checked) safety proof for a language representing a realistic subset of Rust. Our proof is extensible in the sense that, for each new Rust library that uses unsafe features, we can say what verification condition it must satisfy in order for it to be deemed a safe extension to the language. We have carried out this verification for some of the most important libraries that are used throughout the Rust ecosystem.

UR - http://resolver.tudelft.nl/uuid:c948c5fb-5681-4963-9317-b13ad7ff98bb

U2 - 10.1145/3158154

DO - 10.1145/3158154

M3 - Article

VL - 2

SP - 66:1-66:34

JO - Proceedings of the ACM on Programming Languages

JF - Proceedings of the ACM on Programming Languages

SN - 2475-1421

IS - POPL

M1 - 66

ER -

ID: 40911273