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...
Interesting, but not unheard of. Think of attacks like Row Hammer. No revolutionary physics needed. But chip designers cannot fully apply quantum field theory to an entire CPU, so they necessarily use simplified a simplified physics model. The resulting chips then need to be empirically verified to correct places where that simplified model diverges to much from the messy reality, which means that the chip design is only as good as the empirical testing done to it.
Add to that the potential for unknown and mis-moddeled manufacturing defects, and manipulated electrical voltages and signals, random particle interactions, and there is a lot of room for known physics to break a verilog level proof of correctness.
Comments
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.
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...
A backdoor in physics would be interesting indeed, but not as likely as a rogue agent in a TSMC fab...
Interesting, but not unheard of. Think of attacks like Row Hammer. No revolutionary physics needed. But chip designers cannot fully apply quantum field theory to an entire CPU, so they necessarily use simplified a simplified physics model. The resulting chips then need to be empirically verified to correct places where that simplified model diverges to much from the messy reality, which means that the chip design is only as good as the empirical testing done to it.
Add to that the potential for unknown and mis-moddeled manufacturing defects, and manipulated electrical voltages and signals, random particle interactions, and there is a lot of room for known physics to break a verilog level proof of correctness.