5 ms·

tptacek, 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 so

by jMyles 10y ago

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

nl 10y ago
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.
- lomnakkus 10y ago
  > 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.
  - nl 10y ago
    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 http://arieg.bitbucket.org/pdf/seahorn.pdf
    - tptacek 10y ago
      My company doesn't do this. But many companies specialize in it.
  - jsudhams 10y ago
    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
  - jsudhams 10y ago
    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
kazinator 10y ago
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.
- lisper 10y ago
  > 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.
  - tptacek 10y ago
    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?
    - lisper 10y ago
      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.
      - tptacek 10y ago
        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.
        lisper 10y ago
        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.)

by jMyles 10y ago

nl 10y ago

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.

lomnakkus 10y ago
> 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.
- nl 10y ago
  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 http://arieg.bitbucket.org/pdf/seahorn.pdf
  - tptacek 10y ago
    My company doesn't do this. But many companies specialize in it.
- jsudhams 10y ago
  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
- jsudhams 10y ago
  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

kazinator 10y ago

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.

lisper 10y ago
> 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.
- tptacek 10y ago
  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?
  - lisper 10y ago
    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.
    - tptacek 10y ago
      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.
      - lisper 10y ago
        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.)