[wyager]

The fact that C++ is so widely used reflects the fact that it’s both old and acceptably designed. It does not even remotely indicate that it’s universally a good tool choice.

I think C++ is not a great choice for complex crypto software because it doesn’t have very good safety-by-construction properties and it has to deal with (extremely) untrusted and probably malicious input. Parsers written in C or C++ are historically one of the biggest attack vectors out there.

[hh3k0]

Okay, I'll bite. What language would be "a great choice" for complex cryptography applications, in your opinion?

[nickpsecurity]

Ada with SPARK Ada variant and careful refcounting wouldve been my baseline given it's all safe by default before Rust came along. D also had potential. Now Rust with SPARK. Im keepimg SPARK in for semi-automated verification. Just rewriting Skein's C code in SPARK automatically found an error thanks to prover. If affording specialists, then something like F star used in miTLS verified stack, Isabelle/HOL, Jasmin language, and/or imperative ML. All core, trusted functionality done that way.

I choose languages with tight control on memory for crypto-related stuff since you want to prevent leaks. You'll follow with a covert-channel analysis to be sure. If not crypto and stopping code injection, then a memory-safe language with interface checks and input validation will cover most problems. Those have been around since one was deployed in first, business mainframe: Burroughs B5000.

[hiq]

What do you mean by imperative ML? Using a language from the ML family, but mostly its imperative features? Can you expand on that?

[nickpsecurity]

Yeah, I should have. There's been prior work porting linear types and other stuff (think Rust safety) like that to ML since that's an easy-to-analyze language academics like to work in. Tolmach et al actually made a converter for it to Ada one time. ML is also the language that most formal verification extracts to by default. CakeML is a verified compiler for ML. There's flow analysis and concurrent variants for it. So, ML by itself is a good choice for correct code that will get a lot of analysis. Imperative ML, imperative for the needed efficiency gains, combined with type systems like Rust's to ensure its safety with numbers mapped to say 64-bit can go a long way.

When I wrote it, though, I was mainly thinking of recent work that converts functional, verified specs into imperative specs that extracts to ML. I think that has a lot of potential for producing a pile of verified data structures with low cost similarly to the COGENT language that was used for ext2 filesystem. Got a link for Imperative/HOL-to-ML below.

http://www.ssrg.ece.vt.edu/~lammich/pub/itp15_sepref.pdf

[zerokernel]

I didn't expect anything interesting to come up as replies, but here we are - thanks for those insights.

[wyager]

Depends on the application. I would personally use Rust for embedded applications (since it’s low-overhead and ADTs are basically a requirement for safe parsers) and Haskell for non-embedded. But if neither of those float your boat, there are other safe-by-construction parser-friendly languages available, mostly from the ML family.

[xiphias]

At this point Rust is the clear winner, as it's providing higher safety for similar run-time speed.