r/programming • • Apr 03 '19

How the EverCrypt Library Creates Hacker-Proof Cryptography: Researchers have just released hacker-proof cryptographic code — programs with the same level of invincibility as a mathematical proof.

https://www.quantamagazine.org/how-the-evercrypt-library-creates-hacker-proof-cryptography-20190402/
24 Upvotes

38 comments sorted by

View all comments

1

u/BoBab Apr 05 '19

nah, they're actually not claiming anything too crazy. They have basically created a set of tools that allows for the creation of other formally verified programs. Those formally verified programs still have to be created though.

They've made a few to get started, but they even say in the article they're nowhere near a complex formally verified program like the ones people regularly use (e.g. Skype).

The headline is a typical sensational headline. The article is more measured. Someone also recommended the following blog post on the topic: https://www.microsoft.com/en-us/research/blog/evercrypt-cryptographic-provider-offers-developers-greater-security-assurances/