Effect system for panics and transitive unsafe

[Ekleog]

This is a follow-up from Rust beginner notes & questions

The idea is basically to add an effect system to Rust, for handling things that people may want to consider like unsafe in some circumstances, here panics and transitive unsafe (that is, unsafe hidden behind an unsafe block), in the aim of:

• For panics, having a system that can provably not panic (thus ensuring that the system cannot have unexpected code paths, basically like a method that cannot throw in Java)
• For transitive unsafe, reducing dependency on dependencies for security, as an ill-written unsafe block may easily turn out to be a serious vulnerability. It also helps in cases like Tock OS, where ensuring safety of capsules is essential for the security (even though the absence of any rustc bug allowing to trigger unsafe behavior without the unsafe keyword is debatable, let's not debate this right here, that's just an example use case )

Relevant posts from the main thread:

Rust beginner notes & questions

I think this is the crux of it. C++ is a machine gun with no safety that people wave around in a terrifying fashion. Rust to me feels like a machine gun with a safety installed, but I see a bunch of people walking around with the safety off. I see too many uses of panic! and unsafe, and not enough mechanical means to ensure safety. There's no equivalent of the grumpy sergeant taking everybody's clips away from them when they return to base. Nobody likes the sergeant, he's no fun, but it just t…

Rust beginner notes & questions

But panicking isn't unsafe in the machine-gun sense. You may be right that unsafe is overused.

Rust beginner notes & questions

I think it's critical not to conflate those two things. It's absolutely essentially that unsafe usage be thought through carefully. But liberal panic!ing should be encouraged, for conditions not yet handled, so long as it's not ignored by catch_panic. Outside of rust, I've seen use of a "crash if this condition isn't true" macro substantially increase the reliability of a product. It lets to more failures in test, but that's good: you get a nice crash dump showing the situation you hit, and…

Rust beginner notes & questions

It's absolutely essentially that unsafe usage be thought through carefully. But liberal panic!ing should be encouraged, for conditions not yet handled, so long as it's not ignored by catch_panic. I wish to respectfully disagree. For some use cases (example in mind: embedded systems, a target Rust explicitly supports), a panic! may mean deaths (OK so now I'm hyperboling too). I've seriously thought of trying to do a “rust without panic,” but it turns out that's really hard to do, given …

Rust beginner notes & questions

"safety" in Rust means "memory safety". panic is memory safe. Code that is memory safe can still have other kinds of bugs.

Rust beginner notes & questions

"safety" in Rust means "memory safety". panic is memory safe. Code that is memory safe can still have other kinds of bugs. Indeed, I'm not arguing @peter_bertok used the right Rust-y jargon, just that there are real-world cases for wanting code that could provably not panic

Rust beginner notes & questions

E.g., the computerized steering and braking systems in your autonomous car, the engine controls on a commercial airline that prevents turbine overspeed that can cause turbine blades to detach and slice through the fuselage.

In addition, I have had a small discussion with @bgeron with the following relevant content:

@Ekleog

As for panics, well… I prefer Rust to Haskell, but panics and especially their un-avoidability are still a thing that bother me profoundly in Rust, and I’d love it if we could get what I have heard is possible with effect systems à la F* / Ada (which I haven’t used yet), a way to limit panic! usage to some parts of the code much like unsafe. (and ideally it’d be a fully-generic effect system so that it could also handle insecure and similar effects, that are currently handled with hacks).

@bgeron

I prefer Rust to Haskell, but panics and especially their un-avoidability are still a thing that bother me profoundly in Rust

Do you feel it’s better in Haskell? In my view, undefined or missing branches from a case..of are essentially the same as panics.

effect systems

I’m actually currently doing a PhD that involves effect systems. My impression is that an effect system cannot be perfect; there are always either problematic things it doesn’t catch, or good things it doesn’t allow.

Then there is the theorem proving approach (Coq/Agda/Idris/F*): it is sometimes very very hard to convince the computer that something is okay; this is the kind of thing that requires you to give pages and pages of proof for small snippets of code. (Though in F*, you only have to give these proofs sometimes instead of always.)

In my understanding, Ada isn’t that special; essentially it just has language support for putting assertions everywhere and maybe it makes them more efficient. But the assertions still happen at runtime, so your program may crash.

@Ekleog

[snip] I guess what I want is more knowledge
over exactly what unsafe parts are being used (and actually a
transitively_unsafe would make sense to me, so that I could enforce
that a function transitively never uses unsafe , even inside an
unsafe block)

Do you feel it’s better in Haskell? In my view, undefined or missing
branches from a case..of are essentially the same as panics.

Honestly, I don’t think Haskell (or any other language that I practiced
apart from – ironically – C, and Java where IIRC the exceptions must
be described) gets a solution to this problem better than Rust.

But that’s still something that bothers me with Rust, especially given
it’s trying to get a foothold in the embedded world, where the absence
of exceptions is something highly important.

I’m actually currently doing a PhD that involves effect systems. My
impression is that an effect system cannot be perfect; there are always
either problematic things it doesn’t catch, or good things it doesn’t allow.

Oh? That’s a topic into which I planned to get more, but still haven’t
found time for it. So I guess for Rust the effect system would better
allow things it maybe shouldn’t… but that’s still better than only
catching unsafe ? !

Then there is the theorem proving approach […]

Well, that’d be ideal for proving snippets of unsafe code, but I don’t
think Rust is ready yet for integrating a theorem prover into its
compiler, and it’ll live for quite some time into the tooling. Ideally
it’d end up with a way to transitively allow only proven unsafe code and
not normal unsafe code, but… well…

In my understanding, Ada isn’t that special […]

I was maybe thinking of Ada/SPARK? Or maybe that’s just a wrong
recollection due to name similarity with Agda, I can’t remember, sorry!

@bgeron

actually a
transitively_unsafe would make sense to me, so that I could enforce
that a function transitively never uses unsafe , even inside an
unsafe block

Do you mean “even across function calls”?

I think this was discussed briefly somewhere: it could be very useful in some situation but I don’t expect it to become a common thing. If you want to do this across crate boundaries, then suddenly the API of a crate must include which functions are transitively_safe , and that’s a promise that those functions will also stay transitively_safe in future versions. I think a lot of crate authors would hesitate to make that promise for the future. That said, it might well spawn a whole ecosystem around transitively_safe crates.

But that’s still something that bothers me with Rust, especially given
it’s trying to get a foothold in the embedded world, where the absence
of exceptions is something highly important.

I expect that something like Coverity is promising for embedded Rust. It won’t catch all exceptions that will actually happen in real life, but perhaps something like 90%-95%? Embedded software seems simple enough for this to work well. On the other hand, there’s a lot of possibility for panics in Rust. Even stuff like x+1 can cause a panic when the result doesn’t fit in the same type.

C++ has fewer exceptions, but in C++ an integer overflow would typically wrap around (if you use the right compiler options). Perhaps the system doesn’t crash, but you might well get bugs further down the program. I don’t know which option is better.

I was maybe thinking of Ada/SPARK?

Cool! I wasn’t aware of Ada/SPARK. It seems to use essentially the same approach as F*, where the computer does most proofs and you do the remaining proofs yourself.

@Ekleog

actually a
transitively_unsafe would make sense to me, so that I could enforce
that a function transitively never uses unsafe , even inside an
unsafe block

Do you mean “even across function calls”?

I think this was discussed briefly somewhere: it could be very useful
in some situation but I don’t expect it to become a common thing. If you
want to do this across crate boundaries, then suddenly the API of a
crate must include which functions are transitively_safe , and that’s a
promise that those functions will also stay transitively_safe in
future versions. I think a lot of crate authors would hesitate to make
that promise for the future. That said, it might well spawn a whole
ecosystem around transitively_safe crates.

Indeed, I’m thinking of this even across function calls and crates. It’s
a relatively restricted use case indeed. For instance, IIRC Tock OS
stated last year (don’t know now) that it could run untrusted programs
that didn’t use unsafe as part of the OS by wrapping them in a
capsule. Having a transitive_unsafe would make this sort of features
less braindead (well, there’s still rust compiler bugs, and up until now
rustc hasn’t appeared to deem a unsafe-safe-code soundness issues to be
security vulnerabilities).

Actually, upon thinking more about it, transitively_safe would not
make much sense, as soon as there’s a Box there’s going to be some
transitive unsafety… so maybe something based on “transitively safe
apart from code in crates A, B and C”? That’s even harder to encode at
the crate boundary, though.

But that’s still something that bothers me with Rust, especially given
it’s trying to get a foothold in the embedded world, where the absence
of exceptions is something highly important.

I expect that something like Coverity is promising for embedded Rust.
It won’t catch all exceptions that will actually happen in real life,
but perhaps something like 90%-95%? Embedded software seems simple
enough for this to work well. On the other hand, there’s a lot of
possibility for panics in Rust. Even stuff like x+1 can cause a panic
when the result doesn’t fit in the same type.

Yeah, that’s one of the points I was thinking of when thinking panics
are deeply integrated with the language, and it’s really hard to
actually be 100% sure there can be no panics.

C++ has fewer exceptions, but in C++ an integer overflow would
typically wrap around (if you use the right compiler options). Perhaps
the system doesn’t crash, but you might well get bugs further down the
program. I don’t know which option is better.

I don’t think C++ gets the exception story much better than Rust. Java
is the only language I practice that gets it almost right (IIRC), by
forcing exception specification in the prototype of methods.

C also gets it right in a way: it just doesn’t have exceptions. That’s a
good way to make sure there can be no unexpected exceptions. Well, the
other issues of the language do balance this advantage, though. But I
think that’s part of the reason why C is actually almost the only
language used in embedded development ! (this, the possibility to write
code without any dynamic allocation, and Frama-C, if I had to guess)

So, what do you think about introducing an effect system for Rust? I'm sure there is already literature somewhere, but sometimes it's maybe better to start a debate from fresh, as the things one want may change over time? (between insecure, no_panic and no_transitive_unsafe_except_from_crates(A, B, C), I guess there's likely enough to think about a full-fledged effect system without too much over-engineering everything now )

[kornel]

I'm against further demonizing unsafe.

• It has a very very narrow scope as a security feature, because "safe" Rust can still execute arbitrary code (e.g. via Command, fs::write, or #[no_mangle] hacks). There's no sandbox, and no security in the language, so it could be giving false sense of security.

• Wholesale bans on it are a strong disincentive to use unsafe in cases where it's entirely safe and necessary. This will force library authors to write weird and inefficient code in order to stay relevant to both trusting and distrusting fragments of the Rust userbase.

• Ability to individually add exceptions for crates trusted with use of unsafe is both ineffective and collectively a massive waste of time for the Rust userbase. Rust projects use use lots of crates, so you can't expect users to honestly review every crate, so most likely they'll just whitelist based on a hunch. Even if users reviewed crates, doing so individually by every user is a huge duplication of effort.

So the overall problem "is this code bad?", "can I trust this author/crate?" is deeper than just presence of one keyword. I think it could be solved better, with fewer side effects, and with less overall effort required from Rust users by having shared crate reviews.

[kornel]

The effect system for panic seems useful though. There are situations around FFI where you're not supposed to have panics, so it'd be nice to have a static guarantee about that.

Could it be possible to also statically ensure that certain code runs on the "main" thread? This is important for most GUI frameworks, e.g. Cocoa breaks badly when you accidentally call some callback from non-main thread.

[matklad]

@kornel

Could it be possible to also statically ensure that certain code runs on the “main” thread? This is important for most GUI frameworks, e.g. Cocoa breaks badly when you accidentally call some callback from non-main thread.

You can use a non-sync non-send zero sized "main thread proof" object for that.

[dtolnay]

I have been using the linker to enforce a basic effect system for panics: see no-panic.

[Ekleog]

@kornel

I’m against further demonizing unsafe .

I think I poorly explained my (personal) problem with unsafe. It's (for me) not about security that could be worked around with Command, fs::write or #[no_mangle]. For me, it's mostly about “OK, I'd rather assume crate authors know nothing about developing unsafe code, and be better safe than sorry”. And then, if the transitive-unsafe checker raises errors, to either change my dependency, or to actually go check the unsafe usage looks correct and whitelist the dependency.

@kornel

Could it be possible to also statically ensure that certain code runs on the “main” thread? This is important for most GUI frameworks, e.g. Cocoa breaks badly when you accidentally call some callback from non-main thread.

I think it'd be possible to add a single_threaded effect, though I'm no expert on the topic. Making sure the code runs on the “main” thread would be much harder imo, as that's not a local property, but a global one.

That said, for this use case, maybe @matklad's solution is just easier

[Ekleog]

Also, an idea coming to my mind: are effects not just like marker traits? An unsafe function is a function not implementing the Safe auto-derived unsafe trait. An insecure function is a function not implementing the Secure auto-derived “unsafe” (actually insecure) trait. Et caetera. And it'd be possible to implement said unsafe / insecure trait by using an unsafe / insecure block.

I wonder if we could just fit effects through traits, for an easier answer to “how does this interact with the type system?”

@bgeron (sorry if you didn't want to continue this discussion): what do you think about this?

[bgeron]

In a way, effect systems are very much like marker traits in that they're both deducted statically from the source code.

But one is a property on types and the other one is a property on code They're really not the same. There are ways to bring them together (e.g. "effect systems" using monads) but it's not straight, you have to use encodings.

It's probably also better to keep an effect system separate from traits because separately, the error messages will probably be better.

[gbutler69]

@Ekleog

basically like a method that cannot throw in Java

There is no such animal in Java. You can have methods that do not throw checked exceptions, but, any method can throw an unchecked exception (the nearest equivalent of panic) at any time.

[gbutler69]

@Ekleog

For transitive unsafe , reducing dependency on dependencies for security, as an ill-written unsafe block may easily turn out to be a serious vulnerability.

Nearly everything will be transitively unsafe. At the lowest levels, many/most of the fundamental building blocks wrap unsafe code in a safe abstraction. I don't think considering things "transitively unsafe" is a useful concept.

[gbutler69]

@Ekleog

just that there are real-world cases for wanting code that could provably not panic

That sounds like an impossibility. Panic will be needed for many things that should never happen (like a stray cosmic ray flipping a bit of memory to an invalid state) so that the program may not continue with program execution and exhibit UB.

[Ekleog]

@gbutler69

There is no such animal in Java. You can have methods that do not throw checked exceptions, but, any method can throw an unchecked exception (the nearest equivalent of panic) at any time.

Oh I thought that was the case in C++ and Java handled things correctly. Well, I guess I'm now hoping for Rust to be the first language I know to support unwrapping in a decent way that is not just not having it.

@gbutler69

Nearly everything will be transitively unsafe. At the lowest levels, many/most of the fundamental building blocks wrap unsafe code in a safe abstraction. I don’t think considering things “transitively unsafe” is a useful concept.

This is exactly why I wrote no_transitive_unsafe_except_from_crates(A, B, C) in the topmost post Though I guess I should have put it above the quotations, not under.

@gbutler69

That sounds like an impossibility. Panic will be needed for many things that should never happen (like a stray cosmic ray flipping a bit of memory to an invalid state) so that the program may not continue with program execution and exhibit UB.

A stray cosmic ray flipping a bit of memory to an invalid state will most likely not cause a panic, but just cause UB, in current Rust. Also, when doing safety-critical applications, you use ECC RAM, redundant reads, etc. Also, a bit flip can potentially be recovered from.

I know rustc isn't quite there yet, but already having a way to say “OK, there is no occurrence of panic! anywhere in the call graph of this function” would be a pretty consequent step if the right direction (actually, with transitive_unsafe and integration with a theorem prover, that's the most important step I can think of, the other ones are at the compiler level and independent of the language)