This isn't a dig at either Haskell or C; the point is that all programming languages and environments have their "gotcha!" moments.
I don't think that laziness makes things much harder. Compare a C function with if foo return 0 in the middle and a Haskell function that lazily builds thunks that don't end up being evaluated in a particular branch. There's obvious things to do to both to make them run in constant time. The hard part about dealing with a timing attack in both cases is recognising that the function is used in such a context and needs to be constant time.
AFAIK, the haskell TLS stack has not yet been audited. For this reason, there's some reluctance to use it in parts of the Haskell community. Although http-conduit and http-client-tls do use it, so everyone writing programs that hit https from haskell using conduit is using it already.
As far as I understand, this is not sufficient.
Some things that are needed in addition are (at least):
* constant time math operations (multiply, divide, exponentiation, etc.)
* no branching based on secrets (running the code results in no branch conditions based on secret data)
Here's an interesting article on implementing a form of Elliptic Curve Cryptography without even local timing attacks: http://blog.cr.yp.to/20140323-ecdsa.html
cryptofunc x = do
begintime <- gettime
result <- purecryptofunc x
endtime <- gettime
sleep (worstcase - (endtime - begintime))
return resultTime to sleep() would vary across processors, os-es, and even load (!), so it's not exactly a workable solution. Not to mention it would be grossly inefficient (Context switch on every crypto primitive? No thanks).
It also seems reasonable to add a random length of time to the sleep time, so that differences in computation time are indistinguisable from the randomness added by the random variable. I could be completely wrong though.
(also, you probably need to force with seq or deepseq the result of purecryptofunc before getting the second time, or you might be adding that evaluation time to another part of the code, and then this code becomes just a constant time added to the computation)
> The software implementation uses S-Boxes, which might suffer for cache timing issues. However do notes that most other known software implementations, including very popular one (openssl, gnutls) also uses similar implementation.
Oh, well if OpenSSL does it..
Timing attacks is the first thing I thought of when I saw this implementation so this should be interesting if he can respond.
Getting around timing attacks is not too different in Haskell from doing the same thing in C. First, there's 2 different classes of timing issues:
1) cryptographic ones
2) and the others (for the lack of better classification)
For cryptographic ones, it's hard to enumerate all the counter measures used/not used, but some examples:
- use of blinding with RSA
- with ghc 7.8, exponiantiation is using GMP expmod_safe
- AES is using native instruction when possible.
- Use of scrubbed memory/memory constant where possible
- some lowlevel cryptographic implementations are actually in C (hash, aes, ..)
Also, while I'm linking against specific set of cryptographic implementations by default, there's nothing preventing anyone from pulling different crypto implementations from other places.
For the other issues, it's usually just a deal of strictness, and not bailing/notifying error too early. (e.g. This is what Bleinchenbacher and CRIME are all about).
- data comparaison is time constant by comparing all bytes where necessary: prevent padding attack
- there's routines to evaluate boolean values without bailing too early (False && ... -> would bail at the first false)
- lots of part in tls is using strict bytestring, and strict values.
- the GC is adding a lot of noise potentially hiding timing issues, potentially exacerbated by pure values instead of mutable values (like you would in C)
Also, I don't want to claim there's no issues or ever will be. Hopefully there's no such things, but I welcome any audits and questions about stuff that look fishy. But people shouldn't only looks at the cryptographic side of security; openssl had so many issues about basic unchecked values, buffer underflow, overflow that's not even funny anymore. Just sayin'
Likely this work would be necessary to "prove" (not in the strict form) your assumptions about constant-time anyway.
There's two reasons for this... first, a pure-Haskell solution locks it to Haskell only, as there's very little realistic chance of embedding Haskell in any other environment. Having it compile to something like straight assembler or LLVM means that we can almost certainly wrap that in almost any runtime environment effectively. (We might require a bit of new SWIG-like tech to do it, but under the circumstances it would probably be worth it.) To the extent that's not a true statement, imagine that I will research and find the correct level of abstraction. (Maybe it really is C.)
Second, with all due respect to the Haskell runtimes in the world, it's just too big a surface to secure. People are asserting here in this thread that you could avoid side-channel attacks in the Haskell runtime, but how would you prove that? To any degree?
Theoretically, you might be even better off in a real proof language, but it's not clear to me that any of them have a good enough extraction-to-LLVM/assembler story.
This would, in theory, produce a solution that should be embeddable in nearly any other language, and indeed, even in embedded environments, while still leveraging the strengths of Haskell's expressiveness and type safety to build a very safety-critical library. We would also be able to write some powerful tests to verify that the putative time-invariant operations really are time-invariant. My strong suspicion is that we'd discover some processor differences here that would surprise everybody.
http://www.haskell.org/ghc/docs/7.4.1/html/users_guide/bang-...
(The similarly looking BangPatterns extension is supported by GHC only.)
This whole thing has got me curious about techniques for formally verifying software.
I'm a complete beginner on this topic, but I assume there are tools to help write software that's formally verified / proven to be correct. Can they make any guarantees about side-channel aspects such as timing in these systems? Anyone care to give me some pointers on where to begin?
A glance over the modelling doesn't seem to preclude using a model checker like http://www.event-b.org/ for it though.
The challenge comes in when you try to translate. You write your model up and validate your approach, you then try to translate it into C (or whatever) and that point you can be as certain of your design as you like, you still can't be sure that the compiled software will work properly. I haven't seen a convincing solution to that particular problem (and I've done some research on the topic for three separate projects now).
At this point, gcc and clang should at least provide constant time memcmp primitives; any custom solution not supported by the compiler is not portable and needs to be validated separately for each implementation, each platform, each compiler version.