Slashdot Mirror
A Suite of Digital Cryptography Tools, Released Today, Has Been Mathematically Proven To Be Completely Secure and Free of Bugs (quantamagazine.org)
By making programming more mathematical, a community of computer scientists is hoping to eliminate the coding bugs that can open doors to hackers, spill digital secrets and generally plague modern society. From a report: Now a set of computer scientists has taken a major step toward this goal with the release today of EverCrypt, a set of digital cryptography tools. The researchers were able to prove -- in the sense that you can prove the Pythagorean theorem -- that their approach to online security is completely invulnerable to the main types of hacking attacks that have felled other programs in the past. "When we say proof, we mean we prove that our code can't suffer these kinds of attacks," said Karthik Bhargavan, a computer scientist at Inria in Paris who worked on EverCrypt.
EverCrypt was not written the way most code is written. Ordinarily, a team of programmers creates software that they hope will satisfy certain objectives. Once they finish, they test the code. If it accomplishes the objectives without showing any unwanted behavior, the programmers conclude that the software does what it's supposed to do. Yet coding errors often manifest only in extreme "corner cases" -- a perfect storm of unlikely events that reveals a critical vulnerability. Many of the most damaging hacking attacks in recent years have exploited just such corner cases.
EverCrypt was not written the way most code is written. Ordinarily, a team of programmers creates software that they hope will satisfy certain objectives. Once they finish, they test the code. If it accomplishes the objectives without showing any unwanted behavior, the programmers conclude that the software does what it's supposed to do. Yet coding errors often manifest only in extreme "corner cases" -- a perfect storm of unlikely events that reveals a critical vulnerability. Many of the most damaging hacking attacks in recent years have exploited just such corner cases.
But that's a security issue in the hardware itself. Would you claim that their program is insecure if you had a hardware system that allowed any program full access to the memory of any other program? Of course not, you'd point out that nothing could be considered secure when running on such a system so the question itself is flawed.
That's true. One can prove that a particular function is correct, that their code is correct. In this case, library code.
Proving the CPU hardware and microcode is a separate step. Proving the code that USES their library is yet another thing.
All of these can be done. It's just expensive, so you use the simplest thing that will get the job done - prove a little MCU used as a cryto co-processor, not a complex Intel CPU.
I am guessing you never used earlier Windows versions.
From the article:
Yet while EverCrypt is provably immune to many types of attacks, it does not herald an era of perfectly secure software. Protzenko noted there will always be attacks that no one has thought of before. EverCrypt can’t be proven secure against those, if only for the simple reason that no one knows what they will be.
If it comes from a theorem prover, and includes a trace of the proof, then it can be checked with a proof checker. Proof checkers are generally much simpler than theorem provers, because they only need to mechanically check that the proof trace is consistent, whereas a theorem prover has to *find* that trace. Worst case is that you check the steps yourself.
Ezekiel 23:20
Incredible...I could actually hear the eyes of everyone who suffered through Windows ME rolling at that.
Blank until
[ ] you understood G”oels incompleteness theorem
Yes.