Computer Security versions of the Halting Problem I'm plenty familiar with the Halting Problem for Turing Machines. It occurred to me after reading several posts on this site that it would be interesting, educational and useful to start a list of equivalents to the Halting Problem in terms of Computer Security. I think this might help students of computer science and allied areas come to appreciate the true depth and application of the Halting Problem in whatever their application area.

So, I ask that the proposed (or actual) equivalent problem be:

(1) One that makes sense in the domain of computer security. This can be from information management, Cryptography, hacking, or programming (ideally with a security bent, since there are plenty of Halting equivalent problems already well known in the world of programming languages and compilers).

(2) One stated with a reference to literature on that subject if possible, and maybe even (although I wouldn't require it) a proof if you know of an elegant one.

Example: I have an antivirus software on my machine, and I want to know
whether it will ever execute malicious code. As far as I can tell, this is the Halting problem in disguise.
What you're looking for is Rice's Theorem, which is a generalized version of Halting Undecidability.

It basically says that any property of a Turing Machine (i.e. any computer program) is undecidable, if it's a property of the behavior of the program (i.e. a property of the language it accepts/produces), as opposed to a particular syntactic feature of the implementation. This holds unless it's a trivial property (always true or always false).

For example, deciding "Does instruction X ever get executed" or "Is a high security value stored in low security memory" are all questions about program behavior.

But things like "does this program contain a for-loop" or "is this program type-correct" aren't behaviors, because there might be equivalent programs which don't have the same values for those properties. 
You can phrase a program with a for-loop as using while-loops without changing the behaviour, or you can make a version of a program which behaves correctly but doesn't check under your typing discipline. So these aren't properties of the behavior, they're properties of the particular implementation.