Comment on Hacking the Apple Webcam (Again)parentComments−astrange4yI'm not sure you can actually prove a TLS implementation is correct. It depends on the system clock being right, OCSP server being online, etc.Even the encryption has to be free of side channels like timing attacks which are left out of what most people think of as a proof.−wyager4yYou can prove a TLS implementation correct up to defined assumptions (e.g. clock consistency). There are already some projects working on this, eg https://project-everest.github.io/
Comments
I'm not sure you can actually prove a TLS implementation is correct. It depends on the system clock being right, OCSP server being online, etc.
Even the encryption has to be free of side channels like timing attacks which are left out of what most people think of as a proof.
You can prove a TLS implementation correct up to defined assumptions (e.g. clock consistency). There are already some projects working on this, eg https://project-everest.github.io/