What do you mean by verifiablity?

If you are using a casual, inspection = verification definition then I think most would agree that it is true that open source is easier to inspect.

But "verified" software often means formal mathematical verification, and that is orthogonal to if the source is open.

> But "verified" software often means formal mathematical verification, and that is orthogonal to if the source is open.

I think there may be cross-talk here related to who's doing the verifying too. I think the parent is assuming "verification" would imply that a 3rd party could verify the software in question. AFAIUI it's currently nowhere near practical for a 3rd party to verify closed-source software of any non-trivial size. (Correct me, if I'm wrong, obviously.)

It's still a research problem even for open-source unless the software is built with formal verification in mind (for example in Coq or Agda), but at least there's an existence proof that it's possible to do for non-trivial software (see CompCert C). That was still a multi-year effort and it's still a somewhat (architecturally) simple program as compilers tend to be.

Downthread tptacek talks about how his company does verification of binary images. I assume there are limits to what is possible, but that's really the same as any verification approach.

I do agree that 'who is verifying' is a valid way of looking at it too.

Regardless, it's pretty clear that tptacek means formal verification.

Edit: see http://arieg.bitbucket.org/pdf/seahorn.pdf

My company doesn't do this. But many companies specialize in it.

If whatsapp allows few experts or companies access to code they can always verify but the issue is centrally hosted , that is the issue not open or close. If i can build software on and host on my server that might be better

Open vs. closed is obviously orthogonal to verifiability. Those who verify software have access to the source, open or not.

More parties have the opportunity to be verifiers of open software. However, a given OSS program might not attract skilled verifiers.

> Those who verify software have access to the source, open or not.

That's not true. Black hats are essentially verifiers, and they generally do not have access to closed source.

How do you look at the last 15 years worth of Microsoft Windows OS advisories and conclude that closed source has prevented hats of all colors from discovering vulnerabilities?

Why do you keep raising this straw man? It is obviously possible to reverse engineer object code and find vulnerabilities. But it is (equally obviously) easier to examine source code to find vulnerabilities.

This slippery slope goes in both directions. Software is also easier to audit when it's built in higher-level languages, but we don't have ideological objections about verifiability to software written in C.

I'm not sure I understand what you mean by that. Do you mean that people think that it doesn't matter what language code is written in as long as it is open source? I certainly don't believe that. It's pretty clear to me that C is a terrible language for writing secure code. (But coming up with something that is actually better than C is not so easy.)

All agree that higher level (e.g. C) is easier to reason about than lower level (assembly).

Now, you say that open source (e.g. C) is not only easier, but qualitatively different: open source good, closed source bad.

tptacek points out: higher level (e.g. Haskell) is easier to reason about than lower level (e.g. C) - maybe even qualitatively.

So, why are people only complaining about closed source, when they should (by analogous reasoning) be complaining about code written in C? Granted, it's possible to analyse, but it's obviously easier when it's written in Haskell!

For what it's worth, I complain about code written in C too.

Here might be something to look for among those advisories: how many of them were discovered in the source versus in the field.

If the vendor is lazy about verifying code, it being closed is a big disadvantage. "We're not combing the code for bugs, and neither is anyone else; if it's not reported to us, it doesn't exist."

They are verifiers who cannot, with straight faces, declare a body of code verified.

I'll bet some of them can.