Reminds me of Steve Ballmer touting Windows XP as the "Most secure operating system ever" - on the day it was released. Claims that a code is unbreakable or hacker proof are big red flags.
On second thought, I think deliberately releasing a PR advertisement which claims a system is "unbreakable" can be a good way to receive free security audits.
So perhaps EverCrypt as a free and open source project who understands this point, the developers deliberately allowed Quanta Magazine to use this title, and so far, it has successfully received the attention of at least 5 HN users...
The mathematical proof might be 100% solid and hacker proof. The implementation will probably never be.
I agree, I see a few ways that it could go wrong:
- Code is proven correct against the specification, but specification is wrong/buggy
- source code is correct/secure, but compiler is overzealous and botch the securities guarantees.
*for certain definitions of 'unbreakable'
A holiday sweater is more bullet resistant than a thin t-shirt, but no one would say a holiday sweater is "pretty bullet proof".
That virus was running around the internet for years; kept alive by the "most secure operating system ever".
In the immortal words of the virus: "billy gates why do you make this possible ? Stop making money and fix your software!!"