Hacker News Reader

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.

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.

Is crypt32 supposed to be secure against timing attacks?

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)

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

Given the current state of security practices, I'd say we're lucky if they have unit tests.

https://project-everest.github.io/

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

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

[0] https://en.wikipedia.org/wiki/Refinement_(computing)

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.

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

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

Which also doesn't sound right.

I took the proposal on the table to mean that we systematically harden infrastructure code. If that's what we're doing then a rising tide will lift all boats. Except for the people who fall behind on upgrades. There is a period of chaos where your prediction will play out over and over, but eventually there's a new equilibrium where it's just different rocks to look under. Then people get bored again and they fall behind on upgrades, and now every time new functionality is added to the formal system, by definition people using the old version aren't getting that protection, so you'd look there first.

I think the critical question would be is how quickly does a formal system reach homeostasis? If the rate of bugs (or maybe you call them features?) is negligible after a brief flurry of initial activity, then most of my argument collapses in a divide by zero error.

As to priorities, I don't think penetration and debugging are fundamentally that different. And by that I mean, there's some fuzzy math you do regarding cost (to you) of checking a thing times the value of having that information. Yes, that means a ton of cheap scenarios will be tested very early. But ultimately, how valuable is breaking into a boring system? It's definitely not zero, because you've created another resource for yourself.

Doesn't code that runs on a lot of systems get far more attention than code that runs on a few? Wasn't that part of why OS X got away with fewer viruses? Not because it was profoundly harder to hack, but simply because fewer people cared?

> There is a period of chaos where your prediction will play out over and over, but eventually there's a new equilibrium where it's just different rocks to look under.

When we take steps to eliminate classes of vulnerabilities, well, those vulnerabilities stop being a problem, and we're all more secure. For example, code written in Java or C# is immune from the buffer-overflow attacks, and use-after-free attacks, that continue to plague C code.

There was no counterweight built into this. Security was simply improved.

> Then people get bored again and they fall behind on upgrades, and now every time new functionality is added to the formal system, by definition people using the old version aren't getting that protection, so you'd look there first.

Failure to update packages causes security issues, yes. That doesn't mean that security improvements don't, well, improve security, overall. They absolutely do.

> If the rate of bugs (or maybe you call them features?) is negligible after a brief flurry of initial activity, then most of my argument collapses in a divide by zero error.

If they're using formal methods, they won't be adding bugs. (Discounting side-channel issues.)

I believe it's pretty unusual to see a company make non-verified changes to a codebase originally derived through formal methods. If they care about formal verification, they'll probably stick with it as they make changes.

> how valuable is breaking into a boring system? It's definitely not zero, because you've created another resource for yourself.

Sure - botnets.

> Doesn't code that runs on a lot of systems get far more attention than code that runs on a few?

Of course, but I'm not seeing what you're getting at here.

Well, more details about it are out. It looks like the library worked correctly, but in this case the devs forgot to check something (that the curve had the right params). No amount of writing it in a "theorem proving" language can save you if you don't have the actual specification for the problem itself right.

You could go further. There are a lot of bugs in provers like Coq themselves for which developers create their own proofs of correctness [1]. More precisely: the paper which is linked implements a type checker for the core language of Coq which is proven correct in Coq.

https://www.irif.fr/~sozeau/research/publications/drafts/Coq...

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)

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

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

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

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.

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

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.

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?

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?

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.

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.

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.

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.

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.

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://project-everest.github.io/

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.

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

Microsoft is involved in this: 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.

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