RustBelt: Securing the Foundations of the Rust Programming Language¶
Jung, Jourdan, Krebbers, & Dreyer. (2018). RustBelt: Securing the Foundations of the Rust Programming Language: Securing the foundations of the Rust programming language. Proceedings of the ACM on Programming Languages, 1-34.
Cited by¶
2 citations across 2 artifacts.
Each citation links to the sentence it supports in the citing article.
Primes¶
- Property Rights
- Computer science: Capability-based access control, object ownership of mutable state, and resource-acquisition disciplines (such as Rust's ownership-and-borrowing model) enforce who may use, mutate, or delegate a resource, preventing the concurrent-access analogue of the tragedy of the commons — uncontrolled shared mutable state and the data races it produces.
This sourceFormal safety proof for Rust's ownership-and-borrowing model, in which a single owner holds the right to mutate state and aliased mutation is rejected; supports treating Rust ownership as an enforced exclusive entitlement preventing data races.
- Computer science: Capability-based access control, object ownership of mutable state, and resource-acquisition disciplines (such as Rust's ownership-and-borrowing model) enforce who may use, mutate, or delegate a resource, preventing the concurrent-access analogue of the tragedy of the commons — uncontrolled shared mutable state and the data races it produces.
Domain-specific¶
- Type System
- Linear and affine types (Rust's ownership and borrow system) track how many times a value may be used and who currently holds access to it, statically preventing data races and use-after-free errors — a guarantee that other safe languages buy at runtime with a garbage collector, and that static program verification can also supply, as RustBelt does by proving Rust's unsafe library internals sound in a separation logic
This sourceEstablishes that Rust's ownership and borrowing discipline statically rules out use-after-free and data races without a garbage collector — and, being itself a machine-checked separation-logic soundness proof for Rust's unsafe library internals, that static verification can supply the same guarantee.
- Linear and affine types (Rust's ownership and borrow system) track how many times a value may be used and who currently holds access to it, statically preventing data races and use-after-free errors — a guarantee that other safe languages buy at runtime with a garbage collector, and that static program verification can also supply, as RustBelt does by proving Rust's unsafe library internals sound in a separation logic
Verification¶
This reference passed the adversarial substantiation pipeline: it was checked to exist and to support the claim it is attached to. See how references were verified.
Registry ID ref:b93be6ddebc8 · see in the full table