Computer Security versions of the Halting Problem
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.