That’s interesting! Do you mean that we don’t know how these things work in general, we don’t know how they affect crypto in general, or specifically Post-Quantum algorithms?
Crypto in Haskell indeed.
There was some interesting discussion about it years ago:
So far I haven’t seen convincing efforts that demonstrate “yes, we’re aware of all those issues and we solved them”. I hope no one is suggesting SafeHaskell for this.
3 Likes
Unless there is a very specific effort to use primops that produce similar native code, I think it could be slower yes.
I don’t believe you can reliably do SIMD from inside Haskell today, unless you delegate this to LLVM.
1 Like
So, basically, the problems with “native” Haskell implementations are:
- We can’t make them reasonably performant (maybe without pretty advanced tricks and methods);
- We don’t know how to make them Side Channel Attack-resistant (constant time, etc. etc.).
Therefore, for all practical use, the choice was to rely on C-based implementations that satisfy both (1) and (2), and merely add Haskell bindings that won’t impact either of the above. Correct?
To me it means - writing crypto in Haskell is hopeless for the near future. The best we can expect is the ability of Haskell code to use crypto written in other more appropriate languages, via packages like cryptonite, etc.
Yeah basically Haskell itself doesn’t provide guarantees that are the hardest to hold, and it’s easier to spread the cost of formal verification and audit across larger ecosystems. That’s why libsodium bindings are an excellent bet. If we wanted to promote Haskell as the language in which to write cryptography algorithm (and on which other languages would bind), we would need to drastically improve the FFI story, tooling, and get many more cryptographers to learn Haskell.
I think one promising alternative is to use a DSL. Cryptol is an example, although I think that is meant more for analysis and not performant compilation.
Cryptol is very much a specification language that can be used both as a subject for reasoning (e.g. “this property should hold for my crypto primitive - what do you think about it, Z3?”) and as a specification for verifying functional correctness of low-level implementations (e.g. “this LLVM IR should match the semantics of this Cryptol spec - what do you think, SAW and Z3?”). There has been some work on generating reasonably fast executable code from Cryptol specs, mostly useful in prototype systems, but it’s not what I’d use for typical applications, and the generated code is not in Haskell.
Aside from that, Cryptol is certainly written in Haskell, but it’s just another programming language. From the perspective of getting crypto code into Haskell apps, you might as well be writing your crypto in Agda. But an embedded language more in the style of something like Accelerate could indeed work. But from a practical perspective, just as we don’t expect to be writing our RTS in Haskell, perhaps it’s OK to be writing our primitives in a suitable low-level language and wrapping them? Or, even better, using well-tested and vetted libraries?
3 Likes
I disagree. I think Cryptol is a much smaller language, so it should be much easier to implement an ergonomic FFI system or even a Haskell “transpiler” that does fully use predictable low level features of GHC (e.g. unboxed primitives).
1 Like
A big problem with that approach is that Cryptol is only a functional (not in the sense of functional programming, but in the sense of “specifies which outputs come from which inputs”) specification language, and many uses of cryptographic primitives have additional nonfunctional requirements that just can’t be expressed in it. An “FFI” would be easy enough - simply rig up a wrapper around the Cryptol interpreter - but that wouldn’t really meet the needs of most people who need crypto.
1 Like
That’s why libsodium bindings are an excellent bet
No PQ support, and (AFAIK) none planned. 
If we wanted to promote Haskell as the language in which to write cryptography algorithm (and on which other languages would bind), we would need to drastically improve the FFI story, tooling, and get many more cryptographers to learn Haskell
It seems that the problem is not with the FFI per se - but with the Haskell compiler and RTS unable at this time to satisfy the necessary “crypto-professional” requirements. Some cryptographers here (especially those interested in formal proofs and such) do know Haskell, others switched to languages like Agda and Coq…
I personally (probably) wouldn’t consider binding to Haskell crypto implementation from other languages - they already have (or likely to get in the near future) either “native” implementations, or FFI access to C-based. And, more than likely - those implementations already exhibit the required properties that seem unattainable in the current Haskell.
DSL - I was going to discount this idea, until I saw the sponsor of that project. I still don’t like it, but probably/hopefully they know what they’re doing, and why.
Yeah, I didn’t mean to single out Cryptol specifically. I did acknowledge that it was probably not a perfect fit due to its focus on specification and not implementation. But I think a small DSL like Cryptol that does allow you to take into accout the nonfunctional requirements would be ideal. Maybe it would need to be more imperative like C, but it would certainly not have to be as complicated and unsafe.
I think that a cryptography-implementation-focused DSL (esp. EDSL) in Haskell is a great research project that I hope someone undertakes and finds success with. And hooking it up to Cryptol for verification of functional properties would be pretty cool.
3 Likes
There is now a fork of cryptonite called cryptol: using crypton by kazu-yamamoto · Pull Request #931 · yesodweb/wai · GitHub
1 Like
crypton. Cryptol is a DSL for cryptographic algorithms by Galois, Inc.:
1 Like
It looks to me that the Z-Botan package at the moment could be the closest candidate to potentially become a “proper” way to do cryptography in Haskell (and be able to replace cryptonite/crypton). Brief look at the hackage documentation suggests it’s mostly feature complete.
The only problem is it currently depends on the Z-Haskell project that tried to do what foundation also did and it seems it didn’t work out (which makes sense, attempts to start from scratch like this are IME doomed to fail unless you have a significant backing, both financial and marketing wise).
So “someone” would need to fork it, rip out the Z-IO and Z-Data bits and replace them with the standard deps like bytestring etc. I don’t know how much work that would be. I would attempt this, but my time budget for OSS has run out
How does it compare to libsodium bindings/wrappers, given that Botan is a C++ library?
From a brief look I had it looks like Botan can be used to implement everything cryptonite/crypton does, I don’t think libsodium can do that (see Comparison of cryptography libraries - Wikipedia, libsodium is missing a lot).
Also, Botan is BSD2, libsodium is GPL3 (it’s not, I looked at the wrong thing).
The best course of action would probably be to make crypton use Botan for everything underneath over time.
1 Like
Last audit is a while ago, but doesn’t sound too bad.
1 Like
Also, Botan is BSD2, libsodium is GPL3.
Can’t see GPL3 in there.
That would be a showstopper indeed.
I took a brief look, and on the surface it doesn’t look too bad - a lot of the changes would need to occur in Z.Botan.FFI but aside from a few things like the CBytes type, most of the Z-stuff used here appears to be a lot of type-aliases and re-exports.
More concerning is the issue that it relies on an out of date fork of botan pulled in via git submodule using a Custom build-type script - it is 3 years out of date, and would need to be replaced with a maintained dependency.
I may not be the best candidate for the job, but I have written my own bindings to libsodium before, back before cryptonite existed (and saltine didn’t provide the APIs I needed), so if time permits, I may give it a go. No promises though 
3 Likes