5 ms·

While Haskell mitigates or eliminates some classes of bugs common in C (such as buffer overflow), it also makes it more difficult to guard against side-channel

While Haskell mitigates or eliminates some classes of bugs common in C (such as buffer overflow), it also makes it more difficult to guard against side-channel attacks like timing attacks[0], because lazy evaluation makes it more difficult to reason about the actual behavior of the code at runtime. This isn't a dig at either Haskell or C; the point is that all programming languages and environments have their "gotcha!" moments. [0] https://en.wikipedia.org/wiki/Timing_attack https://en.wikipedia.org/wiki/Timing_attack

pintor 13y ago
Maybe Rust will provide the right balance between the two.
- kzrdude 13y ago
  No programming language seems to provide primitives for constant-time algorithms. 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.
  - kivikakk 13y ago
    http://golang.org/pkg/crypto/subtle/ http://golang.org/pkg/crypto/subtle/
    - sseveran 13y ago
      Package subtle implements functions that are often useful in cryptographic code but require careful thought to use correctly.
- awda 13y ago
  whoosh!
codygman 13y ago
Perhaps it would be more interesting to discuss how the author of the Haskell TLS/SSL library gets around timing attacks. Actually I have him on twitter... paging @vincenthz. Timing attacks is the first thing I thought of when I saw this implementation so this should be interesting if he can respond.
- vhz 13y ago
  (author here) 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'
  - TheLoneWolfling 13y ago
    How do you prevent the compiler optimizing constant-time operations into non-constant time?
joeyh 13y ago
http://hackage.haskell.org/package/securemem implements http://hackage.haskell.org/package/securemem implements constant-time bytestring comparisons for haskell. With the bonus that the data is scrubbed when GC'd. This is used by parts of the haskell TLS stack, for example http://hackage.haskell.org/package/cipher-aes http://hackage.haskell.org/package/cipher-aes 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.
- runeks 13y ago
  > http://hackage.haskell.org/package/securemem http://hackage.haskell.org/package/securemem implements constant-time bytestring comparisons for haskell. With the bonus that the data is scrubbed when GC'd. 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 http://blog.cr.yp.to/20140323-ecdsa.html
  - dpatru 13y ago
    Why can't timing be handled external to the scrambling or descrambling operations? Look at the time, do the crypto, then check the time and sleep as necessary so that this particular operation takes about as much time as the worse-case. Something like: cryptofunc x = do begintime <- gettime result <- purecryptofunc x endtime <- gettime sleep (worstcase - (endtime - begintime)) return result
tga_d 13y ago
Exactly the first thing I thought. There are plenty of side-channels in cryptographic code that require access to somewhat low-level hardware to fix (e.g. the acoustic attack on GPG that got plenty of press), and I don't see how you can address those without e.g. inline C or something else that negates the advantages of using Haskell.
- chrisdone 13y ago
  FWIW inline C doesn't negate the advantages of using Haskell. It's inline.
gamegoblin 13y ago
GHC allows you to force fields to be strict rather than lazy. http://www.haskell.org/ghc/docs/7.4.1/html/users_guide/bang-patterns.html http://www.haskell.org/ghc/docs/7.4.1/html/users_guide/bang-...
- quchen 13y ago
  Strict fields are actually standard Haskell, http://www.haskell.org/onlinereport/haskell2010/haskellch4.html#x10-710004.2.1 http://www.haskell.org/onlinereport/haskell2010/haskellch4.h... (The similarly looking BangPatterns extension is supported by GHC only.)
dhotson 13y ago
The first thing I searched for in the README was "constant time". 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?
- runeks 13y ago
  This blog post isn't about writing automated tools to detect timing attacks in code, but it has a lot of stuff about how to write crypto code -- elliptic curve cryptography in particular -- that is impervious to timing attacks, very interesting if you ask me: http://blog.cr.yp.to/20140323-ecdsa.html http://blog.cr.yp.to/20140323-ecdsa.html
- ElliotH 13y ago
  http://scholar.google.co.uk/scholar?q=%22timing+attack%22+%22formal+methods%22+OR+%22formal+verification%22&btnG=&hl=en&as_sdt=0%2C5 http://scholar.google.co.uk/scholar?q=%22timing+attack%22+%2... turns up some papers that consider this. They don't seem to provide much by way of tooling though. A glance over the modelling doesn't seem to preclude using a model checker like http://www.event-b.org/ 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).
jerf 13y ago
If I were handed a few million dollars and told to go create an SSL implementation, my approach would be to write the implementation in Haskell in a way that compiles down to LLVM or, possibly, assembler, which is then what the project would distribute. Haskell's type system can be used for all the juicy goodness being described in the other comments, but it would not be running in the Haskell runtime. See: http://hackage.haskell.org/package/atom http://hackage.haskell.org/package/atom which goes to C; in principle it's not hard to imagine then how you'd go to another target. 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.
carterschonwald 13y ago
Don't make shit up. It'd very easy to write totally strict code in Haskell. It's even possible to write code that won't yield to the run time system for a constant time op.

pintor 13y ago

Maybe Rust will provide the right balance between the two.

kzrdude 13y ago
No programming language seems to provide primitives for constant-time algorithms. 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.
- kivikakk 13y ago
  http://golang.org/pkg/crypto/subtle/ http://golang.org/pkg/crypto/subtle/
  - sseveran 13y ago
    Package subtle implements functions that are often useful in cryptographic code but require careful thought to use correctly.
awda 13y ago
whoosh!

codygman 13y ago

Perhaps it would be more interesting to discuss how the author of the Haskell TLS/SSL library gets around timing attacks. Actually I have him on twitter... paging @vincenthz. Timing attacks is the first thing I thought of when I saw this implementation so this should be interesting if he can respond.

vhz 13y ago
(author here) 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'
- TheLoneWolfling 13y ago
  How do you prevent the compiler optimizing constant-time operations into non-constant time?

joeyh 13y ago

http://hackage.haskell.org/package/securemem implements http://hackage.haskell.org/package/securemem implements constant-time bytestring comparisons for haskell. With the bonus that the data is scrubbed when GC'd. This is used by parts of the haskell TLS stack, for example http://hackage.haskell.org/package/cipher-aes http://hackage.haskell.org/package/cipher-aes 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.

runeks 13y ago
> http://hackage.haskell.org/package/securemem http://hackage.haskell.org/package/securemem implements constant-time bytestring comparisons for haskell. With the bonus that the data is scrubbed when GC'd. 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 http://blog.cr.yp.to/20140323-ecdsa.html
- dpatru 13y ago
  Why can't timing be handled external to the scrambling or descrambling operations? Look at the time, do the crypto, then check the time and sleep as necessary so that this particular operation takes about as much time as the worse-case. Something like: cryptofunc x = do begintime <- gettime result <- purecryptofunc x endtime <- gettime sleep (worstcase - (endtime - begintime)) return result

tga_d 13y ago

Exactly the first thing I thought. There are plenty of side-channels in cryptographic code that require access to somewhat low-level hardware to fix (e.g. the acoustic attack on GPG that got plenty of press), and I don't see how you can address those without e.g. inline C or something else that negates the advantages of using Haskell.

chrisdone 13y ago
FWIW inline C doesn't negate the advantages of using Haskell. It's inline.

gamegoblin 13y ago

GHC allows you to force fields to be strict rather than lazy. http://www.haskell.org/ghc/docs/7.4.1/html/users_guide/bang-patterns.html http://www.haskell.org/ghc/docs/7.4.1/html/users_guide/bang-...

quchen 13y ago
Strict fields are actually standard Haskell, http://www.haskell.org/onlinereport/haskell2010/haskellch4.html#x10-710004.2.1 http://www.haskell.org/onlinereport/haskell2010/haskellch4.h... (The similarly looking BangPatterns extension is supported by GHC only.)

dhotson 13y ago

The first thing I searched for in the README was "constant time". 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?

runeks 13y ago
This blog post isn't about writing automated tools to detect timing attacks in code, but it has a lot of stuff about how to write crypto code -- elliptic curve cryptography in particular -- that is impervious to timing attacks, very interesting if you ask me: http://blog.cr.yp.to/20140323-ecdsa.html http://blog.cr.yp.to/20140323-ecdsa.html
ElliotH 13y ago
http://scholar.google.co.uk/scholar?q=%22timing+attack%22+%22formal+methods%22+OR+%22formal+verification%22&btnG=&hl=en&as_sdt=0%2C5 http://scholar.google.co.uk/scholar?q=%22timing+attack%22+%2... turns up some papers that consider this. They don't seem to provide much by way of tooling though. A glance over the modelling doesn't seem to preclude using a model checker like http://www.event-b.org/ 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).

jerf 13y ago

If I were handed a few million dollars and told to go create an SSL implementation, my approach would be to write the implementation in Haskell in a way that compiles down to LLVM or, possibly, assembler, which is then what the project would distribute. Haskell's type system can be used for all the juicy goodness being described in the other comments, but it would not be running in the Haskell runtime. See: http://hackage.haskell.org/package/atom http://hackage.haskell.org/package/atom which goes to C; in principle it's not hard to imagine then how you'd go to another target. 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.

carterschonwald 13y ago

Don't make shit up. It'd very easy to write totally strict code in Haskell. It's even possible to write code that won't yield to the run time system for a constant time op.