A lot of comments on this thread ponder the difference between logical and physical, between software and hardware bugs. There is absolutely no difference. As a kind reminder, computation is a physical process, period. Any proofs of correctness apply only within the confines of the model in which they are proven. To the folks fond of formal verification, methinks Kripke agrees. To the folks presenting hardware bugs as a counterexample, it is not. If you include hardware bugs in your security analysis, and you should, you are merely taking a wider view of the system.