add Miri paper

[web.git] / personal / _posts / 2025-07-24-memory-safety.md

diff --git a/personal/_posts/2025-07-24-memory-safety.md b/personal/_posts/2025-07-24-memory-safety.md
index 74fd1b018e32ee1654389cb4831ad25c579b7825..50c5db1d59ab62b382a74caa0213b56f8e7d0b50 100644 (file)
--- a/personal/_posts/2025-07-24-memory-safety.md
+++ b/personal/_posts/2025-07-24-memory-safety.md
@@ -70,6 +70,7 @@ If you run this program (e.g. on the [Go playground](https://go.dev/play/p/SC-o_
 panic: runtime error: invalid memory address or nil pointer dereference
 [signal SIGSEGV: segmentation violation code=0x1 addr=0x2a pc=0x468863]
 ```
 panic: runtime error: invalid memory address or nil pointer dereference
 [signal SIGSEGV: segmentation violation code=0x1 addr=0x2a pc=0x468863]
 ```

+This is a segfault, not a normal Go panic, so something has gone horribly wrong.

 Note that the address that caused the segfault is `0x2a`, the hex representation of 42.
 What is happening here?
 
 Note that the address that caused the segfault is `0x2a`, the hex representation of 42.
 What is happening here?
 


@@ -78,23 +79,25 @@ Every time `repeat_swap` stores a new value in `globalVar`, it just does two sep
 In `repeat_get`, there's thus a small chance that when we read `globalVar` *in between* those two stores, we get a mix of a pointer to an `Int` with the vtable for a `Ptr`.
 When that happens, we will run the `Ptr` version of `get`, which will dereference the `Int`'s `val` field as a pointer -- and hence the program accesses address 42, and crashes.
 
 In `repeat_get`, there's thus a small chance that when we read `globalVar` *in between* those two stores, we get a mix of a pointer to an `Int` with the vtable for a `Ptr`.
 When that happens, we will run the `Ptr` version of `get`, which will dereference the `Int`'s `val` field as a pointer -- and hence the program accesses address 42, and crashes.
 

-One could construct a similar example using Go's slices, where the data pointer, length, and capacity of the slice are stored in separate words, and reading a half-updated value can lead to an out-of-bounds access.
+One could easily turn this example into a function that casts an integer to a pointer, and then cause arbitrary memory corruption.

 
 ## What about other languages?
 
 At this point you might be wondering, isn't this a problem in many languages?
 Doesn't Java also allow data races?
 
 ## What about other languages?
 
 At this point you might be wondering, isn't this a problem in many languages?
 Doesn't Java also allow data races?

-And yes, Java does allow data races, but the Java developers spent a lot of effort to ensure that even programs with data races remain entirely well-defined.
+And yes, Java does allow data races, but the Java developers spent a lot of effort to ensure that even programs with data races remain entirely well-defined and memory safe.

 They even developed the [first industrially deployed concurrency memory model](https://en.wikipedia.org/wiki/Java_memory_model) for this purpose, many years before the C++11 memory model.
 The result of all of this work is that in a concurrent Java program, you might see unexpected outdated values for certain variables, such as a null pointer where you expected the reference to be properly initialized, but you will *never* be able to actually break the language and dereference an invalid dangling pointer and segfault at address `0x2a`.
 In that sense, all Java programs are thread-safe.[^java-safe]
 
 [^java-safe]: Java programmers will sometimes use the terms "thread safe" and "memory safe" differently than C++ or Rust programmers would. From a Rust perspective, Java programs are memory- and thread-safe by construction. Java programmers take that so much for granted that they use the same term to refer to stronger properties, such as not having "unintended" data races or not having null pointer exceptions. However, such bugs cannot cause segfaults from invalid pointer uses, so these kinds of issues are qualitatively very different from the memory safety violation in my Go example. For the purpose of this blog post, I am using the low-level Rust and C++ meaning of these terms.
 
 They even developed the [first industrially deployed concurrency memory model](https://en.wikipedia.org/wiki/Java_memory_model) for this purpose, many years before the C++11 memory model.
 The result of all of this work is that in a concurrent Java program, you might see unexpected outdated values for certain variables, such as a null pointer where you expected the reference to be properly initialized, but you will *never* be able to actually break the language and dereference an invalid dangling pointer and segfault at address `0x2a`.
 In that sense, all Java programs are thread-safe.[^java-safe]
 
 [^java-safe]: Java programmers will sometimes use the terms "thread safe" and "memory safe" differently than C++ or Rust programmers would. From a Rust perspective, Java programs are memory- and thread-safe by construction. Java programmers take that so much for granted that they use the same term to refer to stronger properties, such as not having "unintended" data races or not having null pointer exceptions. However, such bugs cannot cause segfaults from invalid pointer uses, so these kinds of issues are qualitatively very different from the memory safety violation in my Go example. For the purpose of this blog post, I am using the low-level Rust and C++ meaning of these terms.
 

-Generally, there are two options a language can pursue to ensure that concurrency does not break basic invariants:
-- Ensure that arbitrary concurrent programs actually behave "reasonably" in some sense. This comes at a significant cost, restricting the language to never assume consistency of multi-word values and limiting which optimizations the compiler can perform. This is the route most languages take, from Java to C#, OCaml, JavaScript, and WebAssembly.
+Generally, there are two options a language can pursue to ensure that concurrency does not break memory safety:
+- Ensure that arbitrary concurrent programs still uphold the typing discipline and key language invariants. This comes at a significant cost, restricting the language to never assume consistency of multi-word values and limiting which optimizations the compiler can perform. This is the route most languages take, from Java to C#, OCaml, JavaScript, and WebAssembly.[^multi-word]

 - Have a strong enough type system to fully rule out data races on most accesses, and pay the cost of having to safely deal with races for only a small subset of memory accesses. This is the approach that Rust first brought into practice, and that Swift is now also adopting with their ["strict concurrency"](https://developer.apple.com/documentation/swift/adoptingswift6).
 
 - Have a strong enough type system to fully rule out data races on most accesses, and pay the cost of having to safely deal with races for only a small subset of memory accesses. This is the approach that Rust first brought into practice, and that Swift is now also adopting with their ["strict concurrency"](https://developer.apple.com/documentation/swift/adoptingswift6).
 

+[^multi-word]: Some hardware supports larger-than-pointer-sized atomic accesses, which could be used to ensure consistency of multi-word values. However, Go slices are three pointers large, and as far as I know no hardware supports atomic accesses which are *that* big.
+

 Go, unfortunately, chose to do neither of these.
 This means it is, strictly speaking, not a memory safe language: the best the language can promise is that *if* a program has no data races (or more specifically, no data races on problematic values such as interfaces, slices, and maps), then its memory accesses will never go wrong.
 Now, to be fair, Go comes with out-of-the-box tooling to detect data races, which quickly finds the issue in my example.
 Go, unfortunately, chose to do neither of these.
 This means it is, strictly speaking, not a memory safe language: the best the language can promise is that *if* a program has no data races (or more specifically, no data races on problematic values such as interfaces, slices, and maps), then its memory accesses will never go wrong.
 Now, to be fair, Go comes with out-of-the-box tooling to detect data races, which quickly finds the issue in my example.


@@ -105,15 +108,17 @@ Even experienced Go programmers do not always realize that you can break memory
 Go is a language *designed* for concurrent programming, so people do not expect footguns of this sort.
 I think that is a problematic blind spot.
 
 Go is a language *designed* for concurrent programming, so people do not expect footguns of this sort.
 I think that is a problematic blind spot.
 

-Of course, as all things in language design, in the end this is a trade-off.
+Of course, as all things in language design, in the end this is a trade-off and the Go folks are [well aware](https://research.swtch.com/gorace) of the problem.[^gosafe]

 Go made the simplest possible choice here, which is entirely in line with the general design of the language.
 There's nothing fundamentally wrong with that.
 Go made the simplest possible choice here, which is entirely in line with the general design of the language.
 There's nothing fundamentally wrong with that.

-However, putting Go into the same bucket as languages that actually *did* go through the effort of solving the problem with data races misrepresents the safety promises of the language.
+However, putting Go into the [same bucket](https://www.memorysafety.org/docs/memory-safety/) as languages that actually *did* go through the effort of solving the problem with data races misrepresents the safety promises of the language.

 The [Go memory model documentation](https://go.dev/ref/mem) is not exactly upfront about this point either: the "Informal Overview" emphasizes that "most races have a limited number of outcomes" and remarks that Go is unlike "C and C++, where the meaning of any program with a race is entirely undefined".
 You could say that the use of "most" here is foreshadowing, but this section does not list any cases where the number of outcomes is unlimited, so this is easy to miss.
 They even go so far as to claim that Go is "more like Java or JavaScript", which I think is rather unfair, given the lengths to which those languages went to achieve the thread safety they have.
 Only [a later subsection](https://go.dev/ref/mem#restrictions) explicitly admits to the fact that *some* races in Go *do* have entirely undefined behavior (which is very unlike Java or JavaScript).
 
 The [Go memory model documentation](https://go.dev/ref/mem) is not exactly upfront about this point either: the "Informal Overview" emphasizes that "most races have a limited number of outcomes" and remarks that Go is unlike "C and C++, where the meaning of any program with a race is entirely undefined".
 You could say that the use of "most" here is foreshadowing, but this section does not list any cases where the number of outcomes is unlimited, so this is easy to miss.
 They even go so far as to claim that Go is "more like Java or JavaScript", which I think is rather unfair, given the lengths to which those languages went to achieve the thread safety they have.
 Only [a later subsection](https://go.dev/ref/mem#restrictions) explicitly admits to the fact that *some* races in Go *do* have entirely undefined behavior (which is very unlike Java or JavaScript).
 

+[^gosafe]: I tried to figure out whether the Go developers themselves consider their language to be memory safe, but was not able to reach a firm conclusion. The Go website does not take a stance on the matter. In [this 2009 talk](https://www.youtube.com/watch?v=rKnDgT73v8s&t=463s), Rob Pike says memory safety is a goal of Go, but in [this 2012 slide deck](https://go.dev/talks/2012/splash.slide#49) he calls the language "not purely memory safe" since "sharing is legal".
+

 ## Conclusion
 
 I would argue that the actual property people care about when talking about memory safety is that *the program cannot break the language*.
 ## Conclusion
 
 I would argue that the actual property people care about when talking about memory safety is that *the program cannot break the language*.


@@ -125,6 +130,7 @@ The moment your program has UB, all bets are off; whether or not an attacker can
 
 In my view, there's a bright line dividing "safe" languages where programs cannot have Undefined Behavior, and "unsafe" languages where they can.
 There's no meaningful sense in which this can be further subdivided into memory safety, thread safety, type safety, and whatnot -- it doesn't matter *why* your program has UB, what matters is that a program with UB defies the basic abstractions of the language itself, and this is a perfect breeding ground for vulnerabilities.
 
 In my view, there's a bright line dividing "safe" languages where programs cannot have Undefined Behavior, and "unsafe" languages where they can.
 There's no meaningful sense in which this can be further subdivided into memory safety, thread safety, type safety, and whatnot -- it doesn't matter *why* your program has UB, what matters is that a program with UB defies the basic abstractions of the language itself, and this is a perfect breeding ground for vulnerabilities.

+Therefore, we shouldn't call a language "memory safe" if the language does not systematically prevent Undefined Behavior.

 
 In practice, of course, safety is not binary, it is a spectrum, and on that spectrum Go is much closer to a typical safe language than to C.
 It is plausible that UB caused by data races is less useful for attackers than UB caused by direct out-of-bounds or use-after-free accesses.
 
 In practice, of course, safety is not binary, it is a spectrum, and on that spectrum Go is much closer to a typical safe language than to C.
 It is plausible that UB caused by data races is less useful for attackers than UB caused by direct out-of-bounds or use-after-free accesses.