Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Cryptic Rumblings Ahead of First 2020 Patch Tuesday

krebsonsecurity.com

Post reply on HN
Print view View original

31–40 of 96 posts

Re: Cryptic Rumblings Ahead of First 2020 Patch Tuesday

#31

Post by thephyber »

r00fus wrote: post #22
computator wrote: post #15

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…

> 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. But how much more profitable could it have been? Is it possible Microsoft makes more money by not doing it? We cannot expect companies to behave in the greater population's best interest unless there is some reward/punishment structure in place. Enter regulation.

Lots of people in this thread are complaining that a formal proof is not reasonable and will not catch all classes of errors.

I think r00fus is right to look at the profit motive of the software supplier. Microsoft would have been climbing a steep curve of diminishing returns for basically no extra revenue.

Windows isn’t the monster revenue generator and in the server space it’s losing to free Operating Systems.

We ask for perfect security but we as an industry/market aren’t willing to pay the premium to go from “it mostly does what I want most of the time” to “life critical with near perfect security”.

That said, I don’t think regulation would work here and I suspect there would be a perverted incentive by the regulator if an issue was found (like in this case where government, military, and critical industry get early access to the fix).

Re: Cryptic Rumblings Ahead of First 2020 Patch Tuesday

#33

Post by TimTheTinker »

bouncycastle wrote: post #28
computator wrote: post #15

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…

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.

Re: Cryptic Rumblings Ahead of First 2020 Patch Tuesday

#34

Post by magicalhippo »

jimbob45 wrote: post #25
asdfasgasdgasdg wrote: post #24

Earlier quoted context omitted.

What does it mean to prove the correctness of code like this. For example, is it possible to prove that no side channel attack exists in a function or library? What form does such a proof take? How do you express, mathematically, that no disclosure of data is possible in response to arbitrary requests and function calls? Are there any recent major vulnerabilities that would have been prevented if the code had been fo…

Well, to start, if you write pure functional code, then you can reason about the code without having to worry about side effects. EDIT: As a starting point. Pure functional programming is one tool among the many in your toolbox. It should not be anyone's entire strategy.

Side effects != side channels.

Side channel is stuff like your multiplication code takes different amounts of time depending on the arguments, or your cache hit/miss patterns depend on arguments and thus can leak the argument.

Re: Cryptic Rumblings Ahead of First 2020 Patch Tuesday

#35

Post by mcguire »

polemic wrote: post #26
jimbob45 wrote: post #25

Earlier quoted context omitted.

Well, to start, if you write pure functional code, then you can reason about the code without having to worry about side effects. EDIT: As a starting point. Pure functional programming is one tool among the many in your toolbox. It should not be anyone's entire strategy.

Bold assertion in the face of side channel and timing attacks.

Is crypt32 supposed to be secure against side channel and timing attacks?

Re: Cryptic Rumblings Ahead of First 2020 Patch Tuesday

#36

Post by mcguire »

AnimalMuppet wrote: post #29
computator wrote: post #15

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…

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.

Re: Cryptic Rumblings Ahead of First 2020 Patch Tuesday

#37

Post by gpm »

bob1029 wrote: post #23
cjbprime wrote: post #9

Earlier quoted context omitted.

Wait, how do you know it's not an RCE? Memory safety flaws in a DLL become RCE all the time. > is there a way to turn a spoofed certificate into a single-click pwn? e.g. The victim clicks on a link to go to your website, their machine wants to validate the TLS cert you sent it, it calls into crypt32.dll to do that, it corrupts memory while handling your attacking cert, pwn? We don't know enough (anything!) about the…

This would be a terrifying outcome if certificate-based RCE. Imagine an actor like google running an intentionally-compromised TLS certificate on their web servers... perhaps even targeted at specific IP addresses or on certain schedules to avoid detection. Certificates are an excellent initiation vector too. Especially, if one wanted to intentionally present a backdoor like this for national security reasons (all of…

I'd more more worried about either hacked sites, or a country with something like China's Great Cannon doing that than a legitimate US company like Google.

Google doing that would be a great way for everyone involved to spend a long time in jail.

Re: Cryptic Rumblings Ahead of First 2020 Patch Tuesday

#38

Post by gruturo »

jorblumesea wrote: post #32

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.

Re: Cryptic Rumblings Ahead of First 2020 Patch Tuesday

#39

Post by tialaramex »

cjbprime wrote: post #9
AaronFriel wrote: post #2

Scary, but not an RCE so threat is limited. It would mean malicious actors could possible create spoofed signatures on malware or possibly websites (EV certificates?). Am I missing something or is there a way to turn a spoofed certificate into a single-click pwn? As I understand it, users would have to download a malicious payload or click a malicious URL to be exposed. Edit: People are asking why I assume it's not a…

Wait, how do you know it's not an RCE? Memory safety flaws in a DLL become RCE all the time. > is there a way to turn a spoofed certificate into a single-click pwn? e.g. The victim clicks on a link to go to your website, their machine wants to validate the TLS cert you sent it, it calls into crypt32.dll to do that, it corrupts memory while handling your attacking cert, pwn? We don't know enough (anything!) about the…

Certificates in the Web PKI (so they'd be trusted) aren't likely to be a good basis for an exploit.

You aren't supposed to get to pick very much of the document in the Web PKI. Rules forbid CAs from letting you write nonsense you made up into most places - they themselves get slightly more opportunity but "Let's attack a windows zero day" doesn't feel like a good use of control over a trusted CA. The biggest contiguous arbitrary chunk of data you get control over will be the public key, an RSA public key might be one kilobyte in size. So, conceivable but unlikely that you can squeeze a working exploit and payload in there.

An X.509 cert that isn't trusted in the Web PKI (ie hand rolled) is a better attack surface because you can write any amount of garbage without some busy body forbidding it, but now your problem is that a non-vulnerable client will see a problem immediately because it's untrusted which is weird. I don't look at the certificates on random web sites I visit... unless they don't work and then I might be curious.

I think code signing certs are a more likely vulnerability, unlike the Web PKI in practice this is down to Microsoft who have a very hands-off approach. I suspect you can get a lot more leeway to write crap into a cert for code signing and as a bonus it'll get seen by the vulnerable Windows PCs, because it's not as though Macs or Linux check the code signing certs on Windows software they can't run anyway.

But as you say we don't know anything, it could be a much more subtle but still dangerous bug.

For example suppose Microsoft's implementation of ECDHE misses a check on the parameters supplied by the other participant. This would make you vulnerable to invalid curve attacks when negotiating ECDHE. Of course a legitimate participant won't try to attack you, but you're doing ECDHE before you know the other participant's identity.

Re: Cryptic Rumblings Ahead of First 2020 Patch Tuesday

#40

Post by msla »

mcguire wrote: post #36
AnimalMuppet wrote: post #29

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.

> One might hope you have a formal spec of a cryptographic library.

Which would be a good first step, but wouldn't protect against timing attacks or Spectre-like hardware frailties.

A solid start is better than nothing, but a false sense of security is worse than nothing.

Post reply on HN