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.
Until it's installed on a computer that uses an Intel (tm) processor, that is....
SImpsons: Sarcasm Detector
Interesting, but how do you prove the proof?
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.
Here's the interesting bit about what they actually did:
The platform needed the capacity of a traditional software language like C++ and the logical syntax and structure of proof-assistant programs like Isabelle and Coq, which mathematicians have been using for years. No such all-in-one platform existed when the researchers started work on EverCrypt, so they developed one — a programming language called F*. It put the math and the software on equal footing.
“We unified these things into a single coherent framework so that the distinction between writing programs and doing proofs is really reduced,” said Bhargavan. “You can write software as if you were a software developer, but at same time you can write a proof as if you were a theoretician.”
If a CPU tells you that 1+1=3, does this mean the math is faulty or the CPU failed?
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.
Couldn't help but notice the code is built with a compiler named "KreMLin". Isn't that interesting.
It's possible to be mathematically perfect...in fact, mathematically is pretty much the only way to be "completely" or "perfectly" anything.
The basic problem with mathematical proofs is that math is an abstraction (the model), and the perfect-and-complete nature of the proof can *only* ever apply to the abstraction. The degree of fidelity to which the model reproduces your particular real situation is another story. Mathematically proving your solution is perfect not meaningful by itself.
It's a huge red flag the the vendor in this ad is directing our attention to a meaningless mathematical proof of perfection in their product. This strongly suggests to me that there is no valid reason to trust their design.
Even if we stipulate a "perfect" set of cryptographic algorithms implemented in a mathematically "perfect" set of code, the solution is meaningless without proper implementation and user procedures.
For example: I've got a great VPN (it uses OpenVPN), but when it fails, all my traffic is suddenly exposed. So I adjust my firewall rules so the only traffic allowed besides that needed to establish the vpn link must go through through tun0. Or use wireguard instead. Until next week when I'm in a factory and I need to talk to some PLCs or I/O modules to configure them, then I turn off the firewall or use the "factory" instead of the "office" setting. Now I have to remember to turn it on again or I won't be protected. etc. etc. etc.
There are no "magic bullets", and somebody claiming to have one has just saved you the trouble of evaluating them any further.
"Reality is that which, when you stop believing in it, doesn't go away." - Philip K. Dick
Proving the code that USES their library is yet another thing.
That's the rub. There will be some wrapper written to make parameter exchange automatic, or facilitate finding a VPN gateway, or whatnot, and it'll undo all the hard work in a few lines of hastily coded VB.
There's a hard and fast requisit for establishing a MITM-proof crypto channel: you have to exchange some keying material safely... whether that's through a CA system or a preshared key or whatever, it simply must be done... and the users will choose the software which skips that step because someone assured them it is taken care of automagically, and well heck, that's much easier.
Someone had to do it.
It' impossible to prove that your crypto library is invulnerable to side-channel attacks. It is possible, however, to prove it's not vulnerable to common side-channel attacks. That's not nothing.
Their marketing hyperbole is so over the top, however, that I wouldn't trust them with anything.
A big problem in general in software crypto is that it's impossible to prove that the random/entropy source provided by the processor is good. There's no software work-around to that - oh, you can try to use I/O timings and so on, but those can be manipulated. Even if the code that generates the mask that is used in the fab is proven correct, we know the NSA is capable of tampering with the mask between code and fab.
After the Snowden revelations were understood, paranoid crytpo guys reached the point of "I can't only trust a hardware entropy source that I build myself from components I bought myself in person from a random store." That's not exactly productizable, but it's a fair assessment of the threat of the NSA.
Socialism: a lie told by totalitarians and believed by fools.
Reminds me of the famous Donald Knuth quotation: Beware of bugs in the above code; I have only proved it correct, not tried it.
Formal verification has huge potential, and can (theoretically, at least), be applied to any software that doesn't have side effects (which mainly means: everything is an input or output parameter - no GUIs, no external input/output, etc..). It's really cool to have something significant that has been formally verified.
That said, formal verification still only takes you so far. There is no way for them to have proven immunity to side channels, or immunity to processor vulnerabilities, or even immunity to brute-force attacks. So this is an important battle, but it doesn't automatically win the war.
Enjoy life! This is not a dress rehearsal.
While you probably can't prove that the compiler will do what you think it will do, and you probably can't prove that the CPU will execute the compiled code the way you think it will, could you prove that your source code does not have a specific set of common developer introduced programming errors? A quick scan of the article seemed to indicate that this was the actual claim. While not earth shattering, it does seem useful.
Of course there is. Code is executed in a logical way. Saying their code is mathematically free of bugs is both valid and provable. Now whether the compiled result, the platform or hardware allows an exploit to run on the final binary is a completely different argument.
I don't see why the NSA would care. They can already get your passwords anyway. My guess is that, if they wanted to, they would just look at every key I type into my computer and save all that data. Which includes my passwords. They could do it by changing my hardware, or putting cameras in my house, or various known remote attacks. Or failing that they could use a wrench to get the passwords out of me.
Protecting yourself from state level actors is too damn difficult for an individual to do.
Your ad here. Ask me how!
Their marketing hyperbole is so over the top, however, that I wouldn't trust them with anything.
Really? What is the "marketing hyperbole" you're talking about? The only hypebole I've seen in this case comes from journalists.
That's true. One can prove that a particular function is correct, that their code is correct. In this case, library code.
Crypto library code is very linear, no conditionals, just a sequence of math operations. I don't think it's hard to prove correctness.
This is just marketing wank.
No sig today...
[ ] you understood G”oels incompleteness theorem
Not disagreeing, just clarifying.
Yes you can prove that it is unaffected by known, enumerated side-channel attacks in the processor / chipset.
You can't prove it would be unaffected by unknown CPU side-channel.
ALSO you can prove that there are no side channels in the code itself - you can enumerate the state parameters which affect the functioning of the code, both internal and external state parameters.
The distinction becomes important when you start proving more than one component of the system. If you prove the library code - including against aide channels in the code, and you prove any kernel - including kernel side channels, and you prove the microcode - including microcode side channels, and you prove the hardware - including hardware side-channels, then you've proved the system to be free of side channels, and the application code, then you've proved the system.
In proving the system, you prove that the output state is identical *per the specification*. If you specify "identical state" as high and low CMOS output, you'll have no side channels re high vs low - but you could still have a high at 3.28 volts vs a high at 3.29 volts.
I found this issue on github and it appears they are not as good as claimed, this is a security 101 mistake. "Currently the generated C functions don't check for the proper length of the input arrays. Indeed the user can read it from the original F* code, but when they make a mistake the code still executes and reports success (like in #53 ). Would be possible to add bound checks on inputs and return an error code (like 1 in case of aead_encrypt "
Yes.
https://xkcd.com/538/
Just because I can hook a shark from a boat, I do no offer to wrestle it in the water.
If you were going to wave a rag in front of the hacker "bull" then claiming some code was proven secure is just the way to do it.
politicians are like babies' nappies: they should both be changed regularly and for the same reasons
Consider the case where the guy is working for the NSA out of college, and then, as an NSA employee, applies to Intel or whoever in hopes of getting into position to make such a change. He has a bright future within the NSA, and a second income for a while.
Socialism: a lie told by totalitarians and believed by fools.
The mathematical proof must be translated into code. You're either dumb or naive if you think that can be done flawlessly.
TFA actually does a good job of discussing it in layman's terms. It's surprisingly devoid of hype and hyperbole.
As a starting point that's not TFA, Formal Verification is the sub-field of CS that this is based on: https://en.wikipedia.org/wiki/...
-Chris
C++ compiler: object is never read from after being zeroed, thus by the abstract machine specification the last write does not lead to any observable behaviour and can be skipped.
It isn't skipped if the program uses the memset_s defined in C11 to modulate the compiler's inference that the zeroing "does not lead to any observable behaviour".
Java JIT: No reads between zeroing and freeing/next writes, skip zero writes. This is an important optimization since by specification all objects are zero initialized, leading to large amounts of overhead if the writes cannot be skipped.
Even if the char[] holding the secret's UTF-16 encoding is cleared by by Arrays.fill method? Oracle itself uses this in its example for Swing JPasswordField .
Any modern OS: let me copy that buffer to the swap file.
A modern OS denies reading swap by nonadministrators within the OS and encrypts swap to protect it from reading outside the OS.
Any SSD: you want to override this? Lets do some wear levelling and overwrite that other location instead.
It's as if you think disk encryption is impossible.