Pre-RFC: Safety Property System

libs
1

The full proposal document is in our tag-std repository. It's too long to read in this post, considering there are more conversations going on.

We are experimenting this feature on verify-rust-std, Rust for Linux, and Asterinas OS.

Any idea and feedback is welcome! :heart:

Summary

This RFC proposes a DSL (domain-specific language)-based mechanism for specifying safety properties, aiming to standardize how safety descriptions are written in API documentation. On the one hand, it seeks to improve the ergonomics of writing safety descriptions; on the other hand, these safety properties can enable finer-grained unsafe code management and automated safety checking.

This RFC operates at the API level rather than the compiler or language level, as it merely introduces attribute macros on functions and expressions that are already expressible today, but may require a linter tool to realize automated check.

This RFC has influences on the entire crate ecosystem, including the standard library and downstream crates.

Demo

Ensure safety requirements are never missing

fn try_fold<B, F, R>(&mut self, mut init: B, mut f: F) -> R {
    ...

    init = head.iter().map(|elem| {
        guard.consumed += 1;

        #[safety::discharges::ValidPtr(elem, T, 1)]
        #[safety::discharges::Aligned(elem, T)]
        #[safety::discharges::Init(elem, T, 1)]
        #[safety::discharges::NotOwned(elem, memo = "
          Because we incremented `guard.consumed`, the deque 
          effectively forgot the element, so we can take ownership.
        ")]
        #[safety::discharges::Alias(elem, head.iter())]
        unsafe { ptr::read(elem) }
    })
    .try_fold(init, &mut f)?;

    ...
}

Update: we will make the syntax less verbose, like this

#[safety { ValidPtr(ptr) }] // defsite: add SP on this API
unsafe fn raw_get_work(ptr: *mut Self) -> *mut Work<T, ID> {
    let ptr = ptr as *mut u8;

    #[safety { InBound, ValidNum }] // callsite: discharge SP
    unsafe { ptr.add(Self::OFFSET).cast() }
}

see Pre-RFC: Safety Property System - #23 by vague

Generate proper doc comments from tags

1638×1011 146 KB

4 Likes
Unsafe assertion invariants
2

I'm very much in favor of machine-checkable safety annotations in some form, and I like the idea of getting there by refining the existing human-readable free-form safety comments.

However, I would like to ask how your scheme would handle a lengthy unsafe code block whose safety presumes the well-formedness of a complex data structure produced on the other side of an FFI boundary. This is the most common reason for unsafe in the code I tend to write, and previous proposals (e.g. the "Unsafe Reasons" pre-RFC) have involved adding so many annotations inside the unsafe block that they would make it difficult to follow the actual logic of the code within.

I posted a concrete example of the kind of code I'm talking about in the "Unsafe Reasons" pre-RFC thread; the full code from which that example was cut down can be found here and here.

1 Like
3

When someone did an unsafe review of one of my libraries, the safety of one section was dependent on the value of a constant and they wanted a comment on that constant to clarify how it was helping meet the safety goal. One of my big concerns for this was this created an implicit dependence on that constant and the callers and I would want there to be some kind of way to programmatically validate this.

Would this fit within this scheme at all?

1 Like
4

Have you seen GitHub - flux-rs/flux: Refinement Types for Rust?

1 Like
5

I think you would just need to be able to define custom safety properties like MyStructureIsValid rather than ValidPtr etc.

But if this is possible (and I hope it is), what about partially discharging a safety property, rather than treating them as something atomic? You need this to make this system truly composable.

I mean, some unsafe blocks may need to work together with other unsafe blocks to make sure an invariant is held (if one unsafe run, but not the other, the structure will be left in an invalid state). To represent this situation, each of them might discharge just part of some invariant.

Maybe this can be achieved like this: the system must be able to conclude that, if MyStructureIsValid is defined as "some ptr is valid, aligned, initialized, (etc, etc)", then if I discharge all those things individually, then it should count as if MyStructureIsValid is discharged. So maybe it's enough if the custom safety property is just an alias or something like that.

But for more complex reasoning it really would pay off to have more finer grained logical relationships properties. For example: you could imagine two properties that, together, imply another property (for example, if I initialize each field of a struct separately, the struct should be considered initialized). Those properties could be discharged by different unsafe code (like, two different places will each initialize a field).

6

I don't think there will be a tagging system that could comprehensively represent all the safety requirements.

For example, let's say we are writing a Rust library:

pub struct ManagerIndex(usize);

pub struct Manager {
    raw: Vec<Foo>,
}

impl Manager {
    pub fn create_new_foo(&mut self, foo: Foo) -> ManagerIndex {
        let index = self.raw.len();
        self.raw.push(foo);
        ManagerIndex(index)
    }

    pub fn clear(&mut self) {
        self.raw.clear();
    }

    pub fn get_foo_mut(&mut self, index: ManagerIndex) -> &mut Foo {
        let ManagerIndex(index) = index;
        unsafe { self.raw.get_unchecked_mut(index) }
    }
}

There are three public APIs of Manager struct. Which should be marked as unsafe?

Usually, the get_foo_mut would be marked as unsafe, which can be applied with the tag system. However, if this function call is very common across the crate, it's also a common practice to mark clear as unsafe instead of get_foo_mut, and the safety contract of clear would be "All indices produced before should be discarded and shall never be used afterwards."

By marking clear unsafe, there are no conflicts with Rust's safety requirements, and the API is more ergonomic.

The example above shows that, the safety requirement of unsafe can be very arbitrary, and is still valid.

7

This proposal does not address the API safety declaration - that decision is still left to the developer and may vary, as illustrated in your example. However, once developers have declared an API as unsafe, its safety requirements should be clearly provided, and abstracted with tags (as proposed in this proposal).

8

I'm afraid that you misunderstand what I said. I'm not saying that this proposal can decide which API should be marked as unsafe. Instead, in the second approach, which marks clear as unsafe, the safety requirement could not be abstracted to tag proposed in this post.

9

Note that that would be unsound anyway, without using something like ghostcell for the ManagerIndex, since I could get a ManagerIndex from a different instance and pass it in when it's out of bounds.

But more generally, as I understand the proposal the point is not that the tooling needs to understand the definition of the tags, just that it can do a prolog-style proof search that the discharges match the preconds.

So you could have

#[safety::precond::IndexesNoLongerUsed(self)]
pub fn clear(&mut self) { ... }

and then correspondingly a

#[safety::discharges::IndexesNoLongerUsed(foo)] 
unsafe {
    foo.clear()
}

later.

(Obviously for well-known things the tooling could help more, or it could integrate with things like kani to help prove that they're true, but I would expect this to accept arbitrary properties like this just fine because people will want precond::IsRfc2324Formatted(x) or whatever too that the tooling can't know all of them.)

10

Yes you are right. We can add this to the safety requirement of clear, or just control the constructor of Manager to make it only be constructed once in a program. Anyway, we can add all safety requirements just to clear and make the get_foo_mut safe, which is all I want to say.

Yes I also think so. The tagging system should accept custom tags for this, which can then become safety::precond::ShouldSatisfySafetySectionInDoc(self) and safety::discharges::HaveSatisfiedSafetySectionInDoc(foo) :grinning_face_with_smiling_eyes:

11

If you don't want to use it, that's spelled #![allow(missing_safety_properties)].

12

I don't mean I don't want to use it. Safety contract is crucial to the safety of the whole rust system. In my understanding, by saying "verifying a system written by Rust", the most important part is to verify that the safety contract is met. If a system is verified, it can then be applied to key infrastructures such as payment. However, if using such ShouldSatisfySafetySectionInDoc tags, the verification is just fake. Without breaking the safety contract down to such primitives, whether such safety contract is met is determined by human instead of machine.

13

As a co-initiator of this proposal, I think that's a great suggestion, and I really like it. In fact, our current prototype already supports a CustomProperty tag, allowing users to define new properties via parameters, e.g., [safety::precond::CustomProperty(ShouldSatisfySafetySectionInDoc)] . To make this more user-friendly, we should explore native support for custom tags, such as your suggested syntax: [safety::precond::ShouldSatisfySafetySectionInDoc(self)] .

14

We support that.

The atomicity of discharge depends on the atomicity of property definition. So we don't have partial discharging.

If a safety requirement is cut into pieces, define small custom properties for each of them. And discharge some of these properties in a place, and the rest in other places.

We're considering call orders in SP (safety property):

unsafe fn f1() {}

---
#[safety::precond::priori(f1)]
unsafe { call() }
15

Yay. I'm aware of that.

And our work tag-std was listed in RustWeek's meeting note Function contracts and type invariants specification.

16

Yeah, that's perfectly one of the concerns on discharging a SP.

  • Implicit dependence on unsafe behavior: Developers may unknowingly change code that other safety assumptions rely on. For instance, the comment "the deque effectively forgot the element" depends on the behavior of Guard's Drop implementation. If try_fold::Guard::drop changes, developers must check whether the associated safety comments still hold. (This RFC does not address this problem, but see Entity Reference System for our thought.)
17

TBH, I'd just assumed they were all custom. I'd figured it was just a prolog-like thing that handled the α-renaming to match stuff up but never needed an actual definition of the properties to check. (Where the actual definitions of things would be more up to one of the proof tools that needs to do way more work of looking at the actual code, not just driving some lints via annotations.)

18

We're trying to support that. From our proposal:

Dynamic safety tag

The reason to have dynamically generated propeties is that we are unable to write an attribute library that can meet all unsafe code.

Low-level crates probably requires their own safety propeties more than libstd defines.

The core idea is a project-aware configuration file, in toml or json format, mapping property name, arguments, description (including string interpolation) and possible other verification macros such as kani. When safety-macro is being compiled, its build.rs will read the project mapping, and auto generate macros. (Suppose we don't have reflection and comptime any time soon.)

We're trying to experiment on this though, as Asterinas OS wants this. Feel free to drop by tag-std#26.

Technically, registering a tool attribute like safety is enough for any path under tool namespace like safety::any_thing::and_everything. But we want to support #[doc] and #[kani] macros as well, therefore a proc-macro crate is a must to add these macros in AST.

19

It depends on the FFI unsafe fn requirements. Your unsafe code contains CStr::from_ptr whose safety properties can be written as

#[safety::precond::ValidCStr(ptr, _)]
#[safety::precond::ValidPtr(ptr, i8, _)]
#[safety::precond::NonNull(ptr)]
#[safety::precond::ValidNum(compute_nul_pos(ptr), 0..=isize::MAX)]
#[safety::hazard::Alias(ptr, ret)]
pub const unsafe fn from_ptr<'a>(ptr: *const i8) -> &'a CStr { ... }

So to discharge them, you may write

unsafe {
    use shim::{UAPIStruct, STRUCTS};
    let mut map = HashMap::new();
    for UAPIStruct { name, align, size, fields, } in &STRUCTS
    {
        #[safety::discharges::ValidCStr(*name, _)]
        #[safety::discharges::ValidPtr(*name, u8, _)]
        #[safety::discharges::NonNull(*name)]
        #[safety::discharges::ValidNum(compute_nul_pos(*name), 0..=isize::MAX)]
        #[safety::discharges::Alias(*name, name)]
        let name = CStr::from_ptr(*name);

        let name = name.to_str().expect("struct tag name not valid UTF-8");
        let mut rfields = Vec::new();
        for i in 0.. {
            #[safety::discharges::ValidPtr(field_ptr, FieldSpec, 1)]
            #[safety::discharges::Aligned(field_ptr, FieldSpec)]
            #[safety::discharges::Init(field_ptr, FieldSpec, 1)]
            #[safety::discharges::NotOwned(field_ptr)]
            #[safety::discharges::Alias(field_ptr, fields)]
            let field_ptr = fields.offset(i);
            let field = field_ptr.read();

            if field.name.is_null() {
                break;
            }

            #[safety::discharges::ValidCStr(field.name, _)]
            #[safety::discharges::ValidPtr(field.name, u8, _)]
            #[safety::discharges::NonNull(field.name)]
            #[safety::discharges::ValidNum(compute_nul_pos(field.name), 0..=isize::MAX)]
            #[safety::discharges::Alias(field.name, fname)]
            let fname = CStr::from_ptr(field.name);
            let fname = fname.to_str().expect("field name not valid UTF-8");
            rfields.push(Field {
                name: fname,
                size: field.size,
                offset: field.offset,
            });
        }
        map.insert(name, Struct { size, align, fields: rfields })
    }
    map
}

I admit it's lengthy, but that's what has to be considered on each unsafe call.

Note ValidPtr(ptr, T, len) means Size(T, 0) || (!Size(T,0) && Deref(p, T, len) ), and Deref means Allocated(p, T, len, *) && InBound(p, T, len) from our spec primitive-sp.

3 Likes
20

Is there a reason why #[safety::precond::ValidCStr(ptr, _)] does not imply the others?

As a sidenote, I think a lot of the repetition comes from repeating the #[safety::discharges:: part. Couldn't the syntax be made so that safety::discharges is the macro and ValidCStr(*name, _), ValidPtr(*name, u8, _) etc etc are all parameters of the same macro?

2 Likes