3 ms·

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

by hh3k0 9y ago

xiphias 9y ago
At this point Rust is the clear winner, as it's providing higher safety for similar run-time speed.
wyager 9y ago
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.
nickpsecurity 9y ago
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 9y ago
  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 9y ago
    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 http://www.ssrg.ece.vt.edu/~lammich/pub/itp15_sepref.pdf
    - zerokernel 9y ago
      I didn't expect anything interesting to come up as replies, but here we are - thanks for those insights.

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

by hh3k0 9y ago

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

xiphias 9y ago

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

wyager 9y ago

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.

nickpsecurity 9y ago

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 9y ago
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 9y ago
  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 http://www.ssrg.ece.vt.edu/~lammich/pub/itp15_sepref.pdf
  - zerokernel 9y ago
    I didn't expect anything interesting to come up as replies, but here we are - thanks for those insights.