5
$\begingroup$

I've recently discovered a potential vulnerability in the type system of Haskell, a functional programming language in use in critical applications at Facebook, Standard Chartered, Input Output et cetera. For context, Haskell's type system distinguishes functions which don't have side effects such as add :: Int -> Int -> Int from functions which do such as putStrLn :: String -> IO () in order to reduce the risk of bugs from unexpected side effects. There are escape hatches such as unsafePerformIO :: IO a -> a, but the user can disallow them using a pragma. In theory this should allow one to use pure functions from third-party modules without fear; the worst thing a pure function should be able to do is run out of memory or diverge, not encrypt your files for example.

The Haskell side of the attack isn't relevant to crypto, but in brief: if one can find two Haskell datatype names with a colliding MD5 hash, one can break the type system in the "safe" subset of the language, coerce between any two types and perform side effects in "pure" code. That could enable malicious package authors to launch supply chain attacks, made more devastating by the type system providing an illusion of safety.

Datatype names are strings starting with an uppercase letter and followed by any number of alphanumeric characters, _ or '. Marc Stevens found a colliding pair of such strings https://x.com/realhashbreaker/status/1770161965006008570, but fortunately Haskell applies a nonstandard string encoding before hashing. The encoding expands each (unicode) code point to 4 bytes in big-endian order; since unicode only goes up to 0x10ffff, that means the first byte is always 0. Furthermore, since only about 100,000 unicode characters are alphanumeric, one is restricted to about 17 bits of entropy per 32 bits of bytestring.

A concrete example:

The string "ab" is encoded to the bytestring 0000006100000062, which hashes to 6fdc87b2b00d3283ee55bc17ca1466b0.

Would it be viable to find a collision of encoded strings in that format? I've looked at Hashclash, but it seems to only support one-byte alphabets.

$\endgroup$
6
  • 1
    $\begingroup$ Why would you guess that it might be less viable with this character encoding than with other character encodings? Doesn't intuitively look like it'd make any difference to me. $\endgroup$
    – n-l-i
    Commented Oct 10 at 16:27
  • $\begingroup$ Perhaps I should've asked how easy it would be instead. I've looked into whether a brute force birthday attack would be economically feasible and it looks like no. The issue then (as I understand it) is how easily existing differential path attacks could be adapted to the encoding. But since they require precise control of individual bytes, that might be difficult since the constraint on 4-byte segments is quite restrictive. I corresponded with Stevens abt it and he said 8 bits of available entropy/32b would be too little, but I've managed to increase it to ~17 since then. $\endgroup$ Commented Oct 10 at 16:57
  • $\begingroup$ I've looked into differential paths, but I'm no expert on them and can't really assess how easy adapting them would be. If it is easy, great - this could become a pretty cool paper imo. $\endgroup$ Commented Oct 10 at 16:59
  • $\begingroup$ Thanks for the clarification! $\endgroup$
    – n-l-i
    Commented Oct 10 at 17:11
  • $\begingroup$ So Haskell uses MD5 for abbreviation of type names? $\endgroup$
    – DannyNiu
    Commented Oct 11 at 3:52

2 Answers 2

4
$\begingroup$

Update: I contacted the Haskell security response team and they'll be fixing this, most likely by swapping out MD5 for a secure hash function. At that point, whether an MD5 collision can be found will be a moot point on systems running up-to-date versions of GHC (Haskell's main compiler).

Furthermore, even if a collision can be found this is a bug rather than a vulnerability per se. While the Haskell wiki currently states "Safe Haskell infers that untrusted code inferred safe and not in IO can be run without fear (aside from fear of resource over-utilization/exhaustion)." [1] that is not true! The Safe Haskell paper [2] may have had the lofty goal of allowing safe execution of malicious code, but it doesn't guarantee that in practice and GHC's maintainers advise against using Safe Haskell for security.

Interested readers can find the discussion on whether to fix or deprecate Safe Haskell here. For now, Haskell developers who wish to run third-party code without fear should either read it or use sandboxing tools outside the Haskell language.

[1] https://wiki.haskell.org/Safe_Haskell

[2] Jones, S.P., 2012, September. Safe haskell. In Haskell'12: Proceedings of the Fifth ACM SIGPLAN Symposium on Haskell. https://www.microsoft.com/en-us/research/publication/safe-haskell/

$\endgroup$
0
$\begingroup$

While some quick ways to find MD5 collisions rely on full control on input data, the way Haskell implement type name abbreviation is definitely problematic if not vulnerable.

Note that, CVEs have scores! Even though currently, there's no known exploitation, getting a low-score CVE and motivate Haskell to change is in my opinion an utmost priority. Recommend them to use BLAKE-2s which supports 160 and 128 bits output (160 is intended by BLAKE team for use in git, and 128-bit is actually slightly faster than MD5)

$\endgroup$
1
  • $\begingroup$ Alright, I'll figure out how to do so ASAP then! $\endgroup$ Commented Oct 11 at 9:40

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.