Memory Safety for Skeptics

I've actually been trying to figure out if it's practical to write assembly but then use a proof assistant to guarantee that it maintains safety. Weirdly feels easier than C insofar as that you don't have (C's) undefined behavior to contend with. But formal methods are a whole thing and I'm very very new to them so it remains to be seen whether this is actually a good idea, or awful and stupid:) (Edit: ...or merely impractical, for that matter)

These C++ developers I'm mentioning are all at least senior (some of them staff+), which makes their remarks on segfaults scary, because clearly, they haven't realized that a segfault is the best case scenario, not the worst one. This means that they very much need a refresher course on memory safety and why it matters.

The fact that they assume that they're good enough to avoid memory errors without tooling despite the fact that most of these errors are invisible and may remain invisible for years before being discovered is a second red flag, because it strongly suggest that they misunderstand the difficulty.

Of course, the conversation between you and I is complicated by the fact that the same words "memory safety" could apply to the programming language/tooling or to the compiled binary.

A logic bug in a library doesn't break unrelated code. It's meaningful to talk about the continued execution of a program in the presence of logic bugs. Logic bugs don't time travel. There are ways to exhaustively prove the absence of logic bugs, e.g. MC/DC or state space exploration, even if they're expensive.

None of these properties are necessarily true of memory safety. A single memory safety violation in a library can smash your stack, or allow your code to be exploited. You can't exhaustively defend against this with error handling either. In C and C++, it's not meaningful to even talk about continued execution in the presence of memory safety violations. In C++, memory safety violations can time travel. You typically can't prove the absence of memory safety violations, except in languages designed to allow that.

With appropriate caveats noted (Fil-C, etc), we don't have good ways to retrofit memory safety onto languages and programs built without it or good ways to exhaustively diagnose violations. All we can do is structurally eliminate the possibility of memory unsafety in any code that might ever be used in a context where it's an important property. That's most code.

https://georgemauer.net/2017/10/07/csv-injection.html

The problem with memory unsafe code is that it can have unexpected and unpredictable side-effects. Such as subtly altering the critical data you're exporting, of letting an attacker take control of your CSV exporter.

In other words, you need quite a lot of context to figure out that a memory bug in your CSV exporter won't be used for escalation. Figuring out that context, documenting it and making sure that the context never changes for the lifetime of your code? That sounds like a much complex proposition that using memory-safe tools in the first place.

Materials to be consumed by engineers are often unsafe when misused. Not just programs like toolchains with undefined behaviors, but in general. Steel beams buckle of overloaded. Transistors overhead and explode outside of their SOA (safe operating area).

When engineers make something for the public, their job is to combine the unsafe bits, but make something which is safe, even against casual misuse.

When engineers make something for other engineers, that is less so; engineers are expected to read the data sheet.

    [A] program execution is memory safe so long as a particular list of bad things, called memory-access errors, never occur

It's also not a meaningful concept within the C++ language standard written by the committee Herb Sutter chairs. Memory unsafety is undefined behavior (UB). C++ code containing UB has no defined semantics and is inherently incorrect, whether that's 1 violation or 1000.

Now, we can certainly discuss the practical ramifications of 95% vs 100%, but even here Herb's arguments have fallen notoriously flat. I'll link Sean Baxter's piece on why Herb's actual proposals fail to achieve even these more modest goals as an entry point [0]. No need to rehash the volumes of digital ink already spilled on this subject in this particular comment thread.

[0] https://www.circle-lang.org/draft-profiles.html

Because submitting code that invokes undefined behavior to one's compiler is a very normal thing that most working C developers do dozens of times per day, and something that a decent C compiler should behave reasonably in response to. (One could argue that crashing is acceptable, but erasing the developer's hard drive is not - but by definition that means means undefined behaviour in this situation is not acceptable).

> Suppose the user insists that he's running the compiler as a CGI script, allowing unauthenticated visitors to their site to compile programs, making it a security issue. How should Herb reasonably reply to that?

By fixing the bug?

What would you even call such a thing? "Compiler Explorer"?

I guess maybe if Herb had helped the guy who owned that web site, say, Matt Godbolt, to enable his "Syntax 2 for C++" compiler cppfront, on that site, it would feel like Herb ought to take some responsibility right ?

Or maybe I am being unreasonable ?

Herb is usually talking about the latter because of the nature of his role, like he does here [0]. I'm willing to give him the benefit of the doubt on his opinions about specific programs, because I disagree with his language opinions.

[0] https://herbsutter.com/2024/03/11/safety-in-context/

For C/C++, memory safety is a retrofit to a language never designed for it. Many people, including me, have tried to improve the safety of C/C++ without breaking existing code. It's a painful thing to attempt. It doesn't seem to be possible to do it perfectly. Sutter is taking yet another crack at that problem, hoping to save C/C++ from becoming obsolete, or at least disfavored. Read his own words to see where he's coming from and where he is trying to go.

Any new language should be memory safe. Most of them since Java have been.

The trouble with thinking about this in terms of "95% safe" is that attackers are not random. They can aim at the 5%.

[1] https://herbsutter.com/2024/03/11/safety-in-context/

> A skilled C++ programmer wouldn't be using unordered_map so it is unfair to point out you can use something bad.

Pretending defaults don’t matter is naive especially in a language that is so hostile to being easy to add 3p dependencies (even without that defaults matter).

C++ isn't my primary language. Pray tell - what's wrong with unordered_map, and what's the alternative?

Better types like VecDeque<T>, better implementations of common ideas like sorting, even better fundamental concepts like providing the destructive move, or the owning Mutex by default.

Even the unassuming growable array type, Rust's Vec<T>, is just plain better than C++ std::vector<T>. It's not a huge difference and for many applications it won't matter, but that's the sort of pervasive quality difference I'm talking about and so I can well believe that in practice this ends up showing through.

2. That's a language feature too. Writing non-trivial multi-core programs in C or C++ takes a lot of effort and diligence. It's risky, and subtle mistakes can make programs chronically unstable, so we've had decades of programmers finding excuses for why a single thread is just fine, and people can find other uses for the remaining cores. OTOH Rust has enough safety guarantees and high-level abstractions that people can slap .par_iter() on their weekend project, and it will work.

This matches my experience with the runtimes in question—I tried Bun out for a very small project and ran into 3 distinct crashes, often in very simple parts of the code like command line processing. Obviously not every crash / null-pointer dereference is a memory safety issue, but I think most people would agree that Zig does not seem to make bug-free software easier to write.

Unsafe functions mark that the caller is responsible for upholding the invariants necessary to avoid UB. In the 2021 and earlier editions, they also implicitly created an unsafe block in the body, but don't in 2024.

Or, in a more pithy tone: an unsafe block is the "hold my beer" block, while an unsafe function is a "put down your beer" function.

I'm always a little guarded about message board definitions of "memory safety", because they tend to be axiomatically derived from the words "memory" and "safety", and they tend to have an objective of saying that there's only one mainstream language that provides memory safety.

For arrays, this problem is not computable at compile time, hence the sarcastic remark that, IF THE ABOVE DEFINITION IS TAKEN AT FACE VALUE, Rust must have solved the halting problem. Downvoters are so dumb here.

  fn f(n : usize) -> usize {
    if n == 0 {
      10
    } else if n % 32327 == 0 {
      1
    }
    else {
      f(n-1)
    }
  }

  fn main() {
    let a = [1,2,3,4,5];
    let n = f(12312);
    println!("{:?}", a[n]);
  }

0: https://lwn.net/Articles/342330/

The worst case of UB is worse than the worst case of most kinds of non-UB memory safety issues.

> NULL pointer dereferences are almost never exploitable

Disagree; we've seen enough cases where they become exploitable (usually due to the impact of optimisations) that we can't say "almost never". They may not be the lowest hanging fruit, but they're still too dangerous to be acceptable.