RFC: Safe because I said so

[Havvy]

Rendered

[jonas-schievink]

It might make sense to experiment with something like this out of tree, comparable to the launch-code plugin

[est31]

checked*

[Havvy]

I should probably remove any instances of "I".

[killercup]

I think you lost a

` lint.

[burdges]

Nice idea! It'll be used more if #[safe()] had sugar like // SAFE, //$, //SAFE//, etc. similar to /// for #[doc()] though. It'll slightly easier for people using stable to adopt a //... notation early too, right?

[bjorn3]

Please also with cryptographic signatures like launch-code.

[ssokolow]

@bjorn3

I'd only consider that acceptable if they were optional. Since I only use Rust for hobby projects, all I need is to have access to an unexplained_unsafe lint for simple annotations of some kind and requiring anything more would risk making it too much work to deal with.

[tanriol]

Maybe not create new attributes at all, but just lint against an unsafe block that has no doc comment (stabilizing them on unsafe block expressions if needed)?

[ssokolow]

"no doc comment" isn't enough because it could be silenced completely accidentally. (ie. By something which explains why I chose that algorithm, rather than why I think it's safe.)

It'd have to be something that's clearly intentional, like SAFE: Explanation here

[burdges]

@bjorn3 There is no need for special signature tooling here since you can verify signatures on all commits containing the word unsafe using git verify-commit `git blame keys.rs | grep unsafe | cut -c1-8` so just add whatever the sugar for this winds up being.

[torkleyy]

Is there really a need for this? It's another annotation in the language and beginners will have to learn another thing (yes it is somehow obvious what safe means but I think the language shouldn't be overloaded with too many keywords).

As the rendered document states, this will lead to many placeholders. I don't think it will really prevent "unsafe unsafes".

If a use of unsafe isn't valid in an obvious way, I'd go for the comment approach.

For the as_mut_slice: This probably would have been prevented if there was an explixit pass_something_immutable_mutably thingy.

[scottmcm]

This should probably apply to unsafe impl, in addition to unsafe blocks.

I feel like this would quickly result is some just-enough-to-pass-CR strings getting copy-pasted everywhere. Like #[safe(justification="Guaranteed by struct invariants")] or something. Especially if multiline-string-literal-in-attribute feels just weird enough to discourage a long text block.

Is the block itself the right scope for a justification? Something like "the first length elements are constructed, but space is allocated for the capacity ones" would probably be a justification for many things in different impl Vec methods.

Also, if every block needs an attribute, that's implicit encouragement to merge unsafe blocks rather than keep them separate and localized. And the extra characters would make a targeted unsafe in a closure, for example, noisy enough that it'd look ugly, so it might just get widened.

Would it be worth letting people say what they're justifying? Say #[safe(function="drop_in_place", justification="Decremented `len` earlier, so won't double-drop even on panic")].

It'd be nice to see some less-"silly" examples, since the current one is just as.

Would this have actually solved the as_mut_slice problem? If the problem was that as_slice was copy-pasted and one of the muts missed, as seems plausible, then the #[safe] would also have been copied. And a copied justification like "Safe because Vec guarantees on construction that len elements are valid, and the inferred lifetime matching self is correct." would have been correct, so not changing it wouldn't be surprising.

Overall, I think I'm 👎: This still depends on careful code review, and at that point it doesn't need to be an attribute.

[ssokolow]

@scottmcm

A lot of your arguments about how it could be circumvented by undisciplined coders could apply equally well to the missing-docs lint and I see this as serving a similar role.

The distinction being that missing-docs is insufficient for this purpose since it can't understand that the following is purely about justifying the use of the fallible access() system call but says nothing about the use of the unsafe block it's wrapped in:

/// API suitable for a lightweight "fail early" check for whether a target
/// directory is writable without worry that a fancy filesystem may be
/// configured to allow write but deny deletion for the resulting test file.
/// (It's been seen in the wild)
///
/// Uses a name which helps to drive home the security hazard in access()
/// abuse and hide the mode flag behind an abstraction so the user can't
/// mess up unsafe{} (eg. On my system, "/" erroneously returns success)

At the very least, I'd argue that such a lint belongs in clippy alongside blacklisted_name and missing_docs_in_private_items which could also prompt un-disciplined coders to tweak their code just enough to fool the check.

TL;DR: Not everything in Rust needs to be held up to the standard the borrow checker enforces on the code. Just because something requires a certain degree of cooperation from the developer doesn't disqualify it from being useful enough to include.

P.S. I believe it was an instance of Andrew File System that I'm remembering being configured to allow creation but not deletion in a production setting.

[nikomatsakis]

@rfcbot fcp postpone

I am strongly in favor of giving more semantic content to our unsafe blocks. However, I'm not in favor of adding anything to the compiler right now to do that -- I'd rather we experiment out of tree. I am aware of at least one such experiment (launch-code, previously mentioned), and I know of a few people pursuing various verification techniques in academia as well. I have my own pet theories for what'd make a nice, simple tool. To throw into the mix, I think that we may want to expand our model of "unsafe blocks" and so forth as part of the unsafe code guidelines work -- so basically there are enough ingredients swirling around that I think it's too early to bless one approach as the winner. Therefore, I move to postpone this RFC.

[rfcbot]

Team member @nikomatsakis has proposed to postpone this. The next step is review by the rest of the tagged teams:

• @aturon
• @eddyb
• @nikomatsakis
• @nrc
• @pnkfelix
• @withoutboats

No concerns currently listed.

Once these reviewers reach consensus, this will enter its final comment period. If you spot a major issue that hasn't been raised at any point in this process, please speak up!

See this document for info about what commands tagged team members can give me.

[Havvy]

cough cough @nrc and @pnkfelix cough cough

Niko thinks more about this than I do, so I'll defer to him if he thinks there's good reasons to wait.

[jessstrap]

Postponing sounds prudent to me, though I do have one new ingredient to add to the general idea soup that might make an initial implementation palatable:
The annotation mechanism should extensiblely support multiple different justifications of different types in one notation instance.

Example (assuming the annotation is an attribute):

#[lint_safe_because(
    error(missing("natural-en-us")),
    warn(missing("launch-code))"
)]

#[config_attr(nightly, lint_safe_because(error(invalid("launch-code"))))]

fn safe_fn() {
    #[safe_because(
        justification("natural-en-us",
            "This block is safe because......"),
        justification("natural-es-es",
            "Esta bloque es segura porque"),
        justification("audited-launch-code",
            "⠐⡛⢾⣯⢓⢵⢖⡆⣈⠇⠸⣼⢁⢦⢰⢷⡫⢙⠻⠺⢗⢻⣷⠋⣸⡐⣂⡜⠇⡍⢁⢗⢜⠢⡢⣵⠩⠲⡈⢈⢂⡑⣷⣩⢲⢖⢃⡓⠄⣴⠩⡹⡸⠥⢱⢭⡼⠡⣻⡥⢜⢔⡌⠅"),
        justification("proof-coq",
            "<some coq source here.>")
    )]
    unsafe {
        //...
    }
}

#[safe_because(
    justification("natural-en-us",
        "This function is safe if callers can prove...."),
    justification("natural-es-es",
        "Esta función es segura si los usuarios pueden probar"),
    justification("audited-launch-code",
        "⠐⡛⢾⣯⢓⢵⢖⡆⣈⠇⠸⣼⢁⢦⢰⢷⡫⢙⠻⠺⢗⢻⣷⠋⣸⡐⣂⡜⠇⡍⢁⢗⢜⠢⡢⣵⠩⠲⡈⢈⢂⡑⣷⣩⢲⢖⢃⡓⠄⣴⠩⡹⡸⠥⢱⢭⡼⠡⣻⡥⢜⢔⡌⠅"),
    justification("proof-coq",
        "<some coq source here.>")
)]
unsafe fn unsafe_fn(i32:foo) {
    //...
}

Validators for justification types would be either external tools, lints (nightly/unstable only) or built into the compiler. Experimental validators could be used to experiment with and validate unsafe guidelines. As unsafe guidelines solidify and formal verification of rust code matures, further rfcs would propose stabilising individual validators.

[bjorn3]

@jessstrap that can already be done with compiler plugins.

[jessstrap]

@bjorn3 Yes, but compiler plugins are only on unstable. To clarify:

I am proposing a stable safe_because(justification("<language_identifier>", "<justification>")) attribute and a stable lint_safe_because([error|warn](missing("<language_identifier>"))) attribute and lint.
The lint_safe_because([error|warn](invalid("<language_identifier>"))) attribute and lint would be unstable until some validator was stabilized.
In the mean time tooling could integrate with the stable attributes and the unstable attributes could be used for experimentation.

[scottmcm]

@ssokolow I like missing_docs because it's not missing_docs_in_private_items. I like the tradeoff that it whispers: "You said it's public; so you know you need to document it. But if you really think it doesn't need documentation, I'll let you skip it if you can find a way to make it private..." (I've seen good devs change their habits to refactor less and copy-paste more if even a private helper method needs a full doc comment.)

There's definitely a place for more help writing and reviewing unsafe code. But I think it needs more than a single opaque string. Maybe, for example, an unsafe method could document its unchecked preconditions in such a way that exactly that set would need to be justified by the caller. Then when writing the code the compiler will prompt you about each thing you need to consider to call the unsafe, and in a bad copy-paste-edit would tell you that there's something extra. (Kinda like lints.) That's not unlike what the example justification in the RFC does--list the things that need to be considered and explain them--just in a way that the compiler can help. I agree that help doesn't need to be borrowck-level-perfect (though maybe with proof-coq it could be), but it ought to at least be resilient to reasonable things done by disciplined coders. As I said before, I don't think a string in an attribute would have caught the as_mut_slice accident.

[ssokolow]

@scottmcm And that's a detail that varies from person to person.

• I enable missing_docs_in_private_items in my projects.
• I never use worthless doc comments to silence things (though, on rare occasions, I may use #[allow(missing_docs_in_private_items)] since it's easy to have a git hook that prevents code containing that from getting pushed.)
• It really grates on me that there's no ready-made Cargo.toml key or command-line flag to tell cargo doc that I want an internals reference, including all private members and to document --bin crates without the need to include a token main.rs + lib.rs separation. (Seriously. What "statically-typed shell script" needs a main.rs + lib.rs separation?)

[rfcbot]

🔔 This is now entering its final comment period, as per the review above. 🔔

[rfcbot]

🔔 This is now entering its final comment period, as per the review above. 🔔

[rfcbot]

The final comment period is now complete.

[aturon]

Closing as postponed, as originally proposed.