> the programming language used to represent a computer program has nothing fundamentally to do with whether it can be verified
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.
You're using a word, "easier", that is keeping us off the same page. I agree that Haskell programs are easier in many senses to verify than PHP programs. But our field does formal methods verification of assembly programs, for instance by lifting them to an IR.
The Skype client was obfuscated, encrypted, and riddled with anti debugging boobytraps, none of which prevented people from figuring out exactly what it did. (Not exactly a formal analysis, but probably news to the people who think messaging apps have never been reversed before.)
AFAICT that's (at best) research level stuff. I'd love to be proven (heh) wrong, though. I think what lisper was after was actual practical applications, e.g. something along the lines of the CompCert C compiler[1].
[1] Which I'll note was written and verified in Coq a high-level proof-oriented language.
I don't know what "(at best) research level stuff" means. Here's a well-regarded LLVM lifter by a very well-regarded vuln research team that's open source:
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.
> 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.
I'm sorry, but once again: this thread began with a different claim. I'm not interested in debating whether it's easier to audit C code or assembly code: I've repeatedly acknowledged that it is.
Then what exactly are we arguing about? My original claim was:
"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.
Look at the original claim you made. You said it's possible to provide evidence of the existence of vulnerabilities in closed source software, but not of their absence. To the extent that's true, it's true of open source software as well. The dichotomy you presented, about absence of evidence vs. evidence of absence, is not about open source software but about all software built without formal methods --- which, regardless of the language used, is almost all software.
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?
I think it's possible that that's true, but am uncertain: the claim depends on formal methods for software construction that defy decompilation. But the higher-level the tools used for building software, the more effective decompilation tends to be. I also don't think we're even close to the apex of what decompilation (even of the clumsy, lossy compiled languages we have today) will be able to do.
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.
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.