[Ygg2]

> People talk as if "memory safety" was a PLT axiom. It's not; it's a software security term of art.

It's been in usage for PLT for at least twenty years[1]. You are at least two decades late to the party.

    Software is memory-safe if (a) it never references a memory location outside the address space allocated by or that entity, and (b) it never executes intstruction outside code area created by the compiler and linker within that address space.

[1]https://llvm.org/pubs/2003-05-05-LCTES03-CodeSafety.pdf

[zbentley]

Not GP, but that definition seems not to be the one in use when describing languages like Rust--or even tools like valgrind. Those tools value a definition of "memory safety" that is a superset (a big one) of the definition referenced in that paper: safety as preventing incorrect memory accesses within a program, regardless of whether those accesses are out of bounds/segmentation violations.

[adgjlsfhk1]

it's not, but for a very subtle reason. To prove memory safety, you need to know that the program never encounters UB (since at that point you have nothing known about the program)

[Wowfunhappy]

...by that definition, can a C program be memory safe as long as it doesn't have any relevant bugs, despite the choice of language? (I realize that in practice, most people are not aware of every bug that exists in their program.)

[cibyr]

Can a C program be memory safe as long as it doesn't have any relevant bugs? Yes, and you can even prove this about some C programs using tools like CBMC.

[Waterluvian]

This is way outside my domain but isn’t the answer: yes, if the code is formally proven safe?

Doesn’t NASA have an incredibly strict, specific set of standards for writing safety critical C that helps with writing programs that can be formalized?

[okanat]

There are safety recommendations / best practice standards like CERT. None of them will prevent you from making intentional looking but logically unsound memory unsafe operations with C and C++. The code can be very indistinguishable from safe code. The things that C and C++ allow you to do basically makes code written in those languages impossible to fully formally prove. Although there are subsets, the basic integer operations and primitive types are messed up with C. So without uprooting how basic integer and pointer types work, it is impossible to make C and C++ safer. Such change will make all C and C++ programs invalid.

C and C++ always defaults to minimum amount of safety for maximum allowance of the compiler interpretation. The priority of the language designers of them is keeping existing terrible code running as long as possible first, letting compilers interpret the source code as freely as possible second.

That's why many military and aerospace code actually uses much safer and significantly more formally verifiable Ada.

[uecker]

There is also a lot of formally verified in C.

[spookie]

> impossible to formally prove

If you assume the entire lang, yes. If you use a large subset, no. Furthermore, compiler interpretation might actually be sane! There are more compilers out there than GCC, Clang or MSVC. I suspect many assumptions are being made on this claim.

[Waterluvian]

Thanks for explaining that. It really fills in a lot for me.

[arto]

https://david-haber.github.io/posts/the-right-stuff/

[ratmice]

It just seems like a bad definition (or at least ambiguous), it should say "cannot", or some such excluding term. By the definition as given if a program flips a coin and performs an illegal memory access, are runs where the access does not occur memory safe?

[Ygg2]

Sure. It can be. In the same way, a C program can be provably correct. I.e., for all inputs it doesn't exhibit unexpected behavior. Memory safety and correctness are properties of the program being executed.

But a memory-safe program != memory safe language. Memory safe language helps you maintain memory-safety by reducing the chances to cause memory unsafety.

[tremon]

There is a huge difference between "a C program can be memory safe if it is proven to be so by an external static analysis tool" and "the Java/Rust language is memory safe except for JNI resp unsafe sections of the code".