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.
The link to the article indicates the story was posted on April 2nd. I think this article was accidentally posted a day late.
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.
April 1st called. It wants its story about bug-free, invulnerable security back.
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?
just saying
Haha April fools!
Oh, I'm sorry, I thought you meant "disprove".
That't the problem with "100% complete proof" in mathematics.
*IN* mathematics. Not in reality!
Mathematics itself would first require 100% complete proof in the real world. Which Kurt Goedel showe to be completely impossible.
Mathematics is a useful tool, IF the constructs can offer statisticalle reliable predictions of reality.
But if not, then it's no better than religion or other beliefs. Not wrong, but merely reliably useless.
The same thing is true for philosophy, by the way. It's also crossing the division between science and religion.
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.”
A broken clock is 100% accurate if you look at it at the right time day.
Because mathematics is only as correct as the unproven axioms and merely arbitrary definitions it is built upon.
Goedel's incompleteness theorem was the ultimate death blow to the hopes of perfectly proving mathematics itself.
So the best you can ever have, is statistically reliable reproducible measurements. Preferably reproduced by you personally.
Don't get me wrong: Mathematics can be great and certainly is extremery useful.
But it is not itself defining itself as useful. Reliably predicting reality is what makes it useful.
And like with philosophy, there is a whole world of mathatics out there that is right on, and often way over the line between dabbling to find things that will be useful in the future, and merely self-made-up arbitraty constructs that are as reliably useless as religion.
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.
... Hold my beer.
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.
Shouldn't the headline be "P != NP". I'm pretty sure it's required to prove that encryption works.
"...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
Very good & it's what spooks me when I 'stick my neck out there' like THIS https://science.slashdot.org/c... - how SOLID/SAFE is the underlying compiler code (& I tend to 'steer clear' of 3rd party libs/dlls OR units (.pas), modules (.bas) & headers (.h)).
* IF you can't write the code YOURSELF & verify it, yourself? You need to as best as is possible - the rest, users will uncover/determine. For my hosts engine?
I chose Object Pascal because it outright SMOKED MSVC++ in years past (especially in MATH & STRINGS + has NO ISSUE in string related bufferoverflows C/C++ can (latter can avoid via std string use, copied from PASCAL having len in str OR check @ least prior)).
HOWEVER: "verified design" is a RARE thing (even for compilers & IT SHOULD BE there most of all - they create all else).
(I don't know if they're "lying" but they ARE taking a hell of a RISK of "EATING THEIR WORDS" given time...)
APK
P.S.=> See subject & nice post gweihir + see what I had to do to an UNIDENTIFIABLE LYING TROLL here (NSA 'Ghidra' bs artist who shot his piehole off & couldn't BACK it validly w/ proof https://games.slashdot.org/com... ) in ADDITION to what's in my initial link... apk
I thought April Foo's Day was 3 days ago?
They created a custom compiler for this. That could easily introduce bugs if it isn't formally proven...
This story clearly should have been released on Monday.
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...
I had to check the date for an obvious April Fool relationship.
Any sufficiently complicated software system *CANNOT* be proven correct, and the fundemental reason so has to do with the fact that you are USING THE SYSTEM UNDER TEST, to test itself. These computer scientists should know this. I bet their grant or whatever funding source they were working under sure wanted this result, and hey, it paid the eggheads bills for parties and wine for a while, but I hope the rest of us realize the truth... there will always be bugs.
AND.. who the hell creates a new programming language and calls it ONLY 'F*'?! why not get serious here and call it F*314159 or any other transcendental function reference?
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.
The Supreme court in the United States is going to love this:
“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.”
We have been arguing for years that all software could be reduced to mathematical expressions - which are not patentable. Math is discovered, not invented.
Their code is based on assumptions, any one of which may be incorrect.
Incorrect assumption invalidates their claims.
Crypto library code is very linear, no conditionals,
Why stop at crypto code? It's possible to avoid branching statements for most logic. Here I avoid a lookup table & branching to eliminate branch prediction vulns (spectre / meltdown) in a bin2hex function:
// Convert each byte of the input array into two hexadecimal digits: [0..9a..f]
void * while_jump = &&BinToHex_WHILE;
void * while_finish = &&BinToHex_WHILE_FIN;
sintp_t while_mask = -1;
goto BinToHex_WHILE_TEST
BinToHex_WHILE:
cl_sint8 ch = *rPos++;
cl_sint8 cl = ch & 0xFU;
ch = (cl_uint8)ch >> 4;
*wPos++ = 87 - ( ((ch - 10) >> 7) & 39 ) + ch;
*wPos++ = 87 - ( ((cl - 10) >> 7) & 39 ) + cl;
BinToHex_WHILE_TEST:
rPos - end;
while_mask >>= (sizeof( sintp_t ) << 3) - 1;
while_jump = (while_jump & while_mask) | (while_finish & (~while_mask);
goto while_jump;
BinToHex_WHILE_FIN:
Note that I have also (somewhat defensively / needlessly) avoided a while loop branches by use of the computed goto. This code must not be placed in memory with the highest bits set. (addr 0x8000000000000000 and above in 64bit); However, by emulating a carry-out operation I could also make it placeable anywhere in memory (but the example would have been even more obtuse). This relies on C (not C++) ability to predictably use the result of an integer overflow on a machine using two's compliment, but a carry-out operation could have also been used to avoid use of the overflowed integer for implementation in C++ etc.
TL;DR: Branching statements = branch prediction side channel. GOTO has always been our sacrificial savoir!
Oops, HTML escapes ate a bit of code, but it should still suffice for demonstration of the theory...
EverCrypt is the first library to be provably secure against known hacking attacks.
Known hacking attacks.
I'll expand on that further (OS & API - were THEY also verified? Probably not & your compilers CALL ON THOSE too) in addition to my reply to gweihir https://science.slashdot.org/c... regarding compiler code as well which YOU hit on also (great minds think alike).
* ONLY OS I've ever heard of that was iirc is HP-UX @ a B rating?
(Correct me if I'm off/wrong - it's been YEARS since I looked @ "Orange Book" C2 certified or better ratings... & iirc, they use a diff. std. now too there...)
APK
P.S.=> Anyhow there ya go "onwards & UPWARDS"... apk
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.
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.
You lack imagination young padawan.
how can you prove that side channels in the code itself? Are you talking source? Compiled?
Formal proofs are about the correctness of the code -- does it do exactly and only as specified -- and say absolutely *nothing* about security. You can have absolutely, formally proven correct code with side channel attacks. Row hammer laughs at your formal proof. The attack on PGP utilizing known plain text and a microphone as found on a smartphone to expose the private key: no formal proof can defend against that.
In your last paragraph you start trying to use physical specifications for "proof" and your example illustrates that you have no experience with actual side channel attacks. Many side channel attacks work specifically because it was a side channel not considered by the designer and so was not part of the specification to start with.
Again, a proof of "meets specification" is only what it is, a proof that the specification was accurately and completely followed. It does nothing for security. For that you need to look to your specification. And hope that you've conceived of all the inconceivables (like a bog standard microphone being a viable exploit for an audio side channel relating to CPU operations).
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"
Challenge accepted!
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.
Oops: -(x >= 10) invokes a check of the CPU (carry) flags, which is what the GP was trying to avoid. If The CPU may (probably) trigger parallel (speculative) execution and evaluate both x >= 10 and x < 10, which is what allows Spectre vuln to do mean stuff. It's probably the case that code would be somewhat processor specific to avoid processor specific vulnerabilities. On the Z80 we don't have any spectre or meltdown vulnerabilities, for example, and simple if statements and lookup tables would not result in the vulns since it has no parallel (speculative) execution. The Mill CPU would also be invulnerable to certain Spectre variants.
Note that the expression 'a' - '9' - 1 becomes the compile-time integer constant 39.
Only if the underlying charset the compiler is build for is based on ASCII, but there's no guarantee of that. Today's code should specify the charset operated within and explicitly emit or accept ASCII / UTF-8 or Unicode use in functions to use a standard representation internally, independent of the compiler's host charset. Perform translation into the target environment's charset upon display.
That way your BBS code can run on multiple platforms while using a common charset interchange. Also, you don't have to track down charset related bugs because logic changed when you compiled on C64 petscii vs IBM P2 CP437. C takes the opposite approach, its source code files must be translated into the host environment that the compiler is compiled against, and makes no effort to standardize a charset's values so that the C compiler can run on any platform no matter the char layout. However, for code that will be writing/reading data files to/from other machines possibly over a network, you don't want to let C decide what layout the characters will have. That isn't the world we live in today, we're working towards having everything (except slashdot) be Unicode compliant.
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.
The implication is that all other crypto security is not secure. This is a straight up ploy to try to gain a large user base quickly. The fact that they make such a claim should land them in court cases for fraud when they get proven false, and that will just be a matter of time. In marketing terms, they will find a way to spin it as not their fault, but this is straight up marketing.
Yesss! Hmm. Hmm?!
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 only proven unbreakable cipher is the one-time pad. Anything deterministic (run on a computer) can, with enough time and computing power, be broken. One-time pads depend on having a key made of truly (not pseudo-) random data. So have they really just created a one-time pad system that uses provably correct software? How are they generating their pads? How are they ensuring that they're used only once and completely destroyed after that?
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.
Spherical cows are for amateurs.
Professionals use cubical cows of unit edge length.
They stack *so* much better . . . :_)
hawk
Academics and mathematicians love this stuff but they are wrong.
I don't care what the math says. The history of this business is that there will always be bugs and there will always be security holes. Always. And lots of them! Hasn't anyone been paying attention?!
Look, I know that certain techniques, languages, and diligence can produce higher quality code. This industry has done it several times and places. However even in those pockets of high quality, are you comfortable saying there were no bugs? No security exploits? The software was perfect?
This quest reeks of trying to find and use some technical methodology. The trouble is, our methodologies get overruled by politics, money, management, human foibles, and competing priorities. Technical means can only get you so far. The rest is the human condition. We produce our tech with humans, we sell with humans, and humans are our customers.
The most powerful thing you can do to ensure quality and security is to create a culture and a value proposition that depends on that. Make it so good quality gets managers their bonuses. Make it so that sales depend upon good security. Do that and the rest will follow.
When you start with the technical means, you are getting the motivations wrong (by implying that motivations don't matter). And thus you started with the wrong thing.
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.
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.
LoL.
Kerckhoffs's principle => If the code you are using is unsecure by design the code owner always owns you too, as he wish. If it is open source code, at least you can read it for yourself and immediately follows why not trying to proove it and to programatically check if it is the grail of the open source philosophy itself ?
https://en.wikipedia.org/wiki/Kerckhoffs%27s_principle
For ex I use Firefox and I don't trust it because I will never read its code myself. There is a community saying you can use Firefox because it may hold 5 minutes if an hacker targets you and the other browsers are worst. Its okay because I dont specialy trust people I randomly talk to in the street either but I trust there is a shared etiquette in the city that you won't be targeted in the 5 minutes after arrival.
The article says that the next step is to proove TLS (https) and implement it. I won't really trust the prooven TLS because I cant use EverCrypt. But it is like a public declaration that the CCTV on the streets cannot be tampered by policemen themselves and the videos are write only on a SSD datacenter.
So we are dumb and we cant read the code nor use EverCryt or Coq or Isabelle but we have the defeasible understanding that a prooven TLS will be trustable.
https://en.wikipedia.org/wiki/Defeasible_reasoning
And by the way when I take a plane I assume the theories that Vasco de Gama circled Earth by sail and that Newton's law F= G.m1.m2/r2 holds the plane from being lost in space and the pressure difference on the wings makes the plan fly, without performing ANY experiment before buying the ticket.
So I trust math, even horribly complicated math I will never check. It a bias for Descartes' math demon but I dont specially have trust in the existence of demons even if my Intel CPU based random generator lurks, waiting me to use a crypto software.
https://en.wikipedia.org/wiki/Evil_demon
Of course we are dumb anonymous cowards but researcher always experiment their proofs :
https://www.quantamagazine.org/formal-verification-creates-hacker-proof-code-20160920/