4 ms·

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 vari

by amalcon 13y ago

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.

quasque 13y ago
Could you elaborate on how lazy evaluation is problematic for such a project?
- chongli 13y ago
  Nope. This is a common troll whenever any Haskell project is mentioned. It's despicable FUD and just plain wrong. Haskell makes it very easy and lightweight to add strictness annotations to your data structures; far, far easier than it is to add laziness to a strict-by-default language.
- bvttf 13y ago
  Not him, but I don't think the regular lazy evaluation worry about building up a million thunks and GC hell would be as much of a problem as it being awkward to not have things happen too fast and leave side channel attacks from timing.
- amalcon 13y ago
  In cryptography, for most operations, you need to be sure that the operation takes the same amount of time for all possible inputs. Otherwise, you leak information. The classic example of this is checking string equality with strncmp(): this takes a different amount of time depending on how similar the strings are. If one string is secret and the other is controlled by an attacker, the attacker can use a clock and multiple attempts to discover the secret. Obviously this particular one isn't relevant to SSL, but there are a number of other possibilities to worry about in most languages, most obviously short-circuiting operations like boolean AND/OR. Lazy evaluation makes every operation short-circuit, so you need to worry about this in every operation. It can be done, but it's harder than it needs to be.
  - automatthew 13y ago
    So we should choose the approach that gives us trivial attacks that reveal 64K straight out of Compton to the approach that may be slightly harder to defend against timing attacks?
    - deleted 13y ago
      [deleted]
    - amalcon 13y ago
      This is such an obvious false dichotomy that I'm sure most people will notice, but I'm pointing it out anyway. We could use something that gives both advantages, like the OCaml I already mentioned. Or, we could take a hybrid approach, where something like Haskell generates C code that provably can't have buffer problems. Or, we could statically verify that the library is written in a known-memory-safe subset of C++. Or, we could use a language like Rust, which (once it's eventually complete) seems ideal for this sort of application.
      - dllthomas 13y ago
        I think the "define a strict, branchless DSL" approach is the right one, if you're going with Haskell. Then use the type system to ensure that only that stuff can touch key data. No problems with laziness or timing attacks, if the core of that is implemented correctly.
Hemospectrum 13y ago
Lazy evaluation is the default in Haskell, but that doesn't mean strict evaluation is unavailable. Here's an example of a type definition that specifies strict evaluation https://github.com/vincenthz/hs-tls/blob/master/core/Network/TLS/Record/State.hs#L39 https://github.com/vincenthz/hs-tls/blob/master/core/Network... See? They don't have to switch languages after all.
- amalcon 13y ago
  This is an excellent point, and I didn't mean to imply that it's impossible to implement TLS securely in Haskell (though my original comment did seem to; I plan to fix that shortly). Only that there are more natural choices that give the same primary advantage (a strong algebraic type system).
codygman 13y ago
Why don't you test the library before making assumptions about it's runtime characteristics. How about doing the slightest bit of research on the creator?
codygman 13y ago
Simple(ish) example of using strictness annotations with folds: http://www.haskell.org/haskellwiki/Foldr_Foldl_Foldl%27 http://www.haskell.org/haskellwiki/Foldr_Foldl_Foldl%27
edwintorok 13y ago
There is a TLS implementation in OCaml in progress, it still has a long way to go though: https://github.com/mirleft/ocaml-tls https://github.com/mirleft/ocaml-tls

by amalcon 13y ago

quasque 13y ago

Could you elaborate on how lazy evaluation is problematic for such a project?

chongli 13y ago
Nope. This is a common troll whenever any Haskell project is mentioned. It's despicable FUD and just plain wrong. Haskell makes it very easy and lightweight to add strictness annotations to your data structures; far, far easier than it is to add laziness to a strict-by-default language.
bvttf 13y ago
Not him, but I don't think the regular lazy evaluation worry about building up a million thunks and GC hell would be as much of a problem as it being awkward to not have things happen too fast and leave side channel attacks from timing.
amalcon 13y ago
In cryptography, for most operations, you need to be sure that the operation takes the same amount of time for all possible inputs. Otherwise, you leak information. The classic example of this is checking string equality with strncmp(): this takes a different amount of time depending on how similar the strings are. If one string is secret and the other is controlled by an attacker, the attacker can use a clock and multiple attempts to discover the secret. Obviously this particular one isn't relevant to SSL, but there are a number of other possibilities to worry about in most languages, most obviously short-circuiting operations like boolean AND/OR. Lazy evaluation makes every operation short-circuit, so you need to worry about this in every operation. It can be done, but it's harder than it needs to be.
- automatthew 13y ago
  So we should choose the approach that gives us trivial attacks that reveal 64K straight out of Compton to the approach that may be slightly harder to defend against timing attacks?
  - deleted 13y ago
    [deleted]
  - amalcon 13y ago
    This is such an obvious false dichotomy that I'm sure most people will notice, but I'm pointing it out anyway. We could use something that gives both advantages, like the OCaml I already mentioned. Or, we could take a hybrid approach, where something like Haskell generates C code that provably can't have buffer problems. Or, we could statically verify that the library is written in a known-memory-safe subset of C++. Or, we could use a language like Rust, which (once it's eventually complete) seems ideal for this sort of application.
    - dllthomas 13y ago
      I think the "define a strict, branchless DSL" approach is the right one, if you're going with Haskell. Then use the type system to ensure that only that stuff can touch key data. No problems with laziness or timing attacks, if the core of that is implemented correctly.

Hemospectrum 13y ago

Lazy evaluation is the default in Haskell, but that doesn't mean strict evaluation is unavailable. Here's an example of a type definition that specifies strict evaluation https://github.com/vincenthz/hs-tls/blob/master/core/Network/TLS/Record/State.hs#L39 https://github.com/vincenthz/hs-tls/blob/master/core/Network... See? They don't have to switch languages after all.

amalcon 13y ago
This is an excellent point, and I didn't mean to imply that it's impossible to implement TLS securely in Haskell (though my original comment did seem to; I plan to fix that shortly). Only that there are more natural choices that give the same primary advantage (a strong algebraic type system).

codygman 13y ago

Why don't you test the library before making assumptions about it's runtime characteristics. How about doing the slightest bit of research on the creator?

codygman 13y ago

Simple(ish) example of using strictness annotations with folds: http://www.haskell.org/haskellwiki/Foldr_Foldl_Foldl%27 http://www.haskell.org/haskellwiki/Foldr_Foldl_Foldl%27

edwintorok 13y ago

There is a TLS implementation in OCaml in progress, it still has a long way to go though: https://github.com/mirleft/ocaml-tls https://github.com/mirleft/ocaml-tls