You can demonstrate the presence of a vulnerability in closed source software but there's no way to demonstrate (or even provide evidence of) the absence of any vulnerabilities.
Open vs. closed-source software is a concern orthogonal to verifiability.
I know this is a tough thing for people to get their heads around since it challenges a major open source orthodoxy. I like open source too. But the people who ratified it were not experts in this field, and this particular benefit of open source is overstated.
That's not true. The design of a language can make it easier to verify with respect to certain properties. For example, it is much easier to verify that a typical Python program does not dereference dangling pointers than a typical C program.
It is true that open source does not help as much as some of its adherents like to think. But that doesn't mean that it doesn't help at all, and it is certainly not true that it cannot help substantially in principle even if it does not help much in current practice.
[1] Which I'll note was written and verified in Coq a high-level proof-oriented language.
https://blog.trailofbits.com/2014/08/07/mcsema-is-officially...
There are a bunch of other lifters, not all of them to LLVM.
Already, with the idea of IR lifting, we're at a point where we're no longer talking about reading assembly but rather a higher-level language. But this leaves out tooling that can analyze IR (or, for that matter, assembly control flow blocks).
Someone upthread stridently declared that analyzing one version of a binary in isolation was hard enough, but that the work of looking at every version was "staggering", "capital-h Hard". But that problem is in some ways easier than basic reverse engineering, which is why security product companies and malware research teams have teams of people using BinDiff-like tools to do it. "BinDiff" is a deceptive name; "Bin" refers to compiled binaries, because the tools work based on graph comparisons of program CFGs.
Part of the problem I have talking about this stuff is that this isn't really my area of expertise --- not in the sense that I can't reverse a binary or use a BinDiffing tool, because most software security people can, myself included, but in the sense that I'm describing the state of the art as of, like, 6 years ago. I'm sure the tooling I'm describing is embarrassing compared to what our field has now.
Open vs. closed source is an orthogonal concern to verifiability.
The evidence you have presented does not support this conclusion. All you've shown is that it is possible to reverse-engineer object code, but this was never in doubt. It is still an open possibility (indeed it is overwhelmingly probable) that it is a hell of a lot easier to audit code if you have access to the source. All else being equal, more information is always better than less, and, as I pointed out earlier, the constraints imposed by some languages can often be leveraged to make the verification task easier.
"You can demonstrate the presence of a vulnerability in closed source software but there's no way to demonstrate (or even provide evidence of) the absence of any vulnerabilities." [Emphasis added] (Also please note that I very deliberately did not use the word "prove".)
Your response was:
"That's identically true of open-source software."
If you acknowledge that it is easier to audit source code then it cannot be the case that anything is "identically true" of open and closed source software (except for uninteresting things like that they are both subject to the halting problem). If it is easier to audit source code (and you just conceded that it is) then it is easier to find vulnerabilities, and so it is more likely that vulnerabilities will be found, and so (for example) the failure of an audit conducted by a competent and honest agent to find vulnerabilities is in fact evidence (not proof) of the absence of vulnerabilities.
But if you have source code written in a language designed to admit formal proofs then it is actually possible to demonstrate the absence of certain classes of vulnerabilities. For example, code written in Rust can be demonstrated (maybe even proven) to not be subject to buffer overflow attacks.
The point you made is orthogonal to the question of whether we can understand and evaluate ("verify") closed-source software.
Let me try to advance a different thesis then: it is possible to write software in such a manner that the source code is amenable to methods of analysis that the object code is not. Accordingly, for software written in such manners, it is possible to provide certain guarantees if the source code is available for analysis, and those guarantees cannot be provided if the source code is not available. Would you agree with that?
So, it's an interesting question, and one I have much less of a strong opinion on.
If you can't tell, my real issue here is the idea that closed-source software is somehow unknowable. I know you're not claiming that it is. But I think if you look over these threads, you'll see that they tend to begin with people who do believe that, or claim to.
Over the years interacting with you here on HN, I think this basically sums up the worldview that puts you and I at odds:
> Open vs. closed-source software is a concern orthogonal to verifiability.
Is there a place where you have written at length, defending this assertion?
I am open to it. But it does not resonate with my understanding, nor my (substantial, I think) experience in deployments of open- and closed-source software with specific respect to verifiability.
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.
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.
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.
More parties have the opportunity to be verifiers of open software. However, a given OSS program might not attract skilled verifiers.
That's not true. Black hats are essentially verifiers, and they generally do not have access to closed source.
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!
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."
I would guess that programs in a Turing-incomplete language will be easier to verify than ones in a Turing complete one.
I'd say that's hard for open source software to do as well.
Introducing backdoors into open source source is also more difficult.
EDIT: WTF people? Why is every response to this comment being downvoted into oblivion? The sibling comment to this one (https://news.ycombinator.com/item?id=13395657) was killed in a matter of minutes despite being (IMHO) a perfectly reasonable and constructive response.
(That comment is incorrect but I agree with you that it's constructive).