Open
Description
Context
- RustWeek - All Hands - Naming safety requirements & invariants (2025.05)
- Rust Safety Standard - Increasing the Correctness of unsafe Code (2024.09)
- RFC PATCH 0/5 Introduce the Rust Safety Standard (2024.07)
- Safety comments and atomicity requirements (2024.03)
Idea
Since tag-std currently is a PoC, there are several ways to apply it to R4L
- write a universal tool that can apply to any Rust project
- or enhance klint a static analysis tool/infrastructure in R4L
- or write a universal library that can be shared in different workflows/tools
- Feat: add tag-std and cargo-tag-std demo by driving rustc #1 demonstrates a normal workflow for single file and most cargo-based projects
- libstd needs a workflow: Black arts of verifying libcore/libstd os-checker/distributed-verification#52
- R4L needs its own: klint can reuse the library
- the main downside is multi-toolchains problem: StableMir should ideally solve this
cc #2
#![register_tool(klint)]
#[klint::NotNull(self.ptr)]
unsafe fn foo(&self) { ... }
Metadata
Metadata
Assignees
Labels
No labels
Type
Projects
Milestone
Relationships
Development
No branches or pull requests
Activity
hxuhack commentedon May 19, 2025
This work was originally not intended to support all Rust programs, but focused solely on the standard library. The main reason is that the safety properties may not generalize well or reach convergence. However, following a request from Rust-for-Linux and inspired by the work of asterinas, we believe it may be possible to extract a set of general safety tags for Rust-based operating systems as well. We’ve decided to begin exploring this direction and will keep our findings updated in os-sp.