Do I understand it right that the implication is that NSA helped find or patch bugs in MS crypto libraries? If so that's incredibly useful.
That has been confirmed this morning in the linked article.
Cryptic Rumblings Ahead of First 2020 Patch Tuesday
81–90 of 96 posts
Re: Cryptic Rumblings Ahead of First 2020 Patch Tuesday
#82It's a shame that mathematically proving correctness of code, even for extremely important code , is never done. I wonder how many lines of code in crypt32.dll. Is it on the order of 7500 lines? If Microsoft spent a few man-years mathematically proving the correctness of that code, they could have the saved the world about 10,000 man-years. Windows has a user base of 1 billion[1]. A ballpark figure for proving the co…
Define "proving correctness". Proving that it does what it's supposed to? You need a formal spec as the starting point for that; how do you prove that the formal spec correctly describes what the software's supposed to do? Proving that it has no bugs? That only works for the kinds of bugs covered by the proof. Your proof that it has no null pointer crashes tells us nothing about whether it has off-by-one errors. For…
> For each kind of bug, you need a different proof.
Not necessarily; if your definition of security and correctness is sufficiently general and if you can prove that your program conforms to those definitions, you have effectively proven your program to be secure and correct for all bugs. Unless of course your definition of security and correctness was too narrow, which as you note is where the crux of the problem is.
But this is not a hopeless task, there is a lot of active research in building axiomatic definitions of what security and correctness mean, so in theory it could be possible to prove a program 100% correct if the axioms are self-evident.
Re: Cryptic Rumblings Ahead of First 2020 Patch Tuesday
#83It's a shame that mathematically proving correctness of code, even for extremely important code , is never done. I wonder how many lines of code in crypt32.dll. Is it on the order of 7500 lines? If Microsoft spent a few man-years mathematically proving the correctness of that code, they could have the saved the world about 10,000 man-years. Windows has a user base of 1 billion[1]. A ballpark figure for proving the co…
Note that even if you prove correctness of code, there still might be bugs in the compiler, so you will have to prove the compiler. Then there could be bugs in the modules / DLLs / dependencies in the OS, so more proving needs to be done. Then there might be bugs in the CPU. So it's not so easy. T hen there are things which you simply can't prove, eg. In crypto the code may be correct, yet it may still leak some side…
I suppose that with enough time and attention one could build a proof system that accounts for things like Rowhammer and timing attacks but are we even anywhere close to that right now?
The only time anyone wrote a mechanical proof for my code, I was still finding security bugs a year later. One in particular stands out.
(note to bosses: never, ever ask the security guy "what's the worst that could happen?" the worst that could happen is always along the lines of "we go out of business and you go to jail", maybe add on "people could die," depending on domain. "How bad is this?" will get you more coherent answers)
Re: Cryptic Rumblings Ahead of First 2020 Patch Tuesday
#84Earlier quoted context omitted.
While proving code matches a spec is very helpful, it's only as helpful as the spec being "correct" from a "does what we want it to do" angle. For example, you could do a bunch of spec proving on CPUs, but you wouldn't catch something like Spectre if your definition of correctness didn't include "no information leakage can happen through timings on branch prediction". And even then! You need to have the right definit…
>but you wouldn't catch something like Spectre i I don't think software should prove that some CPU from the future will have shortcuts that leak information, CPU guys should prove their hardware is also safe.
Sure, but I believe the point was that e.g. timing attacks might not be part of your proof but still be a real threat.
Re: Cryptic Rumblings Ahead of First 2020 Patch Tuesday
#85Earlier quoted context omitted.
Note that even if you prove correctness of code, there still might be bugs in the compiler, so you will have to prove the compiler. Then there could be bugs in the modules / DLLs / dependencies in the OS, so more proving needs to be done. Then there might be bugs in the CPU. So it's not so easy. T hen there are things which you simply can't prove, eg. In crypto the code may be correct, yet it may still leak some side…
The goal isn’t to deliver a provably correct system - that’s effectively impossible. But if core OS features or APIs (like the network stack) can be written in a theorem-proving language, huge benefits can be realized — the attack surface can be vastly reduced.
People will just go around.
I find it hard to resist making a comment in those movies set in New York City where a character has a steel jacketed door and a million locks but I bet the wall is cheap gypsum board and studs on 18 inch centers. You could steal a lot of stuff around a door without even compromising the building structure. You just need the right sheet rock knife and a quiet hallway.
Someone told me about Microsoft having a data center in a leased building, and they had the forethought to fill the space above the false ceiling with motion sensors to prevent someone just getting a ladder and going over the top of the walls. People don't always think about these things.
If you have a model that works for certain patterns, people will begin to ask what situations it can't handle. The attacks will move to that space. They may even look at release notes and try things that were reported as fixed, similar to the way people are now doing analysis on updates for operating systems.
Will it keep lazy criminals out? Yes. But they're not all lazy.
Where it's more likely to help is that you'll find crashing bugs you may have missed, and you save some face by not having particularly naive bugs in your code. That alone may be worth the cost of entry. But it's 'safer', not 'safe'.
Re: Cryptic Rumblings Ahead of First 2020 Patch Tuesday
#86Earlier quoted context omitted.
It's part of their mission. Back in the day they helped make DES stronger against differential cryptanalysis, which was unknown at the time.
When they feel like, most of the time however they hold back vunerablities so they can exploit them for their own purposes. Modern NSA is more Black Hat than white Hat sadly
>When they feel like, most of the time however they hold back vunerablities so they can exploit them for their own purposes.
You have no idea if that's true or not. It's probably true, but neither of us have the information required to assert our opinions on the matter as fact.
Re: Cryptic Rumblings Ahead of First 2020 Patch Tuesday
#87It's a shame that mathematically proving correctness of code, even for extremely important code , is never done. I wonder how many lines of code in crypt32.dll. Is it on the order of 7500 lines? If Microsoft spent a few man-years mathematically proving the correctness of that code, they could have the saved the world about 10,000 man-years. Windows has a user base of 1 billion[1]. A ballpark figure for proving the co…
> If Microsoft spent a few man-years mathematically proving the correctness of that code, they could have the saved the world about 10,000 man-years.
Formal verification takes a tremendous amount of skill and effort. The most impressive formally verified operating system we have today is seL4, as you mentioned. Its functionality is very limited, though.
> A ballpark figure for proving the correctness of 7500 lines of very complex code[2] is about 30 man years[3]. If even 1% of the 1 billion Windows users and sysadmins has to spend a couple hours on things related to this patch, it works out to 9615 man-years of worldwide waste (based on an 8 hour workday and 260 workdays a year).
1. I doubt this idea is practical
2. Assuming it's possible, the cost would be enormous
3. The resulting system would likely be hard to change without breaking its formal guarantees
4. Microsoft would have to justify this cost on their own terms. If the code is already 'stable enough', they would do better to spend that money developing other features. Which of course they did.
> 100 per cent bug-free and therefore immune to crashes and failures
seL4 are careful to state that it does not offer guarantees against timing-attacks or other side-channel attacks.
Re: Cryptic Rumblings Ahead of First 2020 Patch Tuesday
#88It's a shame that mathematically proving correctness of code, even for extremely important code , is never done. I wonder how many lines of code in crypt32.dll. Is it on the order of 7500 lines? If Microsoft spent a few man-years mathematically proving the correctness of that code, they could have the saved the world about 10,000 man-years. Windows has a user base of 1 billion[1]. A ballpark figure for proving the co…
Define "proving correctness". Proving that it does what it's supposed to? You need a formal spec as the starting point for that; how do you prove that the formal spec correctly describes what the software's supposed to do? Proving that it has no bugs? That only works for the kinds of bugs covered by the proof. Your proof that it has no null pointer crashes tells us nothing about whether it has off-by-one errors. For…
> how do you prove that the formal spec correctly describes what the software's supposed to do?
This is a valid point. With formal verification, the buck stops with the model. Looking at existing projects like Sel4, though, it's clearly not a knock-down argument against formal methods.
> Your proof that it has no null pointer crashes tells us nothing about whether it has off-by-one errors. For each kind of bug, you need a different proof. Did your proof cover every category of bug? Almost certainly not.
This appears to be a guess at how formal methods work. It is wrong.
Formal methods are able to take an abstract model and 'refine' it into an executable program that implements the formal model. [0] This process is mathematically watertight (ideally at least). There is no room for language-specific bugs (such as buffer overflows) to creep in.
What you don't tend to get from formal methods, is a guarantee against side-channel attacks, such as timing-based attacks. This may be a real security concern. From a quick google search, this seems to be an active area of research.
Re: Cryptic Rumblings Ahead of First 2020 Patch Tuesday
#89It's a shame that mathematically proving correctness of code, even for extremely important code , is never done. I wonder how many lines of code in crypt32.dll. Is it on the order of 7500 lines? If Microsoft spent a few man-years mathematically proving the correctness of that code, they could have the saved the world about 10,000 man-years. Windows has a user base of 1 billion[1]. A ballpark figure for proving the co…
Note that even if you prove correctness of code, there still might be bugs in the compiler, so you will have to prove the compiler. Then there could be bugs in the modules / DLLs / dependencies in the OS, so more proving needs to be done. Then there might be bugs in the CPU. So it's not so easy. T hen there are things which you simply can't prove, eg. In crypto the code may be correct, yet it may still leak some side…
> you will have to prove the compiler
Strictly speaking you don't - that's one of two approaches. Fortunately, the CompCert compiler already exists if you want to go the route you describe.
The alternative to use a non-verified compiler, but verify that the generated code corresponds to the model. This is the route the seL4 project took. They used GCC, but verified the correctness of the code it generated.
Re: Cryptic Rumblings Ahead of First 2020 Patch Tuesday
#90Earlier quoted context omitted.
The goal isn’t to deliver a provably correct system - that’s effectively impossible. But if core OS features or APIs (like the network stack) can be written in a theorem-proving language, huge benefits can be realized — the attack surface can be vastly reduced.
People will just go around. I find it hard to resist making a comment in those movies set in New York City where a character has a steel jacketed door and a million locks but I bet the wall is cheap gypsum board and studs on 18 inch centers. You could steal a lot of stuff around a door without even compromising the building structure. You just need the right sheet rock knife and a quiet hallway. Someone told me about…
> Where it's more likely to help is that you'll find crashing bugs you may have missed, and you save some face by not having particularly naive bugs in your code.
That doesn't sound right at all. Systems with atrocious security are more likely to be compromised than systems with good but imperfect security. Attackers do not have infinite resources.