Improved article about memory safety

[u/ThomasMertes]

Thank you to everyone who gave feedback on my article about memory safety.

I used the input to vastly improve the article (see "Achieving memory safety").

Please take a look and share your thoughts again and consider starring the Seed7 project on GitHub.

[u/Athas]

Since memory safety is all about avoiding accidental mistakes and also intentional maliciousness from scoundrels, I am going to ask some slightly antagonistic questions:

Seed7 is memory safe and there are no unsafe parts. A Seed7 function cannot read secret data stored somewhere in your program.

Does Seed7 restrict IO operations in any way? On many operating systems, if you can do IO, you can read arbitrary memory through various mechanisms (on Linux, via the /proc filesystem). This is the case for most memory-safe languages and is usually not considered a major problem, but it means you need to be very precise about what exactly Seed7 guarantees. There are languages in which functions absolutely cannot do this, but they tend to be languages that require you to be explicit about IO in the type system. From browsing the Seed7 documentation, it seems conventional in its handling of IO.

Objects and other data which needs to be referenced several times use reference counting. This data is freed when the reference counter reaches zero.

How does Seed7 deal with circular references and the risk of memory leaks? This is a bit of a trick question, as memory leaks are often defined as not an aspect of memory safety (e.g. Rust programs can leak), but it is still a common memory bug that can lead to program malfunction.

Therefore, in addition to a formal proof of the language specification, a proof of the actual implementation is needed as well.

Usually the formal proof is the first step, and only very rarely is the actual implementation proven correct as well. This is because proving an actual implementation correct is significantly more complicated. In fact, even the formal proof for the language definition is usually on a simplified subset. Auditing and testing the implementation (as you do) is of course still a useful activity, and provides a lot of bang-for-the-buck.

[u/ThomasMertes → u/Athas]

Does Seed7 restrict IO operations in any way?

Depending on how you opened a file reading or writing might not be allowed and attempting to do so will trigger the exception FILE_ERROR. Beyond this, there are no restrictions.

On many operating systems, if you can do IO, you can read arbitrary memory through various mechanisms (on Linux, via the /proc filesystem). This is the case for most memory-safe languages and is usually not considered a major problem, but it means you need to be very precise about what exactly Seed7 guarantees.

This wasn't on my radar. I expected that operating system privileges would handle that, but this seems not to be the case. I asked Google AI and got:

Under Linux, no special or elevated privileges (like root or capabilities) are needed to read the memory of your own process via the /proc file system.

I need to consider that.

There are languages in which functions absolutely cannot do this, but they tend to be languages that require you to be explicit about IO in the type system.

How is this done?

I can imagine that the functions that open a file, look at the path and fail if the memory of the own process is requested. But this is operating system specific and it might not be easy to make it 100% correct.

Maybe it is possible to tell the OS that accessing the own memory should not be allowed for the current process. I saw that on Linux there is prctl() and seccomp(). Maybe these can be used.

How does Seed7 deal with circular references and the risk of memory leaks?

Contrary to languages with pointers, Seed7 was not designed to support implementing low-level data structures such as linked lists. So instead of using pointers to create e.g. linked lists Seed7 proposes using container types like array and hash to build complicated data structures.

That said, circular references could lead to memory leaks. BTW., neither the Seed7 example programs nor the Seed7 run-time libraries contain any circular reference.

Usually the formal proof is the first step, and only very rarely is the actual implementation proven correct as well.

When using a programming language the memory safety of the actual implementation is what counts. It does not help if a language is formally proven to be memory safe if it is not in practice.

[u/koflerdavid → u/Athas]

Does Seed7 restrict IO operations in any way? On many operating systems, if you can do IO, you can read arbitrary memory through various mechanisms (on Linux, via the /proc filesystem). This is the case for most memory-safe languages and is usually not considered a major problem, but it means you need to be very precise about what exactly Seed7 guarantees. There are languages in which functions absolutely cannot do this, but they tend to be languages that require you to be explicit about IO in the type system. From browsing the Seed7 documentation, it seems conventional in its handling of IO.

The claim about not being able to access any secrets stored somewhere else in memory is definitely tacky. On the other hand, memory safety is something distinct from sandboxing and thus this hole should be disregarded. In-process sandboxing is extremely hard to achieve since the POSIX security model draws security boundaries at user level; everything below is assumed to play nice to each other.

[u/ThomasMertes → u/koflerdavid]

I just added the chapter "A loophole introduced by operating systems" to the "Achieving memory safety" article.

What do you think about that?

[u/koflerdavid → u/ThomasMertes]

I'm unfortunately not knowledgeable enough to judge whether there are other holes that have to be closed, or whether it is indeed possible to close all avenues that a process can use to break its own memory safety. There is a reason why Android assigns separate users to each app to segregates them.

[u/Athas → u/[deleted]]

How is this done?

In Haskell, whether or not the function can do IO is part of the type system. If you have a function of type Int -> Int, then it cannot possibly do any kind of IO operation (assuming you're not using escape hatches like unsafePerformIO, but those can be disabled). Haskell is however coarse-grained, so if you have a function of type Int -> IO Int, then it can do any kind of IO, including going into /dev and /proc to subvert process memory (or more directly just use library IO functions to mess with the process). Despite its coarseness, this is still a pretty useful distinction in practice, although it is not something you can retrofit onto a classical language. A major current research topic in programming languages is to make this distinction more fine-grained, so we can talk more precisely about which effects a function may have. Look up languages like Koka or Flix as examples of languages with "effect systems". Personally I am skeptical of splitting up true IO effects, as once you can read/write files, you can do basically anything.

When using a programming language the memory safety of the actual implementation is what counts. It does not help if a language is formally proven to be memory safe if it is not in practice.

Indeed, but proofs of implementation correctness are so rare that we usually cannot expect them. Also, implementation bugs are reasonably easy to fix, whilst fundamental unsafety in the language design is much harder.

I should note that my guesstimate is certainly that Seed7 is memory safe, because it omits the features that usually lead to memory unsafety. It doesn't even have threads, as far as I can see, which is otherwise sometimes a way in which unsafety can sneak in undetected.

[u/ThomasMertes → u/Athas]

In Haskell, ... so if you have a function of type Int -> IO Int, then it can do any kind of IO, including going into /dev and /proc to subvert process memory ...

So for functions which allow IO there is no distinction between normal reading from a file and reading its own memory via /proc.

For memory safety I would need exactly this distinction. Having a class of functions which are not allowed to do IO does not help in this regard.

Protecting a program against reading its own memory via /proc needs a different strategy.

The Seed7 run-time could check the path every time a file is opened. This would include absolute and relative paths to /proc/self/mem, /proc/self/maps, /proc/thread-self/mem, /proc/thread-self/maps, /proc/<PID>/mem, and /proc/<PID>/maps.

As an alternative functions which open files could be protected like this:

prctl(PR_SET_DUMPABLE, 0);
aFile = fopen(...);
prctl(PR_SET_DUMPABLE, 1);

Sub-processes could still access the memory of the parent process. To prevent this prctl(PR_SET_DUMPABLE, 0) would be necessary for sub-processes as well. But with prctl(PR_SET_DUMPABLE, 0) a process cannot be debugged.

I should note that my guesstimate is certainly that Seed7 is memory safe, because it omits the features that usually lead to memory unsafety.

Thank you.

[u/Athas → u/ThomasMertes]

Protecting a program against reading its own memory via /proc needs a different strategy.

This is impossible to do. You need to rethink the definition of memory safety, because if you include arbitrary IO, then there is no way to avoid arbitrary system-level actions. What would prevent an IO function from launching another process, perhaps a shell script, to do whatever you are trying to prevent in your library? I see that Seed7 has a Shell library, so this is straightforward today. There is also /dev, which contains ways of modifying system memory if the process is privileged.

These are not Seed7-specific concerns. Any memory safe language that supports IO must be careful to specify what they mean by memory safety, and my guess (it's not my field) is that it's usually a guarantee "modulo external effects caused by IO", or something like that.

[u/ThomasMertes → u/Athas]

Protecting a program against reading its own memory via /proc needs a different strategy.

This is impossible to do.

Why?

As far as I know a process that uses prctl(PR_SET_DUMPABLE, 0); cannot read its own memory via the /proc filesystem. And the PR_SET_DUMPABLE flag is inherited to child processes so they can't access the memory of their parent either. So launching another process or a shell script will not help.

What a privileged process can do is something different. Keep in mind that memory safety weaknesses are usually exploited to get superuser rights. If you are already superuser you have all power to do dangerous things.

These are not Seed7-specific concerns.

Yes. This is something that the operating system needs to fix, since this memory safety loophole is provided by it. prctl(PR_SET_DUMPABLE, 0); comes quite near to a fix, but it prevents debugging and maybe other useful things. What is needed from the operating system is something that prevents any access to the own process memory and also prevents any child process to do so (this is what prctl(PR_SET_DUMPABLE, 0); does) and additionally allows debuggers to read the memory (since the debugger started the process).

Hopefully Linux will do its homework. :-)

modulo external effects caused by IO

I will think over such a refinement of my definition of memory safety. Loopholes provided by the OS are definitely a thing.

[u/Athas → u/ThomasMertes]

Why?

I am not a security expert, so a specific analysis is beyond my ken. However, the basic problem is that the Unix security model is not intended to protect processes from other processes running as the same user. This means that if you take a sufficiently broad view of "memory safety" (broader than any other language), then performing IO (or in particular launching other processes) becomes a problem. I think the right solution is to not use such a broad definition of memory safety.

What a privileged process can do is something different.

In some sense it is more important that root processes are safe, because they can compromise the entire system. This matters only on servers of course; on personal machines the normal user account has access to all data that matters. Also, various common container techniques (like Docker) often run processes as the root user, and it would be strange if a language security guarantee depends on what user ID it runs under.

Yes. This is something that the operating system needs to fix, since this memory safety loophole is provided by it.

They will not fix it, since your definition of memory safety is not shared by other languages, and the security properties you expect are intentionally not part of the security model guaranteed by operating systems. I'm not a Windows expert, but since you can inject threads into processes with the same user, I'm sure you can easily break memory safety that way if you keep this extremely strict definition of memory safety.

[u/ThomasMertes → u/Athas]

I just added the chapter "A loophole introduced by operating systems" to the "Achieving memory safety" article.

What do you think about that?