On Wed, 20 Dec 2023 13:19:09 +1300, Peter Reutemann wrote:
-- source: https://arstechnica.com/security/2023/12/hackers-can-break-ssh-channel-integ...
I found this part hilarious: While the risk Terrapin poses varies, it invalidates proofs published in 2016 that concluded such attacks weren’t possible. The real lesson is that practical evaluations, like the one provided in Monday’s research, are crucial for revealing previously overlooked flaws in such proofs. This reminds me of a quote from Donald Knuth, back in the day: “Beware of bugs in the above code; I have only proved it correct, not tried it.” In computer programming, we rely primarily on testing to assure ourselves that our code is correct. In some reliability-critical applications, one may also find use of techniques to try to prove programs correct. These tend to take a lot more effort to apply, which is why they are not more widely used. Also I have always wondered about how you might find bugs in such proofs. Conversely, mathematics is all about proving theorems correct. If there was a way to somehow test those theorems as well, it seems to me that would be useful for uncovering potential bugs in those proofs.