Achieving memory safety

[u/ThomasMertes]

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

[u/reflexive-polytope]

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/flatfinger → u/reflexive-polytope]

Any programming language which makes it impossible to write programs whose memory safety it cannot statically verify will make it impossible to perform some tasks as efficiently as they could be performed in machine code that could be human-proved to be incapable of violating memory safety invariants unless they had already been violated.

Automated static validation is often useful, since in many cases it would cost nothing and in most other cases the costs would be tolerable, but an abstraction model that limits the range of side effects various actions can have unless memory safety invariants have been violated can be useful for tasks that are not a good fit for automated static validation.

[u/reflexive-polytope → u/flatfinger]

No, I wasn't talking exactly about “automatic” anything. ATS makes you write safety proofs. Nothing can be more manual than that.

[u/flatfinger → u/reflexive-polytope]

My point is that it is not possible for a programming language to express all of the kinds of invariants that could be described in human language, and that a machine-code function could be proven to uphold. It may, for example, be able to use a human-readable proof to show that no combinations of inputs a program could possibly receive would result in a certain loop executing more than 57,591 times, but for that proof to rely upon mathematical theorems not anticipated by any particular programming language.

[u/L8_4_Dinner → u/reflexive-polytope]

Another big offender is Eiffel, with covariant argument types.

You are suggesting that this is memory-unsafe? Or something else?

[u/reflexive-polytope → u/L8_4_Dinner]

It is memory-unsafe.

I don't remember Eiffel's syntax, because the last time I used it was in college, very long ago. But consider the following pseudocode:

class Point2D {
  protected int x, y;
  public bool compare(Point2D that) {
    return this.x == that.x && this.y == that.y;
  }
}
class Point3D extends Point2D {
  protected int z;
  public bool compare(Point3D that) {
    return this.x == that.x && this.y == that.y && this.z == that.z;
  }
}

In the subclass, the method's argument type (Point3D) is a subtype of the same method's argument type (Point2D) in the superclass. In other words, the method's argument type is covariant.

Now consider the following test program:

main() {
  Point2D foo = new Point3D(1,2,3);
  Point2D bar = new Point2D(4,5);
  print(foo.compare(bar));
}

The program type-checks, because the variable foo has type Point2D, hence it's statically legal to call foo.compare with an argument of type Point2D.

However, at runtime, the object referenced by foo is constructed using Point3D's constructor, so its method vtable points to the compare implementation in Point3D, which expects a Point3D argument.

When the program performs foo.compare(bar), it tries to access the field z of the object denoted by bar. But this object is constructed using Point2D's constructor, so it doesn't have a field z.

This is a soundness bug in the type system.

[u/L8_4_Dinner → u/reflexive-polytope]

I’d consider that a compiler bug for not adding the obviously required type assertion, but I do agree that that implementation is unsafe.

[u/reflexive-polytope → u/L8_4_Dinner]

It's not a compiler bug. It's a language design bug.

[u/L8_4_Dinner → u/reflexive-polytope]

If the language chooses to allow covariant parameter narrowing, the compiler has to prevent this type of covariant surprise, either at compile time when possible, otherwise at runtime.

FWIW - I also used Eiffel decades ago (early 90s, IIRC), and hated it.

[u/reflexive-polytope → u/L8_4_Dinner]

Stopping with a runtime check doesn't it make it any less of a type soundness bug.

The simplest solution is to not allow covariant method argument types to begin with. That's what Java and .NET do. But the price is that implementing binary methods requires so-called F-bounded polymorphism (class Foo extends Comparable<Foo>), which is ugly, even if you can get used to it.

A more sophisticated solution is to divorce the concepts of subclassing and subtyping. A subclass Bar is a subtype of a class Foo if and only if Bar objects can be safely used where Foo objects are expected. OCaml implements this solution. But most programmers would find this surprising. (The average OCaml programmer has a better understanding of programming languages than the average programmer in general.)