Comment by gizmo686

You don't need to prove the hardware correct to prove that the software is free from timing side-channels. You just need a model of the hardware that captures timing information.

Sure a hardware or model bug would render your proof non-applicable, but that is already the case for the existing proofs.

The bigger problem is simply that hardware designers do not care about timing side channels. Even if you did accurately model the timing behavior of a modern processor, you would just discover that trying to write software free from timing side channels is a practical impossibility.

> And then you'd need assurance that the Verilog is faithfully transcribed in the silicon, which is a can of worms in itself.

You would also need to prove that our model of physics accurately describes how that silicon would behave, and the the environment around the silicon is within the physical parameters you modeled...