[nmrm2]

I think with security (and esp. privacy), the problem is more coming up with the specs in the first place. If you can do that in a reliable way, designing appropriate static analyses is probably doable.