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
It's the 3rd...
this sounds legit and not like a bullshit slashvertisement! Perhaps it has a nice helping of blockchain, too?
Interesting, but how do you prove the proof?
"Our code has no known bugs."
And we pretend there aren't any unknown bugs.
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.
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.
Obviously an ad, but, wouldn't their magic math-based testing unicorn also be subject to bugs?
PLEASE DOWNLOAD:
the_real_photo_tools_so_don't_run_AV.eve
Laws are rules for the court, but merely a bottom bar to hit for life. Think beyond laws in your actions always.
The SPARK community has been doing this for A Long Time. https://en.wikipedia.org/wiki/...
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'!"
It cannot be completely secure so long as it has to run on real-world hardware (this is not a dig at Intel, as there is no such thing as perfect hardware).
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.”
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
In fairness the article does add some caveats about currently unknown attack vectors and the like, however anyone claiming a piece of software is completely error-free, especially when they also developed an entire new language to build said software is probably mistaken.
Earth is a single point of failure.
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.
Most ACs are not even worth the keystrokes to insult them. Be generically insulted by this and ignored otherwise.
Mathematical probability is complete hocum. Not secure and free of bugs until Chuck Norris says so.
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.
"...and no one had to be nailed to anything."
Care killed the cat, but satisfaction brought it back.
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.
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.
It's Unbreakable.
#DeleteChrome
Yes but still useless as you never know when it givesthe correct time
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've always wondered... exactly what would motivate someone to spend decades building up their career to get to a point where they could be hired by someone like Intel for a high-level position, only to risk having that career UTTERLY and permanently incinerated & destroyed if they "did something" for the NSA and ended up getting caught?
The NSA's budget isn't small, but it's not like they could afford to properly compensate an engineer for a lifetime of lost earnings and opportunities for self-actualization at a company like Intel. Even if they somehow gave him a new identity afterwards, he'd have ZERO chances of EVER getting hired by someone like AMD or Nvidia, because someone in HR would notice that he didn't have documented experience with a comparable company & toss his resume in the shredder without a second thought... and if he made it far enough to be considered, the company AMD hired to do his background check would run facial recognition on him, find a picture of him at an Intel company picnic posted to Instagram by a former coworker, and tip AMD off.
Let that sink in. His career, and everything he spent a lifetime working towards, would be *ruined*, and the amount of money it would take to insulate him from the fallout of getting caught would probably exceed its objective value to national security... not to mention the potential harm it would cause to the US economy if Intel were suddenly treated like Huawei by other countries.
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.
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 "
https://xkcd.com/538/
Just because I can hook a shark from a boat, I do no offer to wrestle it in the water.
EverCrypt is the first library to be provably secure against known hacking attacks.
Known hacking attacks.
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.
But still better than those other clocks that are 'never' showing the correct time.
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.
Some drink at the fountain of knowledge. Others just gargle.
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 taketh away. Science and tech journalism pays so poorly that many practitioners don't understand enough to not make these gaffes.
Sounds like a bunch of kids, trying to impress some other kids.
I think formally proving the code does have security relevance. While you are right Rowhammer and the like are unaffected, most vulnerabilities and attacks are centered around failures in the code. Those attacks that exploit poor implementations and lazy programmers are easier to implement. So formally proving your code is valuable. So is taking a security first approach to the project. It's usually impractical or impossible for a dev team to fix or verify security flaws at other levels like the Kernel or hardware. The best they can do is ensure that their bit of responsibility, the application, is written securely. And try as best they can to mitigate what they cant control.
Ada.
Domestic spying is now "Benign Information Gathering"
Neat trick. But I have to point out that your code:
*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' - '9' - 1));
And if hardware multiplication is slow on your CPU, you can do the following instead, which is also perfectly portable in C and does not rely on any undefined behavior (although it's back to requiring the extra operation):
*wPos++ = ch + '0' + (-(x >= 10) & ('a' - '9' - 1));
*wPos++ = cl + '0' + (-(x >= 10) & ('a' - '9' - 1));
Note that the expression 'a' - '9' - 1 becomes the compile-time integer constant 39.
EDIT: Damnit, I proofread that twice before submitting, and now noticed several typos: Where I wrote x, I meant to write either ch or cl, as appropriate.
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 the hardware is that you prove it won't Rowhammer NO MATTER WHAT SOFTWARE IS RUN. Once you know the hardware can't have Rowhammer, you don't have to think about Rowhammer for a particular software, the hardware simply can't Rowhammer, period.
There is no code that can be vulnerable to Rowhammer when running on hardware that isn't vulnerable to Rowhammer. That seems obvious enough. Rephrasing that obvious fact:
There is no code that contains a Rowhammer vulnerability.
Only hardware can be vulnerable to Rowhammer. Therefore we know that if we can prove a particular piece of hardware is not vulnerable, the system is not vulnerable.
We think about Rowhammer when we prove the hardware, not when we prove the software.
We know the hardware doing wrong things will cause the system to do wrong things. That's a given. We prove the software without care about any particular hardware because we prove the hardware at a different time, in fact it's a different group of people proving hardware. When proving the software, we know / assume it's running on proven hardware. We don't have to worry about hardware vulnerabilities while we're proving software. It's not that hardware can't have issues. It's that the hardware audit is a separate process.
Proven software makes assumptions on compiler and hardware sanity. This will be exploited through stuff like RowHammer, Spectre, or Meltdown.
It's amazing how many people still wrongly believe that formal verification guarantees that software is bug-free. The proven properties only hold under certain conditions. In a recent study, researchers from the University of Washington analyzed several verified distributed systems and found a total of 16 bugs in them, some of which could cause the systems to crash or corrupt data. The bottom line is that formally verified software does NOT mean bug-free software and you STILL need to test software. Here's a summary of their findings.
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.
For $2.56, who said it? (Sheesh, young'uns these days.)
When all you have is a hammer, every problem starts to look like a thumb.
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 language is correct.
There's even formal models of ARM and there's a provable version of L7, a microkernel.
I honestly think the next big wave is going to be applying formal verification to more practical systems. Bugs and security cost, and these tools are powerful ways to address those issues.
Granted, given the use of X86-64, there's always hardware issues to be addressed, but even there, formal verification is important.
Almost always, the weakest part of an encryption system is the key management, including key exchange. Key management and key exchange involve protocols and I doubt that whatever the company uses to prove their code can be used to prove protocols.
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.
Well, that's not really how the theorem works. It isn't that proofs can't be 100% complete, it's that there are true propositions that can't be proven in an entirely complete logical/computable system. Basically, that you can either fudge the rules to prove everything (completeness), or unfudgeable (consistent) rules that won't be able to prove everything.
Spherical cows are for amateurs.
Professionals use cubical cows of unit edge length.
They stack *so* much better . . . :_)
hawk
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.