Hacker News Reader

Comment by staticassertion | Hacker News Reader

One thing I've realized with Rust is that its guarantees are a moving target. Today we can guarantee (barring compiler errors) memory safety in safe rust, but not unsafe rust.

But that story is improving. For one thing, we have people working to build safe abstractions for more unsafe use cases, at zero cost. We also have people improving fuzzing, and in theory safe rust code grows at a much faster rate than unsafe rust code, so fuzzing is far more tractable. We have people working on proving more about rust code, even when unsafe is around.

I'm quite excited to see how far Rust is able to go, I don't believe the state today is the end at all.

View on HN

While some patterns that call for unsafe today might be eliminated in whole or part, code that violates the ownership and borrowing rules will have to remain unsafe. I think fuzzing is not guaranteed to reach all unsafe code paths, nor provide full test coverage. Ideally, you want a) some sort of formal proof that the unsafe code cannot violate memory safety, b) 100% branch coverage for unsafe code, or c) both (because profilers and proofs can be wrong too :)

edit: grammar.

Why does code violating the rules have to stay unsafe? Haven't the rules been improved before? Why won't they be improved again?

What I really want is an integration of automated proof checking with unsafe code, allowing completely safe rust programs.

Additionally, this could be extended to safe code to allow removing overhead from safety in things like bounds checks and Rc.

This requires a formal semantics for Unsafe Rust. It's a hard problem, albeit one that's being worked on.

I'm aware that however it's done it'll be hard.

Does it really require formal semantics for unsafe rust though? I'm not familiar enough with rust to give an example, but if you imagine there's the unsafe rust level and beneath that the "machine code" (not actually machine code, just at the abstraction level equivalent to it) you should be able to hand write what the rust code is doing, without requiring the compiler to construct the machine level operations.

With a formal semantics the proof checker just checks that the written proof (at rust level) matches with the rust code, but requires as you said an understanding of how unsafe rust interacts with the proof, whereas with a proof written at machine level, you don't need to understand the rust semantics, you just need to translate the rust to machine level and then check the proof there.

Perhaps the machine level could be some layer in llvm? I'm only a little familiar with compilers, and hardly at all with more complicated compiler theory, but this seems reasonable to me.

> With a proof written at machine level, you don't need to understand the rust semantics, you just need to translate the rust to machine level and then check the proof there.

This approach would only be able to verify a particular compilation result as safe. If you want to verify that it will always be safe, you need to be comparing against the behavior of future compilers, which requires some kind of contract about their behavior. “Formal semantics” is the technical term for that contract.

The problem is that the unsafe-safe boundary needs to be specified. Unsafe code often relies on invariants ensured due to safe rust's checks. Also, there are properties that unsafe code has to satisfy which are special to rust, for example involving rules around special traits like `Drop`. So even if the unsafe code itself could be proven to have no memory corruptions, if it does not satisfy these invariants, it could lead to wrong behaviour in other parts of the program.

Any references?

Amen to that. Integrated formal systems giving the spec working with the programming language on the implementation side is the holy grail.

Unsafe Rust can be (and has been) formally verified to satisfy its Rust type, meaning calling it from safe code can't violate memory unsafety. We don't need to trust manual inspection.

IMHO, this is going a bit too far. Some parts of unsafe Rust have had a model produced that can check some of the invariants required for safe Rust. For example, in my understanding, traits were not modeled at all. Still very promising work, but don't want to overstate it either!

I never said all unsafe Rust code was verified, but we certainly have verified the parts required for stuff like Arc and RwLock beyond reasonable doubt.

How, when they rely on semantics that are not fully locked down? Are you referring to something other than the Rust Belt work?

You mean, if they were used with dynamic trait objects or unsized types or something? I suppose theoretically there could be some issue, since they aren't modeled yet, but in that case it would almost certainly be a (much more worrisome) issue with the safe part of Rust itself, not the specific unsafe code involved in those types. I don't think any proposal for how to model trait objects, for example, would change the model of how semantic types are defined, it would involve adding new semantic types and new theorems about them.

Cool, then yes, we’re on the same page here, I am just extremely cautious when talking about this. It is true that that stuff would indicate a larger problem, but it’s not like we haven’t discovered unexpected larger problems in the past.

Today we can guarantee (barring compiler errors) memory safety in safe rust, but not unsafe rust.

Not quite. An unsafe function can export its lack of safety to other code. If an unsafe function can be called with parameters which make it violate memory safety, it opens a hole in memory safety.

Calling an unsafe function can only be done inside an unsafe block.

I assume OP s point is that unsoundness or UB in an unsafe block is not contained in that block, but can taint safe code anywhere in the program. Which is true.

Yes, it's true, but that wasn't what Animats said. And even if that was Animats' point, it doesn't invalidate the GP. The key value proposition of Rust isn't that "you'll never have memory safety bugs," but rather, that if your unsafe code is correct and sound, then safe Rust will be free of memory safety bugs. The important bit is the implication that grants one the power to make that sort of reasoning. It's important precisely because it limits the places in your code that need to be audited.

This is indeed a very powerful property. However, I have a question: is it a regular practice to ensure that code marked unsafe is actually safe for whichever parameters it receives? Or could the safety of some unsafe code depend on the way its safe wrapper is called?

If you have an unsafe function---that is, a function that is unsafe to call---then it is common practice to document the precise preconditions that the caller must uphold in order to ensure safety. This may indeed include passing a correct parameter. For example, the preconditions of the slice method `get_unchecked` require the caller to verify that the index provided is in bounds, otherwise the behavior is UB.

If you have a safe function that uses unsafe internally, then all possible invocations of that function should be safe. If this isn't true, then we call those sorts of APIs unsound and they are strongly discouraged. David Tolnay wrote a great blog post about it: https://docs.rs/dtolnay/0.0.7/dtolnay/macro._03__soundness_b...

Than you for the details, that makes a lot of sense!

only if that block, or something in its "trusted set" (my term, for things in the same module that can access private members) is incorrect, though.

safety/unsafety in Rust is factorable, which is a key part of the reason Rust is useful at all.

Rest of your program blindly believes that the interface of your "trusted set" is safe because you owned that responsibility when you marked it unsafe.

If you have a memory safety bug in that interface, then you can taint the rest of the program's memory safety as well, correct?

Yes, that's the whole point though.

I think that is too strong. Consider this code:

    unsafe { libc::fork() };
    let v = vec![1];

This may hang or even crash (malloc in the child) but there's no sense in which the unsafe block is "incorrect." Some unsafe code has unavoidable implications for the entire program.

Indeed, some uses of unsafe aren't meaningfully factorable. File backed memory maps or shared memory with other processes are other important real world examples that are difficult or impossible to meaningfully factor in the context of a single process. But I still think that saying "safety in Rust is factorable" is accurate beyond a mere first approximation. Figuring out how to encapsulate unsafety is, in my experience, the essential creative aspect to using unsafe at all. Because if safety wasn't something you could encapsulate, then Rust really wouldn't be what it is. (I have spent many long hours thinking about how and to what extent the safety of file backed memory maps could be encapsulated. Which is to say, factoring safety is really the ultimate goal, even if certain things remain beyond that goal.)

I’m unsure what you’re responding to. As I understood it, the comment took issue with saying that you can make guarantees about safe Rust but not unsafe Rust because unsafe Rust is not verified in that way and opens the door to violating guarantees in your “safe” code if your bugs leak out.

That may be what you understood, but that's not what Animats said. See my reply above for more of an elaboration: https://news.ycombinator.com/item?id=24028359

Can you rephrase or restate your point? It's really hard to understand..

“Your comment doesn’t really make sense, https://news.ycombinator.com/item?id=24027224 “

I don't know the veracity of the claims but it's pretty crystal clear.

safe becomes unsafe really quickly

The function containing the unsafe block can be called from safe code. So unsafe functionality can be exported. Said unsafe functionality might not be safe for all possible inputs. That's a classic hole, as with APIs that can be exploited.

Then that's a "function containing an unsafe block," not an "unsafe function." In any case, this is still a misunderstanding of what staticassertion said. I elaborated more here: https://news.ycombinator.com/item?id=24028359

My bigger point here is that you're misunderstanding the advocated Rust value proposition. The value proposition isn't literally "Rust will forever and always eliminate all memory safety bugs in safe Rust." That's silly and no serious person with any credibility would double down on that claim.

They say can call though, so they are correct: if you can call then you are in an unsafe context.

Yes...? But they're responding to a point about safe Rust. See my other comment: https://news.ycombinator.com/item?id=24028359

But you can expose unsafe code with a safe API, right?

The point of the GP was that any safe code using this safe API could in fact be memory unsafe is there is a bug in the unsafe implementation.

Yes but it's easy to take this too far and conclude that e.g. Javascript is not memory safe because browsers are written in C++ and they have to interface with the kernel which is written in C. At some point you simply need to trust that the current implementation is correct and bug free. This is also a problem with formal verification. What verifies the verification?

Yes, of course you can. But that's not what Animats said. Animats specifically said "unsafe function," which means you need to use the unsafe annotation to call it. See my other reply for more elaboration: https://news.ycombinator.com/item?id=24028359

Yep. For example, it's easy to make intentional memory leak in Rust using safe API, which is unsafe. However, it's also easy to find such memory leak. Rust cannot stop you from doing weird things, when you want this, but it can help you to prevent, or quickly find, weird things, when you don't want them in your code.

"For example, it's easy to make intentional memory leak in Rust using safe API, which is unsafe."

In what way is leaking memory in rust unsafe?

It's a safe way to crash program by OOM killer. :-)

> However, it's also easy to find such memory leak.

How? By manually inspecting all code in the project + dependencies marked with "unsafe"? The approach doesn't scale past "hello world" level of complexity.

I don't code Rust, using C# for same purpose. I remember couple times I spend hours debugging weird crashes caused by stupid bugs in totally unrelated unsafe C# code.

It's much easier to find memory leaks or native memory corruptions in C++, than in unsafe subset of a memory safe language. C++ has lots of runtime support for that (especially in debug builds), and many great tools, both in the compilers and external ones. Unsafe C# has none of them.

You can also use those tools on Rust. It looks close enough that’s it’s fine. Valgrind, fuzzers, that stuff still works.

Simpler stuff like debug C heap, and checked iterators in C++ standard library, catch 95% of memory corruption issues in C++. These are enabled by default in debug builds, very often just pressing F5 in visual studio finds the buggy line of code in a matter of seconds.

Valgrind is Linux-only, I don’t have it. One Windows equivalent is memory profiler under Debug / Performance Profiler / Memory Usage in visual studio, Rust is not supported by visual studio. A cross-platform equivalent is Intel VTune Profiler, no support for Rust either.

I mean, if you’re talking about checked iterators... that’s checked in Rust too.

I am 100% Windows, but don’t triage these issues often enough to suggest tools; the unsafe code I write tends to be small and pretty obvious. (More like “write to this register” than “here’s a complex data structure.”)

> that’s checked in Rust too

In safe Rust. Safe C# is the same, it doesn’t even have raw pointers in the language unless compiling with /unsafe, and writing code in unsafe blocks.

> More like “write to this register” than “here’s a complex data structure.”

I sometimes write C++ DLLs precisely to implement these complex data structures. Modern CPUs have progressively worse proportion of RAM latency / compute speed. This means you need full control over memory layout of data on the performance critical paths of code, or it will be slow.

Also, many external APIs have incredibly complex unsafe structures. Here’s a piece of Linux kernel API I have recently consumed in C#: https://www.kernel.org/doc/html/v4.20/media/uapi/v4l/v4l2.ht... Way more complicated than writing registers.

They’re checked in unsafe too. You only skip those checks if you use a specific “do this index with no checks” function. Unsafe does not change the semantics of code, only gives you more options.

Yes, and many people write that kind of code in Rust too, and use tools to help them debug it. I’m just saying that it’s not an issue for the kinds of code I write, so I can’t personally recommend tooling. I know "use GDB" isn't a great response to a Windows user, even if it is what I end up personally doing.

Funny enough, I just booted up VS, and it's not perfect, but https://imgur.com/a/kHvPIEr

(It's true that I can't get the performance tools working though, but given I've used VS for all of 20 minutes... I'm also very interested to see if support happens native-ly, given how much interest there is for Rust inside of Microsoft right now.)

However you put it, tooling support is way, way better for C and C++ for obvious reasons.

Other critical bits for commercial development in many industries (certs, standards, third-party support, official bindings...) are also completely lacking.

That is not something against Rust, it is just what happens until things get popular enough.

Absolutely. All I’m saying is that it’s non-zero, not that it’s equivalent.

Memory leaks are not memory unsafe.

Lots of talk about formal methods, but I think the high order bit would be for unsafe code to use debug_assert! to check its preconditions.

Right now it doesn't, because of rather silly technical reasons regarding how libcore is built and tested.

Reply on news.ycombinator.com