71–80 of 96 posts
I wonder if Windows 7 will get this on its end of support day tomorrow.
It would be remarkably convenient if Microsoft, having turned off support for Windows 7 and advocated an upgrade to Windows 10 that a lot of the hold-outs don't want because of the user-hostile changes, then mysteriously discovered a serious security flaw within hours of the cut-off. The optics would be terrible.
Ah! - does this explain the weirdly specific message that came out from GCHQ last week? https://www.telegraph.co.uk/news/2020/01/12/gchq-warns-not-u...
Ah! - does this explain the weirdly specific message that came out from GCHQ last week? https://www.telegraph.co.uk/news/2020/01/12/gchq-warns-not-u...
Not sure if related. Support ended, so it's a good recommendation whether some new attack is revealed or not. Especially when new patch for a newer version can reveal unpatched issues in older versions. What do you think is oddly-specific about it?
Earlier quoted context omitted.
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…
One might hope you have a formal spec of a cryptographic library.
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.
It's part of their mission. Back in the day they helped make DES stronger against differential cryptanalysis, which was unknown at the time.
Modern NSA is more Black Hat than white Hat sadly
I wonder if Windows 7 will get this on its end of support day tomorrow.
The reason they won't support they systems forever is the cost of doing so (and of course they want people to upgrade), but the cost of fixing a really bad security issue in an otherwise unsupported system every other year is probably fine.
Earlier quoted context omitted.
One might hope you have a formal spec of a cryptographic library.
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…
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.
It'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…
That doesn’t mean that properly validating code so it at least doesn’t overflow its buffers is useless of course.
It's an "airtight hatchway", guys!
It'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…
https://www.irif.fr/~sozeau/research/publications/drafts/Coq...