A new future for cryptography in Haskell

Announcements
#68

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
#69

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
#70

That’s why libsodium bindings are an excellent bet

No PQ support, and (AFAIK) none planned. :frowning:

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.

#71

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.

#72

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
#73

There is now a fork of cryptonite called cryptol: using crypton by kazu-yamamoto · Pull Request #931 · yesodweb/wai · GitHub

1 Like
#74

crypton. Cryptol is a DSL for cryptographic algorithms by Galois, Inc.:

1 Like
#75

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 :frowning:

#76

How does it compare to libsodium bindings/wrappers, given that Botan is a C++ library?

#77

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
#78

Last audit is a while ago, but doesn’t sound too bad.

1 Like
#79

Also, Botan is BSD2, libsodium is GPL3.

Can’t see GPL3 in there.

That would be a showstopper indeed.

#80

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 :slight_smile:

3 Likes
#81

Right, it’s ISC which is equivalent to BSD. Sorry for the confusion, I must’ve looked at the wrong thing.

#82

Indeed, I’m not sure why the author did this. Botan package (at least on Arch Linux) supplies a .pc file, so using external dependency should be easy with pkgconfig-depends.

#83

After diving into this yesterday, this is my reaction to many things regarding this library. I did not accomplish much of anything aside from gathering information, but here is what I have discovered so far:

  • Some things like JSON / Text / Vector aren’t re-exports like I initially thought - they are all custom types (yikes!)

  • Most uses of Text are used like CB.fromText . T.toText or to derive their custom Z.Data.Text.Print class, so I don’t think pose a large problem per se and I think it could be swapped out for Data.Text.

  • All uses of JSON are just used for deriving instances of it, so they can probably be ignored entirely.

  • All uses of Vector are for Z.Data.Vector.Bytes which is actually a thin wrapper around PrimArray Word8 - we could convert this to use ByteArrayAccess / ByteArray constraints possibly, but we’re going to have to deal with it. Ditto for another type CBytes, which is a direct newtype around PrimArray Word8.

  • The Z.Data.CEBytes is intended for constant-time equality checks, but it is also a newtype over PrimArray Word8 - this might be replaceable with a newtype ConstEq ba = ConstEq ba with instance (ByteArrayAccess ba) => Eq ba where (==) = constEq or something. We’re going to have to deal with it same as Z.Data.Vector.Bytes

  • Z.IO.BIO stuff is unnecessary / experimental and can probably be jettisoned / ignored entirely.

  • Some stuff in Z.Foreign gets a lot of use eg withPrimVectorUnsafe so we’ll have to be careful bringing in or replacing it.

There’s also some questions of how far do we want to go, beyond our initial focus on stripping out the Z-* dependencies. We can conceptually look at this as two libraries - there is the low-level botan bindings in the Z.Botan.FFI file, and the higher-level crypto interfaces in Z.Crypto.*. We should think about what we want the crypto interfaces to look like.

  • A prime example of this is how this library uses large enumerations like the HashType and CipherType data types to represent all algorithms as one type. However, this is entirely the choice of the Z library author, and is not required by botan itself. It is also awkward and limits type-level programming compared to functional dependencies with a witness / proxy a la cryptonite, or associated type / data families that I’ve written in the past.

I’m sure there will be more, but these are my major thoughts after getting it to build, and rifling through everything a bit yesterday and this morning.

I’ll keep this thread updated as needed.
Edited to differentiate CBytes and CEBytes

4 Likes
#84

Yeah, that’s a good question. Considering that crypton seems to have been well-received and a few packages already switched to it, a good option would be to have a low-level package for botan bindings and then use this package to switch crypton to use botan for everything it does over time.

This approach has significant advantage over coming up with a new library since tons of existing dependencies would directly benefit without having to switch to a new API and improvements could be incremental, i.e. make crypton use AES from botan, then use hash functions from botan etc.

botan supports a ton of cryptographic primitives, so presumably crypton could use it for everything it does. This needs double checking though.

And since botan also implements TLS protocol, presumably the tls package could also be made to use it in the end, which I think would put the Haskell ecosystem in a comfortable place cryptography-wise.

That’s obviously a significant undertaking, but perhaps Haskell Foundation could help here @david-christiansen?

2 Likes
#85

Perhaps! It would be based on a cost-benefit analysis, of course. This is the kind of thing that our proposals process is really built for - to help explore the actual costs and benefits of this kind of thing, and enumerate just what kind of help is needed.

2 Likes
#86

An update on some brief hackery: On closer inspection, I realized I never had actually gotten it to build properly, but I’m not sure it really matters because I discovered many more issues while fiddling around with the Z-Botan repo knocking out pieces to get it to work.

  1. It uses an older version Botan 2, not Botan 3.

  2. Z-Botan is itself woefully out of date, even for its own Z- dependencies

    • It has strict primitive (>=0.7 && <0.8) and time (>=1.11 && <1.12) dependencies
    • It needs Z-Data 8.6.1 and Z-IO 8.1.1, which are themselves outdated
    • It needs ghc865 to get versions aligned.

  3. Botan setup / configuration is done via configure.py script

    • This script is 3400+ lines of python.
    • Z-Botan calls this during the custom Setup.hs phase (and is a tad inscrutable because there are no comments).
    • args = configureFile:"--amalgamation":"--disable-shared":hostFlag is where we can inject the arguments to control botan’s build
    • Building The Library — Botan

These issues are severe enough that, between the need to strip out the Z-IO and Z-Data plus the need to update to Botan 3, it might be better to start over with new bindings in a new project rather than try to cajole Z-Botan back to life.

My next move is probably to see if I can get Botan 3 building solo, then try and integrate it into a fresh project, and then pick a subset of the bindings (eg, hashing) and try to implement them using Z-Botan as a reference. This should tell us a lot about the viability of this trajectory, without having to update dozens of modules with hundreds of bindings all at the same time. If it goes well, we can continue pulling bindings over from Z-Botan until we are done.

I am of course open to suggestions, but will otherwise continue on this course as time permits.

4 Likes
#87

3 posts were split to a new topic: Botan bindings devlog