A number of people are suggesting that this Haskell implementation must be worse than OpenSSL. It probably is. Writing good crypto code is hard. There are probably bugs.
Many are saying that one problem with Haskell is that you can't eliminate side-channel attacks due to features of the language. I disagree. There is no common language better than Haskell at encoding invariants in the type system. One could, for example, implement a "biggishnum" library in Haskell using large but fixed size integers and constant-time operations.
Free monads are a powerful idea in Haskell[1]. They allow one to easily generalize "interpreters" over sequences of commands. In Haskell, more-so than any other language I've ever used, one can decouple execution from algorithm specification.
Free applicative functors generalize further[2]. They define a computational structure that must be fixed a priori. That is, by definition a free applicative functor cannot know the state of the data during its execution.
There are some problems with this. Applicative functors have an operation which can lift regular functions into it. That operation would have to be hidden, so that only a kernel was exposed that offered the ability to initialize data, and then perform computations upon it.
But it's possible to do this. It is actually not a radical idea to imagine this being done in Haskell. Making a library and a set of primitive operations that can be used by an end user safely, in provably constant time is possible.
> Many are saying that one problem with Haskell is that you can't eliminate side-channel attacks due to features of the language. I disagree. There is no common language better than Haskell at encoding invariants in the type system. One could, for example, implement a "biggishnum" library in Haskell using large but fixed size integers and constant-time operations.
Why do you disagree?
Timing attacks are probably the easiest kind of side channel attacks to prevent but CPU cache line eviction and branch prediction are a lot more difficult to deal with. Especially when using a programming language with managed memory where you can't be quite sure what kind of memory accesses a program will perform. And in the days of virtual machines on cloud servers, they are very relevant.
I do not think that it is totally impossible to write Haskell crypto code without any side channels, it is certainly more difficult than writing crypto code in C or Assembler.
But the big problem is that now you'd need the programmers dealing with crypto not only to be proficient cryptographers but also experts on the internals of the Haskell runtime system. That's a pretty tall order.
I would like to hear from the original authors of this library, what was their motivation in starting this project? I am sure they were not unaware of the potential of side channel attacks. I don't think this project was started with the intention of replacing OpenSSL in production use, but perhaps for fun or educational purposes. Or perhaps to write offline tools for creating and validating certificates, etc.
I'm wondering about a situation where forgetting a strictness annotation is the analogous Haskell situation of forgetting to bounds-check some input. There are lots of ways in Haskell for something not to be evaluated. (No, the simple fixes like 'use strict fields' do not cover all cases.) To put all of them behind a free monad seems like it would be giving up a lot.
In C you could have made some 'safe buffer' struct together with some safe set of functions. But people didn't do that.
> A number of people are suggesting that this Haskell implementation must be worse than OpenSSL. It probably is. Writing good crypto code is hard. There are probably bugs.
Ok, but if it were vetted as much as openssl, it would probably be much better, yes?
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.
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.
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.
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 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.
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.
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?
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.
From the website, it seems that they proved that their implementation is correct with respect to their formalization of the interfaces in the RFCs. That is, their implementation is logically correct.
However, this says nothing about whether or not the implementation is secure. They admit that they don't model time in their proofs, so I doubt their implementation is free of timing attacks. Moreover, its written in F#, so you have to trust your CLI implementation to be bug-free as well.
I'm completely ignorant about Haskell. I see there's some code in a "Benchmarks" folder; I think it would be highly interesting to see a comparison in speed between OpenSSL's SSL implementation and this one (the operations that a web server would normally have to do).
Can anyone make that happen? I can't even figure out how to execute Haskell code in Ubuntu 13.04.
Seems to me like if the code base is 20 times smaller than OpenSSL, and we can assess whether timing attacks are present or not -- and if they are, replace the timing critical code with C code, perhaps -- that this would be a real alternative to OpenSSL. Am I being unrealistic in thinking this? Not that everyone will adopt it, mind you, but that adopting it would be a wise thing to do?
You can install development packages through the "cabal" command line tool. The REPL environment is "ghci".
On one hand, it is a very high performance language with tons of purity, abstraction, and invariants built in to the type system and semantics. On the other hand, certain aspects can be problematic to reason about.
The big difficulty in adopting it in any current codebase is that most current pieces of software are not written in haskell. The huge advantage of projects in C like OpenSSL is that you can produce platform-native shared libraries that can be used easily from any other language.
A bit of research shows that it's possible to make shared libraries with haskell, but not quite as straightforward to use them. I have no practical experience about how troublesome it would actually be.
If you're curious (like I was) if anything else in the Haskell ecosystem is using this, this page lists packages that have dependencies on tls in Hackage (the Haskell package repository). There are 26 packages that depend on tls.
Nice and everything, but I somehow cannot imagine people massively jump over it. Maybe it's superstitious, I dunno…
On the other hand, I undoubtedly agree that we should start making and deploying alternatives in more safe modern languages. In fact, I guess we should start step-by-step rewriting everything that's written in C/C++ and OpenSSL is a good thing to start with.
Crypto poses a unique challenge with the threat of timing attacks. A major benitif of using low level languages is that it is easier to assure that your code takes constant time regardless of the input.
Why rewrite C and C++ parts? Just because someone doesn't program properly in one language doesn't mean you need to rewrite everything written in that language. Bit like throwing the baby out with the bathwater.
The response to a subtle weakness in cryptographic software should not be to reimplement the cryptographic implementation from scratch. This inevitably introduces far more problems than it solves.
Heartbleed is not exactly a "subtle weakness," it is a gaping hole -- and it is a gaping hole that is only possible in languages with simple pointers and simple pointer arithmetic. In other words, using better languages for the next generation of crypto implementations will prevent this from happening, and then we can all get back to worrying about subtle weaknesses.
I'd rather say that the long list of overflow-related vulnerabilities would be a good argument to ensure that all crypto libraries are implemented in some kind of a strict language that disallows a large class of vulnerabilities, even if it costs us some time and effort.
Seriously, for many languages bugs cause unintended behavior within bounds of implemented logic - such as the recent logic bug that returned an 'okay' response even if the certificate was invalid; however, the fact that ordinary bugs tend to have effects of "read arbitrary memory" or "execute arbitrary code" is a very specific niche of C and friends.
In a language appropriate for security, a bug in heartbeat extension would break the heartbeat extension - maybe disable heartbeats not work, maybe cause different heartbeats - but it should be unable to affect the rest of application. In a language appropriate for security, if a single module is secure (i.e., the limited number of API/method calls it exposes are secure), then bugs in all other modules shouldn't be able to affect the insides of that module; so if your app has a tiny core that does some signing w/o exposing the key secrets, then the rest of the app can't touch it even deliberately, much less by an acidental bug.
Haskell is a particularly odd choice for a project like this, as lazy evaluation makes it difficult to reason about the runtime of various operations under various conditions.
Something with a bit more ML in its blood would be better, and for a library that pretty much means OCaml.
Edit: I do not at all mean to imply that it is impossible to implement TLS securely in Haskell. Only that there are more natural choices if one wants the advantage of a strong algebraic type system.
Why? Go doesn't really offer a whole lot in terms of security, except for better managed memory. I'm not even sure you could reliably eliminate side channel attacks in Go.
Bad. They are not something to blow off. They may seem "out there", but they are actually leveraged somewhat frequently. They are particularly dangerous in certain shared-hardware environments (e.g. VPS services like DigitalOceal, AWS, etc), and against physical devices that are supposed to resist data extraction (like smart cards).
When you're talking about something used to secure as much sensitive data for as many people as TLS/SSL, timing and side channel attacks are very important. Any little flaw can lead to information exposure such that people are put into danger.
[+] [-] AaronFriel|12 years ago|reply
Many are saying that one problem with Haskell is that you can't eliminate side-channel attacks due to features of the language. I disagree. There is no common language better than Haskell at encoding invariants in the type system. One could, for example, implement a "biggishnum" library in Haskell using large but fixed size integers and constant-time operations.
Free monads are a powerful idea in Haskell[1]. They allow one to easily generalize "interpreters" over sequences of commands. In Haskell, more-so than any other language I've ever used, one can decouple execution from algorithm specification.
Free applicative functors generalize further[2]. They define a computational structure that must be fixed a priori. That is, by definition a free applicative functor cannot know the state of the data during its execution.
There are some problems with this. Applicative functors have an operation which can lift regular functions into it. That operation would have to be hidden, so that only a kernel was exposed that offered the ability to initialize data, and then perform computations upon it.
But it's possible to do this. It is actually not a radical idea to imagine this being done in Haskell. Making a library and a set of primitive operations that can be used by an end user safely, in provably constant time is possible.
[1] http://www.haskellforall.com/2012/06/you-could-have-invented... [2] http://paolocapriotti.com/assets/applicative.pdf
[+] [-] exDM69|12 years ago|reply
Why do you disagree?
Timing attacks are probably the easiest kind of side channel attacks to prevent but CPU cache line eviction and branch prediction are a lot more difficult to deal with. Especially when using a programming language with managed memory where you can't be quite sure what kind of memory accesses a program will perform. And in the days of virtual machines on cloud servers, they are very relevant.
I do not think that it is totally impossible to write Haskell crypto code without any side channels, it is certainly more difficult than writing crypto code in C or Assembler.
But the big problem is that now you'd need the programmers dealing with crypto not only to be proficient cryptographers but also experts on the internals of the Haskell runtime system. That's a pretty tall order.
I would like to hear from the original authors of this library, what was their motivation in starting this project? I am sure they were not unaware of the potential of side channel attacks. I don't think this project was started with the intention of replacing OpenSSL in production use, but perhaps for fun or educational purposes. Or perhaps to write offline tools for creating and validating certificates, etc.
[+] [-] cynicalkane|12 years ago|reply
In C you could have made some 'safe buffer' struct together with some safe set of functions. But people didn't do that.
[+] [-] freyrs3|12 years ago|reply
There are a few uncommon dependently typed ones with code extraction to other languages though. Though doing so is fairly time intensive still.
[+] [-] orblivion|12 years ago|reply
Ok, but if it were vetted as much as openssl, it would probably be much better, yes?
[+] [-] klrr|12 years ago|reply
[+] [-] chimeracoder|12 years ago|reply
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
[+] [-] joeyh|12 years ago|reply
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.
[+] [-] codygman|12 years ago|reply
Timing attacks is the first thing I thought of when I saw this implementation so this should be interesting if he can respond.
[+] [-] jerf|12 years ago|reply
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.
[+] [-] gamegoblin|12 years ago|reply
http://www.haskell.org/ghc/docs/7.4.1/html/users_guide/bang-...
[+] [-] tga_d|12 years ago|reply
[+] [-] dhotson|12 years ago|reply
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?
[+] [-] pintor|12 years ago|reply
[+] [-] carterschonwald|12 years ago|reply
[+] [-] johnbender|12 years ago|reply
http://www.mitls.org/wsgi
[+] [-] jude-|12 years ago|reply
However, this says nothing about whether or not the implementation is secure. They admit that they don't model time in their proofs, so I doubt their implementation is free of timing attacks. Moreover, its written in F#, so you have to trust your CLI implementation to be bug-free as well.
[+] [-] dyoder|12 years ago|reply
[+] [-] runeks|12 years ago|reply
I'm completely ignorant about Haskell. I see there's some code in a "Benchmarks" folder; I think it would be highly interesting to see a comparison in speed between OpenSSL's SSL implementation and this one (the operations that a web server would normally have to do).
Can anyone make that happen? I can't even figure out how to execute Haskell code in Ubuntu 13.04.
Seems to me like if the code base is 20 times smaller than OpenSSL, and we can assess whether timing attacks are present or not -- and if they are, replace the timing critical code with C code, perhaps -- that this would be a real alternative to OpenSSL. Am I being unrealistic in thinking this? Not that everyone will adopt it, mind you, but that adopting it would be a wise thing to do?
[+] [-] kazagistar|12 years ago|reply
On one hand, it is a very high performance language with tons of purity, abstraction, and invariants built in to the type system and semantics. On the other hand, certain aspects can be problematic to reason about.
[+] [-] tene|12 years ago|reply
A bit of research shows that it's possible to make shared libraries with haskell, but not quite as straightforward to use them. I have no practical experience about how troublesome it would actually be.
[+] [-] jcurbo|12 years ago|reply
http://packdeps.haskellers.com/reverse/tls
Meanwhile, HsOpenSSL (Haskell bindings for OpenSSL) has 22 dependencies:
http://packdeps.haskellers.com/reverse/HsOpenSSL
[+] [-] krick|12 years ago|reply
On the other hand, I undoubtedly agree that we should start making and deploying alternatives in more safe modern languages. In fact, I guess we should start step-by-step rewriting everything that's written in C/C++ and OpenSSL is a good thing to start with.
I guess it's a good chance for Rust & friends.
[+] [-] gizmo686|12 years ago|reply
[+] [-] 72deluxe|12 years ago|reply
[+] [-] kylemaxwell|12 years ago|reply
[+] [-] betterunix|12 years ago|reply
[+] [-] thinkpad20|12 years ago|reply
[+] [-] PeterisP|12 years ago|reply
Seriously, for many languages bugs cause unintended behavior within bounds of implemented logic - such as the recent logic bug that returned an 'okay' response even if the certificate was invalid; however, the fact that ordinary bugs tend to have effects of "read arbitrary memory" or "execute arbitrary code" is a very specific niche of C and friends.
In a language appropriate for security, a bug in heartbeat extension would break the heartbeat extension - maybe disable heartbeats not work, maybe cause different heartbeats - but it should be unable to affect the rest of application. In a language appropriate for security, if a single module is secure (i.e., the limited number of API/method calls it exposes are secure), then bugs in all other modules shouldn't be able to affect the insides of that module; so if your app has a tiny core that does some signing w/o exposing the key secrets, then the rest of the app can't touch it even deliberately, much less by an acidental bug.
[+] [-] thisisdave|12 years ago|reply
Minor edit: almost four years
[+] [-] chongli|12 years ago|reply
Could you elaborate more on this? I fail to see how this is inevitable.
[+] [-] amalcon|12 years ago|reply
Something with a bit more ML in its blood would be better, and for a library that pretty much means OCaml.
Edit: I do not at all mean to imply that it is impossible to implement TLS securely in Haskell. Only that there are more natural choices if one wants the advantage of a strong algebraic type system.
[+] [-] aalpbalkan|12 years ago|reply
Go is probably better at this.
[+] [-] somethingnew|12 years ago|reply
[+] [-] wyager|12 years ago|reply
Why? Go doesn't really offer a whole lot in terms of security, except for better managed memory. I'm not even sure you could reliably eliminate side channel attacks in Go.
[+] [-] dscrd|12 years ago|reply
[+] [-] msie|12 years ago|reply
[+] [-] wyager|12 years ago|reply
Bad. They are not something to blow off. They may seem "out there", but they are actually leveraged somewhat frequently. They are particularly dangerous in certain shared-hardware environments (e.g. VPS services like DigitalOceal, AWS, etc), and against physical devices that are supposed to resist data extraction (like smart cards).
[+] [-] 001spartan|12 years ago|reply
[+] [-] brohee|12 years ago|reply
[+] [-] developer786|12 years ago|reply
[+] [-] pekk|12 years ago|reply
[+] [-] chrisdone|12 years ago|reply
[+] [-] jacobwcarlson|12 years ago|reply