11 year old unsoundness bugs found in Rust borrow checker

I can't tell if you are sarcastic, but in case you are not:

By Rice's theorem you cannot be sound and complete, i.e. accept all valid programs and reject all invalid ones. Most languages choose to be sound but not complete, i.e. reject all invalid programs but also some valid ones (C and C++ are the notable exception, although most languages have escape hatches). GP was saying that the fix might reject valid programs that compile today. This is true for some existing soundness bugs, but not necessarily for this one specifically.

Rust does have undefined behavior, though.

And even if the theorem prover has no errors, the math behind the theorem prover could be inconsistent according to Gödel's incompleteness theorem. So even in principle, we can never be completely certain about the soundness of Rust, though the more theoretical concerns tend to be dwarfed by basic human error.

I think it's a good thing to keep in mind, that the actual implementation of Rust almost certainly isn't sound. Even an "ideal Rust" still has unsafe, which can affect the soundness of even faraway safe code. But I don't think it's nessesarily wrong to talk about Rust as if it were safe. Much of our communication has implicit assumptions, and the way we talk about Rust is no different. It would be exhausting to qualify every discussion of saftey with "assuming the compiler has no bugs", "assuming all unsafe code follows the (not fully specified!) rules", etc.

Ultimately it's like any other implementation of theory into practice. The theoretical model of Rust lets us reason about and design an implementation to achieve certain practical goals even though the model is a simplification of reality. In Rust's case, practical use has demonstrated it achieves design goals like reducing bugs and reducing development time (compared to peers like C++) to a substantial degree.

Or more likely, an error in the formalization. "What you proved is true, but it's not sufficient for what you care about." See for example WPA2 KRACK attacks after WPA2 was proven secure.

This moving of goal posts whenever correctness through type systems is being discussed is a bit tiresome, because it quickly leads to such ad absurdum corner cases.

Yes, you are all correct. The compiler may have a bug. And if it does not, then the type system may have a problem. And if it is formally verified, then the theorem prover might have issues. And if it does not, then the very math it relies on may be wrong.

But what do we contrast this to, what is the alternative to correctness through the type system? Almost every time, when it isn't "nothing", it's "tests". We rely on tests to test whether the program behaves correctly.

And as we all know, quite in contrast to type systems and their checkers, tests are always error-free, complete, and sensible?

No, people who don't actually use Rust just like to pretend it's something more than it is, for some performative outrage or something.

Here's the current list of similar (unsoundness-causing) open compiler bugs in Rust:

https://github.com/rust-lang/rust/issues?q=state%3Aopen%20la...

You can't formally verify the soundness of something that inherently necessarily relies on hardware implementations that themselves could be faulty.

Note that the Lean kernel itself is not formally verified.

No, this isn’t the way to interpret this. Rust has been very successful not just in appearing safer, but actually delivering safety over C. The sense of safety was almost entirely real. Just some situations it didn’t cover.

> but now we can say it gave the false sense of safety

Except we can't say that, at all. This is just a single bug in relatively obscure code, so 99.99999% of your code remains safe.

Meanwhile in C, 100% of your code has the potential to trigger a similar bug, except there's no path for the underlying cause to ever be fixed, unlike here.

You're essentially complaining that something isn't 100% safe, but that's just your misconception of what "safe" means. Nothing is 100% safe, not can it ever be.

It's especially ridiculous to then compare something 99.999% safe to something 0% safe and conclude that all that "supposed safety" is useless, because look: in 0.001% of cases it's NOT safe!

Imperfection isn’t evidence of ineffectiveness.

Considering this has gone unflagged for 11 years... Finding a flaw in Rust’s safety guarantees doesn’t mean that they provide no benefit, over a programming language without them.

> Note that Rust is not a theorem prover

Not that that would make any difference, theorem provers can also have bugs. Famously this summer someone “disproved” the collatz conjecture by exploiting a soundness bug in Lean.

Because people want a performant optimizing compiler.

There is a severe misunderstanding here. Beside being only a subset, CompCert definitely has UB. It just formalizes codegen for codebases not containing UB, which obviously won't be enough for Rust.

Also unlike C, it should be possible to formalize all of Rust, not just a subset. For two reasons: Rust evolution (not initially but today) is strongly tied with formalizing it and the language team consults with formalization experts (which are part of the Rust project themselves) all the time (and formalization or semi-formalization projects are ongoing), and also the mathematical understanding of system languages itself has advanced.

Yeah this is actually quite interesting. I can see how people who have this "slop generator" perspective on AI would see this as an irony. But to me, it isn't an irony, it's a demonstration of why this perspective on AI is wrong.

Something something halting problem. I never said don't use the tool!! I use the tool too! I just dont want to talk/read about it all the time.

Programming will never be dead.

1. Because the situation you describe is fantasy.

2. Even if it is a reality and all software can be verified (it cant), I will still be programming and so will millions of others because its fun, programming and sex are really damn close to things I cant live without. Not everyone got into engineering for the money. I legitimately love this activity, it is my actual passion. I would rather be poor than give it up.

Its like im being told everyday all day, non stop that the thing I love is not worth loving.

Thank you for citing the Anthropic propaganda manual!

I didn't realize that, thanks

Unfortunately, a large proportion of stories submitted to Lobste.rs are slopped out... even if they don't mention AI, it's hard to escape there. Hacker News at least has functioning story-level moderation.

Wow interesting

Yeah the HN home page today seems especially bad

Oh that is very nice. I had been thinking about building something like that, happy to see someone beat me to it. Might actually make me check hacker news more frequently again.

Rust considers fix to unsoundness bug, a change that can be done at any SemVer revision (i.e. a patch version bump can break it).

If your spacebar heater relies on such behaviour Rust can and will break it. If you're in the crater group you'll be notified and urged to upgrade it.

Wait, there's a proven subset of C? Can you point me to some info?

You're mistaking the semantics of the type system, from the implementation. I'm not talking about verifying the compiler. There's nothing to verify there.... literally. There is no spec to the language. By definition it is verified because the only verification you can do is tautological: "does this rust compiler do what this rust compiler does?"

But the unsoundness is because the type system itself, abstractly, was not verified. Or the interactions between parts. I.e. If you verified the compiler you'll find that it implements the algorithms perfectly. But tells you nothing about whether those implemented algorithms, however perfectly implemented, actually provided those guarantees.

>Rust cannot fail, it can only be failed...

Sweet. But why should anyone care..

Would you say the same thing about Java? It’s type system is also unsound.

I don't think the definition of "memory safe" has ever required full end to end stack conformance with a proof. Very few languages have achieved that, though some have. Most people call Java memory safe, C#, Python, Typescript, etc - all of those fall short of a formally verified, sound type system with a verified toolchain.

> Rust cannot fail, it can only be failed.

“Please build the perfect system. Because I specified ‘perfect’ any flaws are due to your incomplete implementation, not my awful brief.”

If the person writing the rust spec was a client I would have to drop them because they would be setting themselves up for dissatisfaction.

https://github.com/model-checking/verify-rust-std

hm, there's an effort but scoped only to the std

It's terrifically complex: https://doc.rust-lang.org/beta/nightly-rustc/rustc_middle/ty...

not of the implementation. Of the type system. And a verification of subsets, but not a verification of their interactions == the whole system is unverified.

That's verifying the implementation. The type system wasn't verified. It implements stuff perfectly, it has tests that prove it, but nobody formally verified that they perfectly implemented the correct algorithms

While true, there are two important differences:

1) Unsoundnesses in Java's type system are checked at runtime.

2) They (or at least some) are intentional or at least won't-fix bugs.

Both are not true for Rust.

Relatively uncommon as in there is not, as far as I know, a single mainstream language with a formally verified spec.

I wouldn’t say so… I consistently choose Rust mainly because it’s a sanely designed modern C++ alternative. It’s 20% more effort than writing Python or Typescript, and you get to use the full power of your hardware without compromise.

Safety is a nice side-benefit. The main reason why I like the safety is because it allows you to fearlessly write high-level code without being constantly paranoid about memory as in C++. It’s more about enabling ergonomics without loosing performance, rather than security or correctness.

Rust has a lot of things that make it nice to write in. Robust enums and pattern matching are something I miss greatly when I’m back in C++. The trait inheritance system is also very flexible and I miss that. Especially compared to monstrosities like multiple inheritance.

Part of Rust's schtick is also cost free abstractions.

Only people who don't write Rust think Rust's whole shtick is safety.

Consider reading past the hashtag.

Idk, it also has a nicely expressive typesystem outside of lifetimes, a lot of modern syntactic features like pattern matching and monadic error handling, well-written compiler error messages, a well-designed standard library, and substantially less accrued cruft when compared to its largest competitor. Safety might be the cudgel its evangelists like to beat everyone over the head with, but there are certainly things to recommend it outside of that.

To be very pedantic, Python was always strongly typed in the sense that every value has a concrete type. This is very different to, e.g. C, where `void*` is often used to actually erase the type or, conversely, more abstract languages where there are only interfaces.

But of course Python function were always duck typed so it often didn't matter to the user.

If you deal mainly with small-to-medium size Python programs, which is probably the norm, that makes sense to me. But if you have a large Python application, or if you own a library API that might have a lot of callers, typecheckers catch sooo many mistakes.

I've been writing python for closing in on two decades (I want to say maybe 2.5 was my introduction point?).

I've found type hints to be remarkably useful and catch significantly more bugs than I ever would have thought, and have quickly picked up the practice of using them wherever I code. My general finding is that if I have to struggle to put useful type hints in place, I probably need to rethink my code.

I even type hint my unit tests because I've learned that sometimes type incorrectness means my tests haven't been testing what I thought they were testing.

Frameworks like pydantic[0] can help you turn those type hints into something runtime enforcing too.

[0] https://pydantic.dev/docs/validation/latest/get-started/

You can't rely on Python's type hints for serious verification, but it can be great for expressing abstractions and giving people (and, today, agents) better affordances for using them. Even static errors that will not always fire can still help a lot for using a library correctly and for noticing mismatches in your codebase as it evolves over time.

> it seems plausible to hit by mistake

The report seems to claim the opposite:

> Looking at the bug itself, it is also very likely that this unsoundness has not caused memory unsafety by accident. While it looks easy to trigger, to exploit this you need an intentionally malicious Drop implementation.

> This bug however is quite dangerous, because unlike many soundness bugs it seems plausible to hit by mistake.

Possibly. I'm no rust expert, so I had the read the code slowly, building up a mental model of the types being used. For me, the effort that required is one of the more painful aspects of Rust.

Nonetheless when I got to this line, I stopped reading:

    q.0 = Some(&l);

Given the type declarations it's "obvious" it should not compile as it directly contradicts the types 'static lifetime. You don't deliberately write code that doesn't compile.

I write lots of code that doesn't compile of course. It's perfectly safe because the compiler catches it. Right now, I feel like a climber at the top of a mountain who just discovered he forgot to attach his safety harness.

Who knows. Maybe all of crates.io will compile with the fixed compiler, because this is a mistake humans or LLM's never make. We will see.

> It leads to broken OOM behaviour

no it doesn't. the broken oom behavior is distros not configuring earlyoom/systemd-oom properly. The problem here is that the kernel doesn't know what software is critical to your OS so the distro needs to be responsible for what processes to protect.

For apps that need to handle oom, Linux is missing something a handle to tell apps to shrink their memory use. Apple does this and it seems to work quite well (and proves that Linux style overcommit works well since it's what they use)

The issue and none of the comments mention AI. It is pretty clear your parent said it by themselves.

I was just checking what outcome an LLM would have based on the patterns in its probabilistic distribution it has seen the wild.

Most LLMs would probably say this piece of code won't compile.

What does "q.0" and "Some(...)" mean?

So the equivalent in C would be:

        $ cat main.c
        #include <stdlib.h>
        #include <string.h>

        struct Q {
                /*@null@*/ /*@only@*/ char * t;
        };


        /*@only@*/
        struct Q *
        Q_new (/*@only@*/ char * t)
        {
                struct Q * q = malloc (sizeof *q);
                q->t = t;
                return q;
        }

        void
        Q_set (struct Q * q, /*@only@*/ char * t)
        {
                free (q->t);
                q->t = t;
                return;
        }

        void
        Q_free (/*@only@*/ struct Q * q)
        {
                free (q->t);
                free (q);
                return;
        }



        int
        main (void)
        {
                /*@only@*/ char * l;
                /*@only@*/ struct Q * q;

                l = strdup ("");
                q = Q_new (NULL);

                Q_set (q, l);
                free (l);

                /* This is UB */
                Q_free (q);

                return EXIT_SUCCESS;
        }

        $ splint main.c
        Splint 3.1.2 --- 21 Feb 2021

        main.c: (in function Q_new)
        main.c:15:3: Arrow access from possibly null pointer q: q->t
          A possibly null pointer is dereferenced.  Value is either the result of a
          function which may return null (in which case, code should check it is not
          null), or a global, parameter or structure field declared with the null
          qualifier. (Use -nullderef to inhibit warning)
           main.c:14:17: Storage q may become null
        main.c: (in function main)
        main.c:43:6: Unrecognized identifier: strdup
          Identifier used in code has not been declared. (Use -unrecog to inhibit
          warning)
        main.c:44:13: Null storage passed as non-null param: Q_new (NULL)
          A possibly null pointer is passed as a parameter corresponding to a formal
          parameter with no /*@null@*/ annotation.  If NULL may be used for this
          parameter, add a /*@null@*/ annotation to the function parameter declaration.
          (Use -nullpass to inhibit warning)
        main.c:47:8: Dead storage l passed as out parameter to free: l
          Memory is used after it has been released (either by passing as an only param
          or assigning to an only global). (Use -usereleased to inhibit warning)
           main.c:46:12: Storage l released
        main.c:12:1: Function exported but not used outside main: Q_new
          A declaration is exported, but not used outside this module. Declaration can
          use static qualifier. (Use -exportlocal to inhibit warning)
           main.c:17:1: Definition of Q_new
        main.c:20:1: Function exported but not used outside main: Q_set
           main.c:25:1: Definition of Q_set
        main.c:28:1: Function exported but not used outside main: Q_free
           main.c:33:1: Definition of Q_free

        Finished checking --- 7 code warnings

(The equivalent warning is main.c:47)

> rust will drop the string l before q

Why?

I know the borrow checker uses rules, but I don't know enough about the internal implementation details to use fully precise terminology. I don't mean borrow checking is just a chain of if-statements or something. I meant check in the abstract.

From the GitHub thread: "I think unification just generally doesn't check lifetime bounds of the type." [0]

There are steps, or rules or whatever, that perform soundness (or well-formedness or whatever) checks. And clearly one was missing.

My guess was just that maybe someone didn't think it was necessary for soundness.

[0]: https://github.com/rust-lang/rust/issues/164250#issuecomment...

How many of them only conditionally implement Drop, based on a generic param lifetime?

OK. That's good to know. I'm not sure why sharing our professional experience with this type of code is controversial, but here we are.

I'm not defending rust here - a correctness bug invalidates the premise. But I am saying that I've never seen a custom drop in production.

For some reason this is controversial, but it remains true.

No we're in a situation where a bug in the type checker was found and will be fixed and a new release will be made.

That it took 11 years for someone to come across this is a fairly intense counterargument to your attempt to paint this as a language with dangerous footguns.

Since the Rust language is defined by the Rust compiler and has no other specification, if it's UB in the compiler then it's UB in the language.

Sure, I think it was still under the same unsound tag regardless.

I think you are talking about a different problem and that has nothing to do with my comment.

Yes. In fact, I have met quite a few humans who make a point NOT to go bashing the work of others. (Of course, I have also met quite a few who do spend their time bashing others.)

The more you understand about your own system the more humility one would think you would have. This is like the dumb guy to jedi meme. It's the people in the middle that shit on other peoples' work because they have something to gain by looking comparatively smarter.