Re: Curious
Is this necessarily so? ie is it that no finite computation can always determine the memory safety of arbitrary chunk of code? I don't imagine its equivalent to the halting problem
To me this looks pretty much identical to the Halting Problem. Adapting the classic simple proof ...
Assume we have a function MemSafe(Code) that returns true/false depending on whether the supplied Code (for this we can take it to be the text of the code) is memory safe or not.
We now create the code (assuming the programming language we are using allows us to do something that is not memory safe):
if MemSafe(Code) then
<<Do something that is not memory safe>>
end if;
If we now apply MemSafe() to this code does it return true or false? It is a classic self-reference paradox (remembering that 'arbitrary' is a rather broad category). The natural conclusion is that we cannot create the function MemSafe() that will work for any arbitrary code.
Of course if the programming language does not allow violation of memory safety the whole question is rendered moot and the function can simply be "return true;"
Anyhow, whilst this is an interesting point in Computer Science it really only serves to show that you cannot write arbitrary code and hope to always be able to prove it is safe.
Those with an interest in proving memory safety should not be writing arbitrary code. They should be following design and coding practices that make proving memory safety straight-forward - in the same way that those concerned with proving the real-time behaviour of their code should not be adopting design and coding practices that make establishing worst case execution time difficult (which would certainly preclude code where it is not possible to determine if it halts).
This all leads back to the inconvenient truth that safety and security (and verifying it) needs to be considered as a fundamental aspect of design and implementation.