A Suite of Digital Cryptography Tools, Released Today, Has Been Mathematically Proven To Be Completely Secure and Free of Bugs (quantamagazine.org) 194
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.
Completely secure and free of bugs. (Score:5, Funny)
Yes, the code is right, only the code. Not "secure (Score:5, Informative)
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.
Re:Yes, the code is right, only the code. Not "sec (Score:5, Insightful)
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.
Re:Yes, the code is right, only the code. Not "sec (Score:5, Interesting)
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.
Re: (Score:3)
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.
Re: (Score:3)
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 pro
Re: (Score:2)
Rowhammer is a hardware problem (Score:2)
Auditing the hardware is important. It's not part of auditing the software. They are two separate processes, both important.
The eventual goal (dream) is to prove the entire system, we prove as much of it as budget allows. To prove a system, we must identify the components and prove each component. That is, we must prove the hardware, we must prove the microcode, etc.
Hardware can be vulnerable to Rowhammer.
Hardware can be proven to be vulnerable to Rowhammer, or not vulnerable. The definition of proving
Re: (Score:2)
An argument could be made that, given the knowledge of a particular hardware vulnerability, software can eliminate the risk when being run on that hardware by working around that vulnerability (to whatever extent is possible).
Can even prove it by removing constraint (Score:2)
By defining "correct" or "expected" hardware behavior as allowing Rowhammer to occur, one can even prove that the software (kernel) will do the right thing despite Rowhammer. That would be very interesting.
Probably more practical would be proving that no code path allows neighboring memory rows to be accessed at a rate faster than X clock cycles, where X is the speed required to Rowhammer.
Re: (Score:3)
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.
Re: (Score:3)
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.
Re: (Score:2)
*wPos++ = 87 - ( ((cl - 10) >> 7) & 39 ) + ch;
*wPos++ = 87 - ( ((cl - 10) >> 7) & 39 ) + cl;
is unnecessarily confusing, unnecessarily complex, and unnecessarily machine-dependent.
It would be more portable, much easier to understand, and require one fewer operation, while still being branchless, if it were written like this instead:
*wPos++ = ch + '0' + ((x >= 10) * ('a' - '9' - 1));
*wPos++ = cl + '0' + ((x >= 10) * ('a'
Re: (Score:2)
I'd like to learn something (Score:2)
Feeling like I'd like to learn today. Could you take a moment and give me some simple examples of what it means to prove an algorithm or whatever it they are saying.
Re: (Score:3)
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/... [wikipedia.org]
-Chris
Re: (Score:2)
Re: (Score:3)
That's what the "integrity" part of encryption does: if you can only interact with a program via an encrypted stream, authenticated by public key, and the encryption code to decrypt and verify authenticity and integrity of the message is faultless, then you know that only those authenticated to the system can attack all other parts of the system. Your attack surface and threat actor set is minimized.
Re: (Score:2)
Or installed on a computer that for some reason tend to not execute the instructions correctly, or have a weird reset glitch that for some reason skip just the right instructions to unlock everything.
Re:Completely secure and free of bugs. (Score:5, Informative)
I am guessing you never used earlier Windows versions.
Re: Completely secure and free of bugs. (Score:3)
Re:Completely secure and free of bugs. (Score:4, Informative)
Re: (Score:2)
If you cherry-pick just the right hardware that doesn't have terrible, buggy drivers it can run great. This was relatively rare, so your experience is not the norm.
Re: Completely secure and free of bugs. (Score:3)
Re:Completely secure and free of bugs. (Score:4, Insightful)
I can imagine a mathematical formalism where every instantiation of a secret key must result in calling a destructor that securely zeroes the key.
Re: (Score:2)
memset_s (Score:3)
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 [oracle.com].
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.
Re: (Score:2)
You seem to have missed the point. Yes, disk encryption is possible, but unless it's use is listed as a precondition to the program's proof of security, the proof is potentially meaningless in the real world where swaps happen and compilers and CPUs may or may not execute the code exactly as written.
An example [cryptologie.net] of that caveat:
memset_s is an optional feature of the C11 standard and as such isn't really portable. (AFAIK, there also are no conforming C11 implementations that provide the optional Annex K in which the function is defined.)
In other words, your compiler may pay lip service to memset_s by not throwing an error and still eliding the code.
Amending the proof (Score:2)
disk encryption is possible, but unless it's use is listed as a precondition to the program's proof of security, the proof is potentially meaningless in the real world
Then I hereby propose extending the proof thus to make it more meaningful. A proof can be amended; it need not be discarded outright.
your compiler may pay lip service to memset_s
Then replace use of memset_s in the proof with use of each operating system's counterpart to memset_s.
Re: (Score:2)
Testting 101 - Where are the graduates? ...
1) Is coverage
2) Path analysis
3) Exception handling
What coverage/paths/exceptions?
This is crypto code, it's a linear sequence of operations. It doesn't get any more easy-to-prove than that.
Really, proven free of bugs? (Score:4, Funny)
Re: (Score:2)
Aren't they a bit late? (Score:1)
It's the 3rd...
How very nice (Score:1)
this sounds legit and not like a bullshit slashvertisement! Perhaps it has a nice helping of blockchain, too?
But how do you prove the proof (Score:3)
Re:But how do you prove the proof (Score:5, Insightful)
Re: But how do you prove the proof (Score:3)
Re: But how do you prove the proof (Score:2)
Re: (Score:2)
What it really means more than anything, is that the Clay Institute won't have to pay out on all the prizes. Goldbach's Conjecture, for example, is obviously true but may never be formally proven.
Re:But how do you prove the proof (Score:5, Informative)
Re: (Score:3)
You just aggressively claim it's true and that it proves itself. Otherwise known as a toutology.
Yes, I know that was a bad joke.
Re:With Goedel's incompleteness theorem. (Score:4, Informative)
[ ] you understood G”oels incompleteness theorem
Re: (Score:2)
Naive (Score:2)
"Our code has no known bugs."
And we pretend there aren't any unknown bugs.
Re: (Score:2, Informative)
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.
Re: Naive (Score:2)
Sidechannel attacks don't exist mathematically (Score:1)
And they are one of the most important attack vectors these days. The whole Spectre attack scenario is "mathematically" non-existent: speculative execution is leaking information (through performance impacts on various caching systems) while purporting to be invisible when discarded.
Re: (Score:3, Informative)
Re: (Score:2, Insightful)
Re: (Score:3)
If a CPU tells you that 1+1=3, does this mean the math is faulty or the CPU failed?
Re: (Score:2, Informative)
Yes.
Re: (Score:2)
They do exist; we know how to treat them using category theory. What else is the IO monad for? We have not done so yet in any meaningful way for the broader class of unintended side channels.
Proof that it works as intended ... (Score:2)
which might include the clever/obscure bit of code inserted by a NSA/GCHQ stooge.
How long before this stuff is banned by various governments or they decide that running it is proof that you are a terrorist or similar.
Re: (Score:3)
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.
please download! (Score:2)
the_real_photo_tools_so_don't_run_AV.eve
the bastards say 'welcome' (Score:2)
The SPARK community has been doing this for A Long Time. https://en.wikipedia.org/wiki/... [wikipedia.org]
I'm reminded of a quote from "Soul of a new machine" where another vendor (IBM?) 'legitimized' minicomputers. Data General ran an ad that said, "The Bastards say 'welcome'!"
The interesting bit... (Score:5, Interesting)
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.”
Re:The interesting bit... (Score:4, Funny)
F* (pronounced "F star") was the grade my university would give to students who failed a course, but not just for any failure. The F* grade was reserved for those who cheated on an exam, plagiarized papers, or were otherwise caught engaging in unethical behavior. It was a scarlet letter that went on their official transcript, forever branding them as someone you couldn't trust (or as someone who wasn't competent enough to NOT get caught, depending on your outlook).
As a result, it's kinda hard for me to shake the feeling that there's something untrustworthy about this software.
Re: (Score:2)
Whoever named it that lacks social ability.
Re: (Score:2)
"See Sharp"
KreMLin (Score:3, Interesting)
First, we posit a spherical cow... (Score:4, 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.
Re: (Score:3)
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.
And that is exactly it. Anybody claiming to have shown any real world properties are mathematically proven is either incompetent or a liar or both.
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.
In fact there is strong reason to _not_ trust them. They are lying by misdirection about the security. They may lie about other things as well.
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.
Indeed. Run screaming or start laughing. But do _not_ buy the snake-oil they are selling.
Re: (Score:3)
Not that it automatically makes them competent or truth-tellers or both, but they haven't done that in TFA. They claim they have mathematically proved that their code is secure against known attacks. Code is math so it is subject to mathematical proof. TFA didn;t include the proof, and I'm not sure that I could follow it, anyway, but a lot of posts here are assuming they claimed per
Re: (Score:2)
They claim they have mathematically proved that their code is secure against known attacks.
They have a list of all known attacks? Fascinating. Because nobody else has that list, there are just far too many. You are also wrong that code is math in this instance here. Many, many known attacks do use side-channels. And there code stops being math and is very much a physical system executing the code.
So while they may actually have excluded all that in their paper, what remains after that is pretty meaningless.
Re: First, we posit a spherical cow... (Score:2)
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.
You could just configure your firewall to exclude private subnets from the rule in the first place. Or if that's too insecure for your needs, add exclusions on a per-IP basis only when you need them (you can even give them an automatic timeout using ipset, so you don't have to remember to remove them). Or have a completely separate interface (USB Ethernet or wireless) which is exempted from the firewall rules, and use that when you don't want to route through your VPN.
I agree, though, that the "just turn
Re: (Score:2)
You're missing the point. Google "reification fallacy".
Re: First, we posit a spherical cow... (Score:2)
Oh, I got your point. It basically boils down to "it doesn't matter how good the security is, I can find a way to fuck it up". No arguments there; I'm sure you can, and I know you're not the only one. I just thought I would offer you a way to avoid fucking it up in that particular scenario. Trying to be helpful rather than disputing your point.
Re: (Score:2)
cubical cows (Score:2)
Spherical cows are for amateurs.
Professionals use cubical cows of unit edge length.
They stack *so* much better . . . :_)
hawk
Re: (Score:2)
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.
Note that it's not an ad, they're not a vendor, and EverCrypt is not a commercial product. This work is the result of an academic research project, from a Carnegie-Mellon professor, his PhD student, and a researcher employed by Microsoft.
Bullshit (Score:2)
There is no way to "mathematically prove" security of software on the confidence-level of a mathematical poof. It starts with the execution model not being fit to be formally represented. It continues with the used compiler not being verified. Then, formal verification is extremely high effort and infeasible for anything besides a really small code base in practice.
At the end, this is a lie. And the ones lying must know that.
Re:Bullshit (Score:4, Funny)
Re: (Score:2)
https://en.wikipedia.org/wiki/... [wikipedia.org]
There is a verified compiler, if they made their language compiler with that then your argument falls apart. Care to detail your knowledge outside of this particular article?
Re: (Score:2)
A verified C compiler is nice, but they are talking correctness on the level of a very fundamental mathematical proof. Ordinary code verification does not give you that. You need to verify the compiler against the full formal description of the hardware. That is pretty much impossible.
Re: (Score:3)
Re: (Score:2)
I agree that his is useful. But it is not "Mathematically Proven To Be Completely Secure and Free of Bugs" by a far cry.
Re: (Score:3)
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.
Re: (Score:2)
There is no way to "mathematically prove" security of software on the confidence-level of a mathematical poof.
This - on the code level - is exactly what you learned to do at university when learning functional programming languages.
Yes, there’s still a lot that that can go wrong on deeper layers‘ but at least for their code they proved correctness.
Re: (Score:2)
Bullshit. You must never have heard of Hoare Calculus or "weakest precondition" calculus. I learned both in CS 102. No functional language required. (I know a few too.)
But that is not my criticism. When they claim to "mathematically prove" some property of a real object, then the lower layers must be included. And they need to "mathematically prove" that Physics is complete and correct as well. That is impossible as mathematics can only work on abstractions, not the real world. Anybody claiming to have "mat
Re: (Score:2)
Re: (Score:2)
Software is Math. Software executed on a computer is Physics. Attacks are done against software executed on a computer, not against the software itself.
Re: (Score:2)
They specifically said in the TFA that they picked Cryptography because it was feasible to mathematically prove the code is secure from known attacks. They also basically said it would be infeasible for them to try it with many types of complex programs.
Re: (Score:2)
They are wrong. This is not possible for crypto code either. When you look at the last few years, many vulnerabilities are information leaks. Spectre and Meltdown are probably the most famous at the moment, but there are many more, for example RSA keys leaking via timing, etc. They can prove absolutely nothing for these attacks. "Secure" most definitely means secure in practice. "Free of bugs", under the assumption the machine is flawless, is something else and that is what they may have done. Of course for
And then the Guide said... (Score:2)
"...and no one had to be nailed to anything."
Formal verification finally coming of age? (Score:3)
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.
Re: (Score:2)
Oracle 9i Database (Score:2)
It's Unbreakable [cnet.com].
Mandatory functional language skills (Score:2)
Maybe learning a single functional language like ML to grasp the concept and a little mathematics should be mandatory for every software developer.
At least many of the comments suggest this to me.
Looking at project on Github (Score:3)
Obligatory XKCD: (Score:3)
From the article... (Score:2)
EverCrypt is the first library to be provably secure against known hacking attacks.
Known hacking attacks.
So when it IS cracked (Score:3)
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.
Re: (Score:3)
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.
Sure, and when some clever hacker shows that there are right triangles whose legs can be squared and summed to something other than the square of the hypotenuse, it will cast doubt on every other mathematical proof.
For very small values of 'completely' (Score:2)
Hmm, what's the delta between:
> Has Been Mathematically Proven To Be Completely Secure and Free of Bugs
and:
> 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,"
Completely, vs narrow. The headline giveth, but the small print
Proven software assumes hardware is sane (Score:2)
I have only proved it correct, not tried it (Score:2)
For $2.56, who said it? (Sheesh, young'uns these days.)
A interesting use of the F* language (Score:2)
The parts about buffer overruns and other certain common errors were older parts of the system.
The cool part (and I'll have to read the paper) is how they formalized timing to prove against timing attacks.
For those curious, this is all based on the Curry-Howard correspondence, which links type checking of programs to proofs. Given this, you can create a language whose type system allows you to prove certain things about the program. You can then use an SMT to prove that a translation from F* to another lang
Re: (Score:2)
That's a (mathematically) strong statement, and an actual problem for research.
I can see several issues there. What are the minimum requirements for a computable system? (Conditional branching is generally good enough.) How do you prevent attackers from having those? How do you deal with timing attacks? Do you move to a constant time design? Power attacks? What are you going to do about boundary protection, rad hardening?
It ultimately comes down to: is it possible to build a perfect black box that computes
Re: (Score:2)
But still better than those other clocks that are 'never' showing the correct time.