Hacker News Reader

Comment by sitkack | Hacker News Reader

This makes the same mistake as Tox, unsafe native code. These kinds of projects need the same level of detail and provable correctness that goes into space or nuclear control systems.

View on HN

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.

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.h...

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

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.

Coq is very hard to use.

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.

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

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.

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.

Mozilla and Samsung are building the Servo rendering engine, based on Rust.

Everybody and their cat knows that. It's also not a functional web browser yet, and doesn't have a measureable market share compared to Firefox and Chrome, which are C++. Let's compare CVEs when it's at least in the top three. But if it survives one day at cansecwest I would be thoroughly impressed.

Well it's an effort, and several popular libraries are releasing bindings for their products using Rust.

And for two large companies to be working on something as large as Servo, even before the language went 1.0, there must be something good about it.

I think you're conflating three issues. One is of course unsafe native code, which could at least in part be fixed by picking a different programming language (cough Rust) that has stronger guarantees. Another is correctness of the implementation with regard to the specification. That is a lot more difficult to verify, and understandably a very big security concern. Third is the security of of the specification itself, which might be easier to prove, but is still no simple feat.

Most professional cryptographers write code in C. And what is arguably the best crypto library (NaCl) is written in C. Look, safety is a great idea. Unfortunately, things like cryptography need to be fast if you expect people to use them, and it is impossible to get the fastest levels of performance without using a low level language and dropping to assembly when necessary.

This is untrue. Java is very fast once the JIT warms up. The biggest cost to java is the startup time, but for a long running application it's not really an issue.

In fact, Java can be faster than C for a long running application, because you avoid problems like memory fragmentation. Garbage collection can compact used objects into smaller sets of memory, improving cache utilization.

Performance is not a singular entity. It is very very hard to write sidechannel resistant code in Java, because of the performance characteristics.

The parent comment said that they need to write it in C in order for it to be fast enough for people to use it, which is false.

As for timing attacks, it's very very hard to write sidechannel resistant code in any language, I don't believe Java is particularly harder. C/C++ is not as deterministic as you would think.

http://blog.erratasec.com/2015/03/x86-is-high-level-language...

Crypto is a only a small part of a project like this. Crypto isn't where a messaging client is going to break. Most likely it will be in parsing data the network. There is no reason to use C for the entire application because NaCl is in C, even if everyone on the project is Daniel J. Bernstein.

Would it be possible to do this (https://github.com/notsecure/uTox/issues/203) in Ricochet though?

They seem to be using more standard libraries than Tox.

Whoa. Am I right in thinking that the proper fix would be not to use the system() function in the first place, so that you don't have to guess the escaping rules of whatever shell the user happens to be using?

Reply on news.ycombinator.com