There is still no standard, precise definition of memory safety. Here is a modest proposal.
Fact. A programming language (PL) consists of a specification and implementation.
The specification lays out precisely what the set of accepted programs is and how the code should behave when the program is executed. An implementation must conform to the specification and is what enables programmers to actually use the PL to translate programs to executable code and execute them.
Fact. Programs are executed in an execution environment.
An execution environment is not necessarily part of an implementation, but it can be (interpreter). CPU, operating system and system resources are all part of the execution environment.
Fact. A specification can, implicitly or explicitly, leave the possibility of execution errors.
Definition. There are two classes of execution errors:
- trapped errors: these are reliably detected and dealt with by the execution environment
- untrapped errors: these are not detected, and execution goes on. The specification cannot prescribe what behavior take place.
A trapped error may lead to invocation of an error handler or to execution being aborted ("fail-stop"). In contrast, untrapped errors include highly problematic situations like undetected out-of-bounds accesses, use-after-free, integer overflows. They can lead to silent data corruption, hard-to-debug crashes, and also to security vulnerabilities that can be exploited by malicious actors.
Definition: Execution Safety
A program is execution safe if its execution never leads to untrapped errors.
A language L is execution safe if all L-programs are execution-safe.
An execution environment is execution safe for a language L if execution of L-programs can never lead to untrapped L-errors.
Execution-safety does not guarantee absence of crashes, absence of memory leaks, or possibility to perform modular reasoning on programs. Nevertheless, it is a very strong guarantee and many PLs in widespread use do not have this property. Execution environments can deal with the consequences of untrapped errors, which may limit the harm even if the language used to write these programs may not be execution-safe.
Definition: Memory Safety
A program is memory safe if no memory access ever leads to untrapped errors.
A language L is memory safe if all L programs are memory-safe.
An execution environment is memory safe for a language L if execution of L-programs can never lead to untrapped L-errors due to an operation involving memory access.
Brief discussion
These definitions are directly derived from Luca Cardelli's "Type Systems" article (2004) from the CRC Handbook of Computer Science and Engineering, 2nd Edition, Ch. 97. You can find it.
Safety is commonly defined as "absence of unacceptable loss". Turning this into an effective definition in the context of programming requires to clarify what unacceptable loss is. Our definitions above are focused on the mechanics of execution: we do not talk about logic errors, stealing your private key from the .ssh directory or causing crashes. So our definition of memory safety is a "technical definition".
Nevertheless, it seems useful: it applies to a range of programming languages, and thus over a range of possible language designs.
For safety of execution environment with respoect to a language, it is subtle and important that the definition of error is tied to language spec L. When an implementation translates to a target language of CPU instructions, an operation like "dereferencing a dangling pointer" may turn into "loading memory from an address" which may not be erroneous from the target language point of view. What makes the operation in the execution environment erroneous is the intent. This intent, as far as safety guarantees go, has to be grounded in the language specification.