6 ms·

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.

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 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). Had there been a wide-spread exploit, it could have cost the world millions of man-years. [1] https://en.wikipedia.org/wiki/Usage_share_of_operating_systems https://en.wikipedia.org/wiki/Usage_share_of_operating_syste... [2] https://www.schneier.com/blog/archives/2009/10/proving_a_compu.html https://www.schneier.com/blog/archives/2009/10/proving_a_com... [3] Professor Gernot Heiser, the John Lions Chair in Computer Science in the School of Computer Science and Engineering and a senior principal researcher with NICTA, said for the first time a team had been able to prove with mathematical rigour that an operating-system kernel—the code at the heart of any computer or microprocessor—was 100 per cent bug-free and therefore immune to crashes and failures. Verifying the kernel—known as the seL4 microkernel—involved mathematically proving the correctness of about 7,500 lines of computer code in a project taking an average of six people more than five years.

saagarjha 7y ago
Usually you don't really verify the correctness of existing code; you rewrite it in a language that makes it possible to make guarantees that you care about. In addition, Microsoft needs to allocate their time: which components should be verified? Not all of them can be verified practically yet.
- chabad360 7y ago
  Keep in mind that we are discussing code meant to run cryptography operations, I'm pretty sure that kind of stuff should be high up on the priority list.
- erk__ 7y ago
  Microsoft is already using quite a bit of money doing this for example they have made the language F* which have been used to write a verifiable implementation of https. https://www.fstar-lang.org/ https://www.fstar-lang.org/ https://project-everest.github.io/ https://project-everest.github.io/
  - saagarjha 7y ago
    I'm not saying that Microsoft isn't doing good work in this area; it's just that it's impractical to pick an old component that's recently found to have vulnerabilities in it and try to blame Microsoft for not having the foresight to write it in a formally verified way.
blattimwind 7y ago
> 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.
- bitexploder 7y ago
  X.509 and TLV is gnarly. So many edge cases. Then there are encoding formats and many other things. It’s 50kloc easy. The file size is like 500k. A lot happens in there for sure.
r00fus 7y ago
> 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.
- thephyber 7y ago
  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).
  - cjbprime 7y ago
    There actually is regulation, though. As I understand it, in theory GDPR could now fine Microsoft 1% of revenue if they've behaved catastrophically negligently at keeping user secrets secure.
asdfasgasdgasdg 7y ago
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?
- jimbob45 7y ago
  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.
  - polemic 7y ago
    Bold assertion in the face of side channel and timing attacks.
    - mcguire 7y ago
      Is crypt32 supposed to be secure against side channel and timing attacks?
  - magicalhippo 7y ago
    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.
- cjbprime 7y ago
  Heartbleed was found (after the fact) by a simple fuzzer. The ability of fuzzers has massively increased in recent years.
  - 7y ago
bouncycastle 7y ago
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.
- TimTheTinker 7y ago
  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.
  - hinkley 7y ago
    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'.
    - 7y ago
AnimalMuppet 7y ago
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.
- mcguire 7y ago
  One might hope you have a formal spec of a cryptographic library.
  - msla 7y ago
    > 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.
    - mcguire 7y ago
      Is crypt32 supposed to be secure against timing attacks?
  - rtpg 7y ago
    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 definition on that front! Having specs and formally proven code helps to make sure your code isn't prone to a certain class of errors (just like bounds checking/lack of raw pointers prevents another class of errors), but it's not a magical catch-all. Especially if you are in a space like cryptography where you're trying to assert negatives (that end up being held up by assumptions around feasibility of certain things)
taneq 7y ago
"Beware of bugs in the above code; I have only proved it correct, not tried it." - Donald Knuth
morpheuskafka 7y ago
Microsoft has been actively working on several mathematical validation projects, including an HTTPS library... https://project-everest.github.io/ https://project-everest.github.io/. So I don't think they are avoiding formal verification just to be cheap.
tinus_hn 7y ago
You can prove some code to be correct as to some specification but it is pretty much impossible to define the specification to be ‘secure’ forever. Not only do unexpected problems pop up, such as the cpu vulnerabilities, also threat models change and it may turn out your specification solidly protects something that doesn’t matter at all. That doesn’t mean that properly validating code so it at least doesn’t overflow its buffers is useless of course.
MaxBarraclough 7y ago
> 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.
fulafel 7y ago
Microsoft is involved in this: https://mitls.org/ https://mitls.org/ - but no idea if they get into certificate or if the verification focuses on just the tls wire protocol. The inertia and complacency of existing code is enormous, MS and other affluent vendors have been watching vulns in their codebases bubble up for decades and their customers tolerate it. Big MS customers buy into it deeply: companies won't hire security professionals as CSOs who would ban insecure "industry standard" setups such as org wide AD domains and MS office attachments that malware most often spreads through.

saagarjha 7y ago

Usually you don't really verify the correctness of existing code; you rewrite it in a language that makes it possible to make guarantees that you care about. In addition, Microsoft needs to allocate their time: which components should be verified? Not all of them can be verified practically yet.

chabad360 7y ago
Keep in mind that we are discussing code meant to run cryptography operations, I'm pretty sure that kind of stuff should be high up on the priority list.
erk__ 7y ago
Microsoft is already using quite a bit of money doing this for example they have made the language F* which have been used to write a verifiable implementation of https. https://www.fstar-lang.org/ https://www.fstar-lang.org/ https://project-everest.github.io/ https://project-everest.github.io/
- saagarjha 7y ago
  I'm not saying that Microsoft isn't doing good work in this area; it's just that it's impractical to pick an old component that's recently found to have vulnerabilities in it and try to blame Microsoft for not having the foresight to write it in a formally verified way.

blattimwind 7y ago

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

bitexploder 7y ago
X.509 and TLV is gnarly. So many edge cases. Then there are encoding formats and many other things. It’s 50kloc easy. The file size is like 500k. A lot happens in there for sure.

r00fus 7y ago

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

thephyber 7y ago
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).
- cjbprime 7y ago
  There actually is regulation, though. As I understand it, in theory GDPR could now fine Microsoft 1% of revenue if they've behaved catastrophically negligently at keeping user secrets secure.

asdfasgasdgasdg 7y ago

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?

jimbob45 7y ago
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.
- polemic 7y ago
  Bold assertion in the face of side channel and timing attacks.
  - mcguire 7y ago
    Is crypt32 supposed to be secure against side channel and timing attacks?
- magicalhippo 7y ago
  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.
cjbprime 7y ago
Heartbleed was found (after the fact) by a simple fuzzer. The ability of fuzzers has massively increased in recent years.
- 7y ago

bouncycastle 7y ago

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.

TimTheTinker 7y ago
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.
- hinkley 7y ago
  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'.
  - 7y ago

AnimalMuppet 7y ago

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.

mcguire 7y ago
One might hope you have a formal spec of a cryptographic library.
- msla 7y ago
  > 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.
  - mcguire 7y ago
    Is crypt32 supposed to be secure against timing attacks?
- rtpg 7y ago
  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 definition on that front! Having specs and formally proven code helps to make sure your code isn't prone to a certain class of errors (just like bounds checking/lack of raw pointers prevents another class of errors), but it's not a magical catch-all. Especially if you are in a space like cryptography where you're trying to assert negatives (that end up being held up by assumptions around feasibility of certain things)

taneq 7y ago

"Beware of bugs in the above code; I have only proved it correct, not tried it." - Donald Knuth

morpheuskafka 7y ago

Microsoft has been actively working on several mathematical validation projects, including an HTTPS library... https://project-everest.github.io/ https://project-everest.github.io/. So I don't think they are avoiding formal verification just to be cheap.

tinus_hn 7y ago

You can prove some code to be correct as to some specification but it is pretty much impossible to define the specification to be ‘secure’ forever. Not only do unexpected problems pop up, such as the cpu vulnerabilities, also threat models change and it may turn out your specification solidly protects something that doesn’t matter at all. That doesn’t mean that properly validating code so it at least doesn’t overflow its buffers is useless of course.

MaxBarraclough 7y ago

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

fulafel 7y ago

Microsoft is involved in this: https://mitls.org/ https://mitls.org/ - but no idea if they get into certificate or if the verification focuses on just the tls wire protocol. The inertia and complacency of existing code is enormous, MS and other affluent vendors have been watching vulns in their codebases bubble up for decades and their customers tolerate it. Big MS customers buy into it deeply: companies won't hire security professionals as CSOs who would ban insecure "industry standard" setups such as org wide AD domains and MS office attachments that malware most often spreads through.