4 ms·

Far from having comparable resources to billion dollar space and nuclear corporations, FOSS developers often have no funding at all and work entirely in our spa

Far from having comparable resources to billion dollar space and nuclear corporations, FOSS developers often have no funding at all and work entirely in our spare time, for free. Any attempt to accomplish "provably correct" code with the same attention to detail that goes into space or nuclear systems would kill a typical FOSS project before a single line of code ever got written.

verbin217 11y ago
This is likely true today but it's increasingly false. Massive efforts are already underway to develop tooling and methodology for this purpose. Once completed the applications developed with them will be significantly easier to produce. Also, since they're provably correct the "maintenance" metaphor is no longer applicable. What we need is provably correct code generation for the output of theorem provers like Coq. These tools generate a large portion of the proof automatically. Programs can be inferred directly from proofs using the Curry-Howard Correspondence. Interesting discussion here: http://www.mail-archive.com/sc-l@securecoding.org/msg01278.html http://www.mail-archive.com/sc-l@securecoding.org/msg01278.h...
- adrianN 11y ago
  > Also, since they're provably correct the "maintenance" metaphor is no longer applicable. If you want your software to never change, then sure, a proof of correctness is enough. But I've yet to see a piece of software that is both relevant and never has to adapt to new requirements.
  - verbin217 11y ago
    Agreed. When I said "maintenance" I was referring to the continuous post hoc work needed to uphold the original functionality as it encounters the full range of it's potential input.
- jeffreyrogers 11y ago
  Coq is very hard to use.
  - deleted 11y ago
    [deleted]
sitkack 11y ago
One can start by not using insecure languages and practices. Using C/C++ for this application domain is a non-starter, now matter how many times one can trump the word free. Does the existence of a free but flawed product make the "secure chat" universe demonstrably better? The level of blasé disregard for basic secure coding makes me think it is on purpose. More attention to security has been put into Postfix and OpenSSH than any of these encrypted but in no way provably secure chat systems.
- glass- 11y ago
  > Using C/C++ for this application domain is a non-starter What language would you use? The requirements are that it be low-level enough that you can zero keys from memory and needs to be able to be ported to every major OS, including iOS and Android.
  - sitkack 11y ago
    What I would use and languages that applicable aren't the same. I'd probably use OCaml. But almost anything is better than C/C++ for this domain. If the goal was to get as many programmers, with the widest distribution, Java 7 would be an excellent choice. RoboVM can compile to native for the platforms that don't have the required runtime. Others might use Rust, ATS or Idris. Hell, even Lua with a small C core (NACL, os calls, etc) would be better. The red herring that gets trotted out is timing and side channel attacks, crypto itself can still be done in nacl. But everything else, GUI interaction, network interaction and parsing of external data should be done in a safe language.
    - xorcist 11y ago
      Obscure != secure. The same argument has been said for Java (but turned out to have worse problems in practice), Ruby (where if you every wrote something in Rails you've been vulnerable halv a dozen times by now) and PHP (and any commentary here should be unnecessary). Sure, all the obscure languages you mention which never had even one project with a fraction of the usage base of Apache or Postfix may have no known security problems, but that's not a something to boast about. If you really want these languages to succeed, build a project with the potential user base of Nginx or Linux. Just don't complain about other's language choices, especially not when those are well known and well understood ones.

verbin217 11y ago

This is likely true today but it's increasingly false. Massive efforts are already underway to develop tooling and methodology for this purpose. Once completed the applications developed with them will be significantly easier to produce. Also, since they're provably correct the "maintenance" metaphor is no longer applicable. What we need is provably correct code generation for the output of theorem provers like Coq. These tools generate a large portion of the proof automatically. Programs can be inferred directly from proofs using the Curry-Howard Correspondence. Interesting discussion here: http://www.mail-archive.com/sc-l@securecoding.org/msg01278.html http://www.mail-archive.com/sc-l@securecoding.org/msg01278.h...

adrianN 11y ago
> Also, since they're provably correct the "maintenance" metaphor is no longer applicable. If you want your software to never change, then sure, a proof of correctness is enough. But I've yet to see a piece of software that is both relevant and never has to adapt to new requirements.
- verbin217 11y ago
  Agreed. When I said "maintenance" I was referring to the continuous post hoc work needed to uphold the original functionality as it encounters the full range of it's potential input.
jeffreyrogers 11y ago
Coq is very hard to use.
- deleted 11y ago
  [deleted]

sitkack 11y ago

One can start by not using insecure languages and practices. Using C/C++ for this application domain is a non-starter, now matter how many times one can trump the word free. Does the existence of a free but flawed product make the "secure chat" universe demonstrably better? The level of blasé disregard for basic secure coding makes me think it is on purpose. More attention to security has been put into Postfix and OpenSSH than any of these encrypted but in no way provably secure chat systems.

glass- 11y ago
> Using C/C++ for this application domain is a non-starter What language would you use? The requirements are that it be low-level enough that you can zero keys from memory and needs to be able to be ported to every major OS, including iOS and Android.
- sitkack 11y ago
  What I would use and languages that applicable aren't the same. I'd probably use OCaml. But almost anything is better than C/C++ for this domain. If the goal was to get as many programmers, with the widest distribution, Java 7 would be an excellent choice. RoboVM can compile to native for the platforms that don't have the required runtime. Others might use Rust, ATS or Idris. Hell, even Lua with a small C core (NACL, os calls, etc) would be better. The red herring that gets trotted out is timing and side channel attacks, crypto itself can still be done in nacl. But everything else, GUI interaction, network interaction and parsing of external data should be done in a safe language.
  - xorcist 11y ago
    Obscure != secure. The same argument has been said for Java (but turned out to have worse problems in practice), Ruby (where if you every wrote something in Rails you've been vulnerable halv a dozen times by now) and PHP (and any commentary here should be unnecessary). Sure, all the obscure languages you mention which never had even one project with a fraction of the usage base of Apache or Postfix may have no known security problems, but that's not a something to boast about. If you really want these languages to succeed, build a project with the potential user base of Nginx or Linux. Just don't complain about other's language choices, especially not when those are well known and well understood ones.