The halting problem only tells you that there can be no algorithm to prove this automatically for any given program.

It could still be the case that for all practically relevant programs there is a proof in each case that they are secure, even if there is no automatic way to find it.