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

21–30 of 96 posts

Re: Cryptic Rumblings Ahead of First 2020 Patch Tuesday

#21

Post by blattimwind »

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…

> 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.

Crypt32 mostly concerns itself with X.509 certificates and I believe actually implements all that stuff (instead of delegating it elsewhere). I wouldn't be surprised if it contains considerably more code than 10k lines.

Re: Cryptic Rumblings Ahead of First 2020 Patch Tuesday

#22

Post by r00fus »

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.

Re: Cryptic Rumblings Ahead of First 2020 Patch Tuesday

#23

Post by bob1029 »

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…

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 the cryptographic primitives are already all right there for you to use to authenticate the cert).

Re: Cryptic Rumblings Ahead of First 2020 Patch Tuesday

#24

Post by asdfasgasdgasdg »

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…

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 formally proven first? Heartbleed? Spectre? Meltdown?

Re: Cryptic Rumblings Ahead of First 2020 Patch Tuesday

#25

Post by jimbob45 »

asdfasgasdgasdg wrote: post #24
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…

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.

Re: Cryptic Rumblings Ahead of First 2020 Patch Tuesday

#26

Post by polemic »

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.

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

Re: Cryptic Rumblings Ahead of First 2020 Patch Tuesday

#27

Post by cjbprime »

asdfasgasdgasdg wrote: post #24
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…

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…

Heartbleed was found (after the fact) by a simple fuzzer. The ability of fuzzers has massively increased in recent years.

Re: Cryptic Rumblings Ahead of First 2020 Patch Tuesday

#28

Post by bouncycastle »

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-channel information (such as timing). Also, nobody has proven that things like sha256 and so on are unbreakable.

Re: Cryptic Rumblings Ahead of First 2020 Patch Tuesday

#29

Post by AnimalMuppet »

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 each kind of bug, you need a different proof. Did your proof cover every category of bug? Almost certainly not. So strong claims like "100 per cent bug free" are almost certainly overstating things, no matter the credentials of the person making them. "100 per cent bug free for the categories of bugs we proved"? OK, but that's a significantly weaker claim.

For the 7500 lines (or however many) in crypt32.dll, you want to prove that there are no security attacks of any category possible. That becomes a harder and harder job as we keep discovering new categories of security attacks.

Re: Cryptic Rumblings Ahead of First 2020 Patch Tuesday

#30

Post by asdfasgasdgasdg »

cjbprime wrote: post #27
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…

Heartbleed was found (after the fact) by a simple fuzzer. The ability of fuzzers has massively increased in recent years.

Fuzzers are great! I have fuzzed one or two mission critical high exposure libraries in my time. But they are a totally different thing than formal verification.
Post reply on HN