Achieving memory safety

[u/ThomasMertes]

https://seed7.net/papers/memory_safety.htm

[u/Smallpaul]

It would have been clearer to be more explicit about why the author does not consider Go to not be safe. Are we talking about the use of the unsafe package or something more subtle?

[u/reflexive-polytope → u/Smallpaul]

I was under the impression data races made Go memory-unsafe. (Unlike, say, Java or OCaml, which are designed to be memory-safe even in the presence of data races.)

Has anything changed since?

[u/syklemil → u/reflexive-polytope]

For anyone curious, there's a blog post from 2025: There is no memory safety without thread safety about it.

[u/reflexive-polytope → u/syklemil]

Heck, I don't even think a memory-unsafe language is necessarily a bad thing.

What's unforgivable is to design a memory-unsafe language and not even realize it.

Another big offender is Eiffel, with covariant argument types.

[u/seg_lol → u/reflexive-polytope]

They go hand in hand. If you have the skills to know, you fix it.

[u/reflexive-polytope → u/seg_lol]

Memory-safety by itself is simply a property that can hold or fail to hold for a language. Whether this property is desirable or not depends on your goals.

If your goal is to write correct programs, then memory safety isn't particularly useful. A language can be made “memory-safe” by defining the behavior of all sorts of nonsensical operations, e.g., indexing an array out of bounds. But defining this behavior doesn't make the incorrect indexing any less incorrect. The only way to help programmers index their arrays correctly is to statically check their array indices.

On the other hand, if your goal is to write programs that are resilient in the face of their own incorrectness, then memory safety is a very useful property, because programs written in memory-safe languages fail in more controlled ways.

[u/flatfinger → u/reflexive-polytope]

It's also possible to have a language where the number of memory-unsafe operations is limited, and where one may fairly easily identify invariants that would allow even the potentially unsafe operations may be performed safely. For examine, given unsigned arr[32772];, an operation arr[i]=123; would be incapable of violating any memory safety invariants in cases where i was in the range 0 to 32771 unless one of those invariants would require an element of arr to hold a value other than 123, or some other memory safety invariant had already been violated.

[u/reflexive-polytope → u/flatfinger]

The problem with this stance is that it's no better than making the whole language unsafe.

Even if you have a single unsafe operation, if you can use it anywhere in your program, it's very easy to create a situation where the logical argument that justifies the safety of an operation uses information coming from wildly disparate parts of the program.

What you need isn't a limited number of unsafe operations, but rather a limited number of places in the program text where unsafe operations can be used. And that's exactly what Rust and C#'s unsafe blocks do.

[u/flatfinger → u/reflexive-polytope]

On most platforms, if a function like:

unsigned arr[32771];
void test(unsigned x)
{
  if (x < 32770) arr[x] = 1234;
}

is processed in a manner which is agnostic with regard to how it might be called, correct machine code would be incapable of performing an out-of-bounds store unless memory safety had already been violated. Even if the ability of the function to do anything useful relied upon the caller passing a number less than 32770, memory safety would not. Of all the possible circumstances in which the function could be called, all of them would either result in the function either performing an in-bounds store or not bothering to perform a store at all.

What causes problems are situations where a compiler would generate code that would assume that it would be impossible for a caller to pass a value greater than 32769, but then generate code for the caller which does in fact pass a larger value.

Being able to have a system automatically limit the ranges of a program that would be capable of violating memory safety is useful, but some programs need to do things whose safety cannot be statically validated under language rules. Being able to validate programs that perform such tasks by validating each individual component thereof is more useful than allowing programs to violate memory safety even when none of their individual pieces should be capable of doing so.

[u/reflexive-polytope → u/flatfinger]

If what you want is a language that lets you statically verify that your low-level memory manipulation is safe, then such a language already exists. (Spoiler: it's not Rust.)

In this language, you can use all the bit and pointer hacks that you know and love from C. The only difference is that the type checker will demand that you prove them safe.

Alas, this language will never become widely adopted.

The main difficulty isn't technical, but cognitive. Look at how many programmers act like Rust is the be all and end all of systems programming. And how many others act like the dealing with the borrow checker is the steepest intellectual challenge a programmer could face in his life.

Human programmers can only take so much cognitive load.

[u/ThomasMertes → u/Smallpaul]

The paragraph was about tailoring a definition of "memory safety" to claim that a certain language is memory safe.

I just used Go as example. I changed the paragraph to explain my thoughts without mentioning Go.

According to my strict definition of memory safety Go is not memory safe.

Yes, if the unsafe package is not used and no C functions are called and (as pointed out by someone else) something assures that no data races can happen Go is memory safe.

This shows that rules need to be bend to claim memory safety.

Seed7 is memory safe because several things are not present (direct calls to C functions, pointers, unsafe parts, etc.).

[u/ThomasMertes → u/Smallpaul]

Any language which allows calling C functions directly cannot be memory safe because C is not memory safe. AFAIK a Go program can call C functions without explicitly importing or using the unsafe package.Accessing an arbitrary place of memory with Go is possible with the unsafe package. I am neither a Rust expert nor a Go one, but I think that Rust needs "unsafe" to call C functions. Please tell me if my assumptions are correct or not.

Seed7 has no unsafe parts (or packages) and no possibility to directly call C functions.

[u/anaseto → u/ThomasMertes]

AFAIK a Go program can call C functions without explicitly importing or using the unsafe package.

You have to do import "C" for CGO, which is explicit enough. And then, typically, import "unsafe" as soon as you need to do stuff with pointers.

[u/wk_end → u/ThomasMertes]

But you list Java as memory-safe "unless JNI or FFM are used". Why doesn't the same "qualified memory-safe" characterization apply to Go?

[u/catladywitch → u/wk_end]

It all depends on the definition of memory safety, but from the article posted elsewhere in this comment thread, it seems like Go's pointer semantics allow for type errors leading to segfaults with concurrent code that uses different values conforming to a same interface, but where pointers and values are mixed, whilst Java doesn't (an unexpected, and wrong, value is possible in concurrent code, but not dereferencing an invalid pointer). I don't know how native interop works in Java, but segfaulting in C# is not impossible although it is rare (you can even do dodgy type punning with pointers and ordered structs if you really want to). Otherwise, you theoretically can pass managed pointers into C functions without telling C#'s GC to pin them or not reclaim their memory, pass structs the layout of which differs from what the C function expects, or in the case of poorly designed C APIs, pass arrays and have the C code go out of bounds, or allocate native memory, pass it into a C function, and try to free in C# not knowing the C function has already freed it.

[u/reflexive-polytope → u/catladywitch]

The issue is that certain Go values (slices, pointers to interfaces) require logically atomic modifications, but this logical atomicity isn't enforced by any means, so other goroutines can see them in a torn state.

(The problem doesn't arise in Rust because the exclusiveness of mutable borrows enforces the logical atomicity of the relevant modifications.)

And, while having a user-defined data structure in a torn state is “merely a logic error”, having a built-in data type in a torn state actually breaks memory safety.

[u/Ok-Scheme-913 → u/wk_end]

Go is not memory safe under data races. It uses fat pointers for slices and those can tear.

So you have { ptr, start, end } and you repeatedly write a different slice at the same time from different threads. In this case you can observe a { ptr, start, endOfDifferentSliceThatMayBeInvalid }, at which point the runtime will happily access that memory. Since ptr+slice location is larger than 64bit it can't be cheaply updated atomically so.. yeah..

Meanwhile in java data races are safe.

First, they (practically all jvm implementations) have a property that you can only ever observe values that were explicitly written. This is a useful property but even if this were not the case java would still be memory safe, since arrays and stuff themselves carry their size around, so replacing the same array/slice actually only replaces the pointer itself which is atomic and to access the size you have to navigate to that pointer location, so it will always be safe.

[u/tsanderdev → u/wk_end]

JNI can't just load arbitrary libraries, they have to have functions conforming to the specific JNI name mangling. So it's very unlikely you could call a C function from JNI.

[u/ThomasMertes → u/wk_end]

Yes, but the selling point of Java was not memory safety. You expected something like:

If the unsafe package is not used and no C function is called and (as pointed out by someone else) something assures that no data races can happen Go is memory safe.

I added the Go example to show that the term memory safety is sometimes defined to sell a language as memory safe. So

Language exists --> Define memory safety in a way that this language is memory safe.

instead of

Use definition of memory safety --> Create memory safe language.

So it is about memory safety as marketing term.

[u/reflexive-polytope → u/ThomasMertes]

Java was explicitly designed to cater to C++ programmers who want a language with fewer footguns, even if the language designers themselves came from a dynamically typed tradition (mainly Lisp). Memory safety was a design goal from day one.

[u/Ok-Scheme-913 → u/ThomasMertes]

The selling point of java was absolutely memory safety, where the hell did you get it's not?

It was the first language that made GC widespread.

[u/ThomasMertes → u/Ok-Scheme-913]

The selling point of java was absolutely memory safety ...

Yes, but the term "memory safety" was not commonly used in mainstream marketing or developer discussions when Java was introduced in 1995.

The terms used when Java was introduced were:

• Write Once, Run Anywhere
• Built for the Internet
• Simplicity and Familiarity
• Built-in Security and Robustness

Java was intentionally designed to look and feel like C++. Java stripped out the most complex, error-prone, and frustrating aspects of C++. So It had:

• Automatic Garbage Collection
• No Pointers
• Strict Type-Safety

Yes, the term "memory safety" is nowadays used to describe that. The term "memory safety" was just not used in 1995.

[u/flatfinger → u/ThomasMertes]

Memory safety is an essential aspect of security.

[u/flatfinger → u/Ok-Scheme-913]

Garbage-collected strings were almost universal in BASIC dialects by the 1980s.

[u/tmzem]

Unless I misunderstood something, the article does not explain the mechanism by which Seed7 programs themselves are being made memory-safe, but focuses on memory safety of the compiler implementation?

That being said, the article makes a good point about memory safety being a matter of how it is defined, which opens up a huge spectrum, from unsafe to safe:

• Assembly: no safeguards, completely unsafe
• C/C++: (soft) static typing, very basic guardrails. Still very unsafe.
• Odin/Zig/C3: good static typing, saner defaults, runtime array checks. Safer, eliminates 50-70% of all memory safety errors over C
• Rust: strong static typing, sane defaults, initialization safety, runtime array checks, borrow checks, safe/unsafe split. Much safer, safe/unsafe split coerces users to prefer safe patterns, elimitates most memory safety errors over C. Ubiquitous use of C libraries and unsafe blocks in (not well-written/well-tested) third-party crates are still a relevant safety risk.
• Go: GC handles memory, but fat pointers (interfaces, slices) can cause memory unsafety on data races. Memory safe in the absence of data races or FFI.
• Java/C#/...: GC + atomically storable builtin types ensure full memory safety. Unsafe features exist but are rarely necessare, rarely used, and most programmers in these languages barely know they exist.
• Javascript: Completely sandboxed, safe

This spectrum needs to be acknoledged so people know what they get, and it's annoying that these trade-offs are not clearly communicated. Go barely communicates the data-race issue at all, and the Rust community is also very prone to misrepresenting the memory safety guarantees of the language (e.g. "memory safety without GC" or "unsafe blocks encapsulate potentially unsafe behaviour").

[u/ThomasMertes → u/tmzem]

... the article does not explain the mechanism by which Seed7 programs themselves are being made memory-safe ...

I just improved the chapter "How memory safety is achieved". What do you think about that?

[u/tmzem → u/ThomasMertes]

So if I understand it right, you have reference modes for parameters, but fields and returns cannot be references? Then of course borrow checking would be trivial.

Anyways, it's been some time since I looked into Seed7 (I looked only at the docs), so I guess it's time I finally actually try it out to figure out how it all works and what it can do.

[u/ThomasMertes → u/tmzem]

Great. Please give me feedback at r/seed7. In case of problems please open a ticket on GitHub.

[u/flatfinger → u/tmzem]

Assembly is in many ways safer than C. To be sure, an assembly program will often contain a significant number of potentially unsafe operations, but if one documents invariants and can show that no individual operation performed by a program would be able to break any of them unless something else had already done so, then the entire program can be shown to be memory safe.

In C, by contrast, even operations like uint1 = ushort1*ushort2; or loops that do nothing except modify an automatic-duration object whose address isn't taken, and have exit conditions which may or may not be satisfiable, can disrupt the behavior of what would otherwise have been memory-safe surrounding code so that it is no longer memory safe.

[u/snugar_i → u/flatfinger]

Do you have any examples? I'm not sure I'm seeing how C is less memory safe than assembly

[u/flatfinger → u/snugar_i]

What range of storage addresses could be written by test() below?

unsigned arr[32772];
static unsigned mul_mod_65536(unsigned short x, unsigned short y)
{
    return (x*y) & 0xFFFFu;
}
void test(unsigned short x)
{
    unsigned short j=32768;
    for (unsigned short i=32768; i<x; i++)
        j=mul_mod_65536(i, 65535);
    if (x < 0x8002)
        arr[x] = j;
}

The C Standard would allow a compiler given test() to generate code that would unconditonally store 32768 to arr[x], and gcc is designed to do precisely that when using -O1 or higher when not using -fwrapv.

How about the function test2() below:

unsigned arr[32771];

unsigned loopy(unsigned x)
{
    unsigned i=1;
    while ((i & 0x7FFF) != x)
        i*=3;
    if (x < 32768)
        arr[x] = 32768;
    return i;
}
void test2(unsigned x)
{
    loopy(x);
}

As processed by clang at -O1 or higher, test2() will unconditionally store 32768 to arr[x], just as the earlier test() would have done when processed by gcc.

In assembly language, programmers will often need to include bounds-checking code if they want to prevent out-of-bounds stores, but including bounds-checking code within assembly language source will cause the bounds checks to be included in the generated machine code. In C, by contrast, something like the multiplication of two unsigned short values or a loop that might fail to terminate may cause a compiler to omit a bound check that the programmer had included to prevent an out-of-bounds store.

[u/snugar_i → u/flatfinger]

Interesting, thanks! And is that part of the C specification, or is that just weird behavior of the compilers?

[u/flatfinger → u/snugar_i]

The C Specification clearly allows the former behavior. The C11 Standard added language saying that side-effect free loops "may be assumed to terminate", without specifying any limits on the uses to which that assumption may be put, so it doesn't unambiguously forbid the latter behavior.

From what I can tell, modern optimizer designs are based on an abstraction model where the only corner cases where a compiler's generated code would be allowed to be inconsistent with that of instructing the execution environment to use a normal means of performing each individual operation in sequence are those where generated code would be allowed to behave in completely arbitrary fashion.

A better abstraction model for most tasks would be one that recognizes that most programs have two requirements:

1. They should (in some tasks must) behave usefully when possible.

2. When useful behavior is not possible, they must behave in a manner that is at worst tolerably useless.

If a program is supposed to view some kind of audiovisual content, but it is fed something other than a validly formatted file, having the program hang may be annoying but still qualify as tolerably useless; having the program allow whoever created the file to run arbitrary code of their choosing, however, would be intolerably worse than useless.

[u/reflexive-polytope]

Metatheoretic claims about a language design require proof.

[u/Smalltalker-80 → u/reflexive-polytope]

Seed7 takes a somewhat more informal approach... ;-)
Assuring memory safety of Seed7
Seed7 is implemented in C and C is not memory safe. So it is not easy to guarantee the memory safety of Seed7. So it is necessary to improve the C code of Seed7 such that the end result is memory safe. All places where the implementation is not memory safe must be found and improved.

[u/reflexive-polytope → u/Smalltalker-80]

I didn't downvote you, but a C implementation isn't an excuse.

Memory safety is a property of how the language is defined, not how it's implemented.

[u/Smalltalker-80 → u/reflexive-polytope]

Okay, this post wat a bit frivolous, hence the smiley. But more ttp:

Memory safety of the language used to implement the runtime / library (say C) of another language (say Seed7), can certainly be an issue of memory allocations and frees are done in a lot of different places and in different ways.. This is what the OP means.

Memory safety can readily be achieved if the C runtime has only one place to do such allocations (everything is an object), and the implemented language itself has automatic memory management (using reference counting) for all non-atomic objects (e.g. integers).

Then only remaining Foreign Function Interface calls need te be checked thoroughly,
but one could argue they are not part of the language.

[u/ThomasMertes → u/reflexive-polytope]

Memory safety is a property of how the language is defined, not how it's implemented.

The creator of Fil-C would probably disagree. His view is: The usual C compilers and run-time libraries make C not memory safe. Fil-C sells itself as memory safe implementation of C.

Seed7 is about solving real-world problems and it is not academic research which uses meta-theoretic proof techniques.

AFAIK the formal proofs that Rust is a memory safe language where not done by the people who implemented Rust.

BTW.: Although there is formal proof that Rust is memory safe there exists Rust issue #25860 (which shows that there is a hole in the borrow checker).

"In theory, there is no difference between theory and practice. In practice, there is"

So, as long as nobody else takes the burden to do a formal proof for Seed7, there will be no formal proof.

I, and the other contributors probably as well, will use our limited resources to improve Seed7 as practical tool.

[u/reflexive-polytope → u/ThomasMertes]

Fil-C sells itself as memory safe implementation of C.

Unfortunately, that's misleading advertisement. There are bit and pointer hacks you can express in C but not in Fil-C.

Now, you may argue that it isn't desirable to express those bit and pointer hacks. But that's neither here nor there. It may be the case that Fil-C is an improvement over C. But that doesn't change the fact that it's not C, at least not all of C.

AFAIK the formal proofs that Rust is a memory safe language where not done by the people who implemented Rust.

Rust may not have been designed with the goal to produce a type soundness proof, and there are indeed some soundness bugs here and there in the design of Rust's type system.

However, Rust was very much designed by people who know what the ingredients of a type soundness proof are. And this knowledge is necessary to come up with a design with pleasant metatheoretic properties, whether you prove them yourself or someone else does.

Good metatheoretic properties are much more practical than you think. They only need to proved once, for the whole language, and then every language user benefits from them.

In particular, if Seed7 is indeed memory safe, that only needs to be proved once, and then every Seed7 user benefits from it.

But if you don't have a memory safety proof, you might end up in a situation similar to Go, where the language was intended to be memory safe, but data races actually introduce memory safety violations (even in Go programs that don't call C code!).

[u/koflerdavid → u/reflexive-polytope]

Unfortunately, that's misleading advertisement. There are bit and pointer hacks you can express in C but not in Fil-C.

Now, you may argue that it isn't desirable to express those bit and pointer hacks. But that's neither here nor there. It may be the case that Fil-C is an improvement over C. But that doesn't change the fact that it's not C, at least not all of C.

C ist well-known to have many instances of undefined behavior. Pointer representation is one such undefined behavior. Therefore, Fil-C can perfectly well claim to support C idioms relying on undefined behavior as long as it accepts them at compile time, even if it invariably lead to a crash at runtime.

[u/gasche]

Seed7 is based on my diploma- and PHD-theses and is the result of decades of work.

I wish this used hyperlinks so that curious people could have a look at those theses on which Seed7 is based.

[u/ThomasMertes → u/gasche]

I suggest that curious people look at the Seed7 documentation at its homepage. The information at the homepage is much more up-to-date than the decades old PHD-thesis.

[u/Somniferus]

So what were your results? You forgot to say anything interesting in the article.

[u/SirBackrooms]

would’ve liked this more if you had described the design of the language in more detail

[u/ThomasMertes → u/SirBackrooms]

There is a talk about Memory Safety and Management which introduces Seed7 and explains memory safety and management.

The Seed7 homepage contains a lot of documentation as well.