6 ms·

Introducing Transport Layer Security in pure OCaml

106 points by tizoc 12y ago

edwintorok 12y ago
Looking at the development history it would appear that this project started in Feb 2014: https://github.com/mirleft/ocaml-tls/commit/10b53cd1ebde036047fb4a0d33261d07ce54432b https://github.com/mirleft/ocaml-tls/commit/10b53cd1ebde0360... . Writing an (almost complete) TLS 1.2 stack in such a short amount of time is amazing! (compared to how long it took for NSS to gain TLS 1.2). Looking forward to the next blogpost in this series.
emillon 12y ago
The work on Mirage is very interesting. If I understand it correctly, it may be possible to run a Xen domain with a Linux application server, and with a TLS reverse proxy in front using another Xen domain (in the form of a unikernel). This would be fantastic and does not change a lot how you run your application, except that you get hardened crypto for free. That's assuming that ocaml-tls has no "high level" bugs (not memory corruption related) of course, but I'm quite sure that it is way easier to review than existing TLS implementations.
- edwintorok 12y ago
  One thing that concerns me is the entropy source in Xen guest domains, but hopefully that'll be worked out for the final version.
  - pqwy 12y ago
    It concerns us too. Right now the entropy in Xen domains is weak, but we are working with the rest of the team to feed some actual environmental noise to keep Fortuna well-fed. You can also run the library on Unix, of course, and there the RNG is periodically seeded from /dev/urandom.
  - avsm 12y ago
    We're putting together a front/backend ring (rndfront/rndback) that will proxy entropy from dom0 directly into the guest. It'll take some time for this to percolate into the public cloud, so we'll need to do what Linux does in the meanwhile (harvest entropy from interrupt timings, attempt RDRAND, and so on). The ENTROPY module type supports this sort of callback in 1.2.0: https://github.com/mirage/mirage/blob/master/types/V1.mli#L75 https://github.com/mirage/mirage/blob/master/types/V1.mli#L7... (If you're interested in contributing, the entropy harvesting is in sore need of more eyes and help!)
    - rwmj 12y ago
      /me grumbles about virtio-rng and reinventing ABIs ...
      - avsm 12y ago
        Dave Scott's added support for a low-bandwidth channel into XL with the intention of reusing virtio-rng (and virtio-serial and friends). http://lists.xen.org/archives/html/xen-devel/2014-06/msg02931.html http://lists.xen.org/archives/html/xen-devel/2014-06/msg0293... On the other hand, I disagree that we're reinventing an ABI given that: 1) virtio isn't the supported PV interface in Xen -- rndfront/back follows the same design principles as net/blk/fb/usb/pci/console etc. 2) The Xen shared-ring interface is older than virtio, and much simpler for pure PV guests such as Mirage (no PCI emulation to worry about). I do wonder what happened to that GSoC project from a few years to add virtio support to Xen though...I don't think any patches ever appeared.
        djs55 12y ago
        s/added/currently trying to add/ :-) For HVM guests I hope that virtio-rng would work as-is (if it could be turned on via the control path). That's definitely worth a look. For PV guests like Mirage I'm currently plumbing through a Xen PV analogue of virtio-serial by hijacking^Wextending the existing PV console support. Since the backend for that is in qemu already it might be possible to hook up the entropy source (with all the rate limiting etc). I think the trick would be to get the guest to recognise the frontend for what it is -- I imagine the virtio-rng device in the guest presents itself as a magic hardware PCI device and 'just works'.
hoggle 12y ago
Are we finally approaching consensus in the field of systems programming that security is more important than performance (thanks to heartbleed)? Or put differently: have we reached the point where computers are fast enough so that we can move on and sacrifice some of those abundant MIPS and extra RAM for much improved clarity in our critical infrastructure code? OCaml could actually be a great choice for maintaining a solid TLS layer.
- pdpi 12y ago
  For the sake of moving things forward: every time we have this discussion, someone always points out that functional languages would make it easier to get correct behaviour from a crypto library, and someone always replies that garbage collection opens you up to side-channel (timing, in this case) attacks.
  - lomnakkus 12y ago
    Isn't even C pretty vulnerable to timing attacks? (I'm thinking primarily through things like L1/L2 cache effects, etc.)
  - hoggle 12y ago
    Interesting, I didn't know that. I always wondered why (non "functional") Ada doesn't get mentioned more often in these kinds of discussions: http://www.adaic.org/advantages/ http://www.adaic.org/advantages/ http://www.seas.gwu.edu/~mfeldman/ada-project-summary.html http://www.seas.gwu.edu/~mfeldman/ada-project-summary.html
    - pgeorgi 12y ago
      And it's "cousin" SPARK, which adds proof capabilities: http://git.codelabs.ch/?p=spark-crypto.git http://git.codelabs.ch/?p=spark-crypto.git
    - e12e 12y ago
      Last time it was brought up, there appeared to be some lingering confusion and issues with how the compiler and runtime was and is licensed. The latest version of Ada is available for a (large) fee from Adacore and for free under the GPL. There is also a version published as part of gcc, that trails the upstream version a little in terms of features -- but like the rest of gcc, the relevant parts are under LGPL, so not all binaries distributed to third parties need be distributed under the GPL, but can be under any licence one choose[1] -- without the need for a commercial licence from Adacore. It would appear the lack of an up-to-date, gratis, version of Ada was a real problem for adoption at some point -- and the impression of Ada being difficult to get access to outside of large contractors put a damper on its popularity (justified or not). [1] The "problem" with a compiler under GPL is that most compilers will have some kind of library code or language runtime that needs to be distributed with resulting binaries, thus forcing all projects to adopt GPL, rather than just the projects that build directly on the compiler.
richardwhiuk 12y ago
It looks like they have some odd cipher suite selection mechanic. https://tls.openmirage.org https://tls.openmirage.org negotiates TLS_RSA_WITH_RC4_128_SHA which is the second worse suite that Chrome 35 will offer by default. If I renegotiate, the server will suggets TLS_RSA_WITH_AES_256_CBC_SHA, so it looks like the server wants to change the cipher later, which seems odd. This means it doesn't support PFS or several other advantages in the newer protocols. I'd be very interested to know about side channel attacks which may be possible in OCaml, as opposed to in another languages - there doesn't seem to be any discussion of them here. They also refer to the Apple Goto fail bug as a memory safety issue - that's not true, it was a programming flaw that could be made in a GCed language. Finally, if I look at the issue tracker I see things like https://github.com/mirleft/ocaml-tls/issues/6 https://github.com/mirleft/ocaml-tls/issues/6 - closed, with no explanation and marked as a security concern - which gives me no confidence that the issue was addressed.
- edwintorok 12y ago
  The blogpost does mention that implementing more cipher suites is a work in progress. Edit: the server uses a random protocol version for testing purposes, so that might explain the odd renegotiations that you observed: https://github.com/mirleft/ocaml-tls/issues/159 https://github.com/mirleft/ocaml-tls/issues/159
- pqwy 12y ago
  Hey, (Disclaimer: one of the authors) We randomize the connection parameters on each connect to help us gauge the stack's behavior with various combinations (see https://github.com/mirleft/ocaml-tls/issues/159 https://github.com/mirleft/ocaml-tls/issues/159 ). Normally it uses first available from the list here: https://github.com/mirleft/ocaml-tls/blob/master/lib/config.ml#L24 https://github.com/mirleft/ocaml-tls/blob/master/lib/config..... (For some reason the RSA variant got on top; it should have been DHE_RSA, which does provide PFS.) Side channel attacks were a very big concern, and I invite you to read the entire series of articles we plan on publishing in the next few days, where we try to lay down our strategy and explain what we know and what we don't. Or even skim through the handshake code and check some of the comments there. We were already warned that CVE-2014-1266 CVE-2014-0224 are not memory safety issues. The article is badly worded there. What was meant is that they are, at least in our pretty firm opinion, issues with C (something we will elaborate in more detail in further articles, but in essence, you get regular control-flow in a functional language and you can encode state machines in a far more explicit manner). Working to update the post and clarify this. As for the issue #6, yes, its closing was not documented too well. This does not mean we didn't expend significant effort to actually address the points there :) . Thank you for the input and please have patience with us. We still have (at least) four more articles to publish!
olifante 12y ago
Security is too damn important to use languages that are insecure by default and that require rigorous discipline and extensive auditing, such as C and C++. The world needs to move its entire crypto and networking layer to functional languages focusing on immutability, thereby immensely reducing the surface of attack.
- jude- 12y ago
  Secure implementations require more than formal, logical correctness. They must also not leak information to adversaries--i.e. the must be free of side-channels. Unfortunately, ensuring this usually requires the developers to be aware of the low-level behavior of the underlying architecture, which is difficult in functional languages since unlike C, they abstract away behaviors of the underlying hardware that can leak information. I suppose you could extend the functional language's type system to tag data as e.g. needing to be compared to other data in constant time, or needing to be accessed in a particular way to avoid cache-timing attacks, and so on, but this just off-loads the problem to the compiler (i.e. the problem must still be addressed, and not in a high-level functional language). But if you're going to go that far, you might as well put the requisite safe code primitives into a shared library, so if you find bugs in them later (or discover new side-channels you didn't think about earlier), you can update the library without having to re-compile and re-deploy everything affected by it.
swordswinger12 12y ago
Any benchmarks? I am very interested in this, it looks really cool!
amirmc 12y ago
Just an additional note that this is the first in a series of posts about the OCaml TLS stack. More are coming in the next few days [1]. [1] https://github.com/mirage/mirage/issues/257 https://github.com/mirage/mirage/issues/257
Hello71 12y ago
it would probably be a good idea to make some mention of 1/n-1 record splitting, lest confusion arise regarding the apparent "new line" between G and ET in the HTTP requests
tenzing 12y ago
There's also miTLS http://www.mitls.org/wsgi/home http://www.mitls.org/wsgi/home - a verified reference implementation of TLS written in F#
wereHamster 12y ago
On one side I see the flaws in the existing openssl and other C-based libraries and when written languages such as OCaml or Haskell those just would not happen. On the other hand those existing libraries work. Which can not be said of the new ones. At least the Haskell TLS library has logic flaws in it that I'm wondering why it works at all. And a lot of Haskell projects use the native tls package instead of the openssl bindings. It is not fun at all having to spend two days to debug something that just works in literally every mainstream language. I hope ocaml-tls doesn't make the same mistake.
- avsm 12y ago
  The Conduit I/O library that we're building in Mirage/OCaml allows the application to select which SSL transport layer implementation that it's linking with. Both Lwt_ssl (which binds to OpenSSL) and OCaml-TLS will be supported when it's released for exactly this reason. There's a blog post due about this next week. As to your other complaint that OpenSSL "just works", note that numerous issues have been swept under the rug over the years (see the LibreSSL CVS logs for more pointers). I'd suggest reading this paper about the most dangerous code in the world for more background: http://crypto.stanford.edu/~dabo/pubs/abstracts/ssl-client-bugs.html http://crypto.stanford.edu/~dabo/pubs/abstracts/ssl-client-b... So when you're using the Haskell library and running into bugs, think of the time you're spending bugfixing and filing patches as a little social tax that contributes to fixing an important technical issue that threatens the stability of the Internet if it's not comprehensively addressed.

106 points by tizoc 12y ago

Looking at the development history it would appear that this project started in Feb 2014: https://github.com/mirleft/ocaml-tls/commit/10b53cd1ebde036047fb4a0d33261d07ce54432b https://github.com/mirleft/ocaml-tls/commit/10b53cd1ebde0360... . Writing an (almost complete) TLS 1.2 stack in such a short amount of time is amazing! (compared to how long it took for NSS to gain TLS 1.2). Looking forward to the next blogpost in this series.

emillon 12y ago

The work on Mirage is very interesting. If I understand it correctly, it may be possible to run a Xen domain with a Linux application server, and with a TLS reverse proxy in front using another Xen domain (in the form of a unikernel). This would be fantastic and does not change a lot how you run your application, except that you get hardened crypto for free. That's assuming that ocaml-tls has no "high level" bugs (not memory corruption related) of course, but I'm quite sure that it is way easier to review than existing TLS implementations.

edwintorok 12y ago
One thing that concerns me is the entropy source in Xen guest domains, but hopefully that'll be worked out for the final version.
- pqwy 12y ago
  It concerns us too. Right now the entropy in Xen domains is weak, but we are working with the rest of the team to feed some actual environmental noise to keep Fortuna well-fed. You can also run the library on Unix, of course, and there the RNG is periodically seeded from /dev/urandom.
- avsm 12y ago
  We're putting together a front/backend ring (rndfront/rndback) that will proxy entropy from dom0 directly into the guest. It'll take some time for this to percolate into the public cloud, so we'll need to do what Linux does in the meanwhile (harvest entropy from interrupt timings, attempt RDRAND, and so on). The ENTROPY module type supports this sort of callback in 1.2.0: https://github.com/mirage/mirage/blob/master/types/V1.mli#L75 https://github.com/mirage/mirage/blob/master/types/V1.mli#L7... (If you're interested in contributing, the entropy harvesting is in sore need of more eyes and help!)
  - rwmj 12y ago
    /me grumbles about virtio-rng and reinventing ABIs ...
    - avsm 12y ago
      Dave Scott's added support for a low-bandwidth channel into XL with the intention of reusing virtio-rng (and virtio-serial and friends). http://lists.xen.org/archives/html/xen-devel/2014-06/msg02931.html http://lists.xen.org/archives/html/xen-devel/2014-06/msg0293... On the other hand, I disagree that we're reinventing an ABI given that: 1) virtio isn't the supported PV interface in Xen -- rndfront/back follows the same design principles as net/blk/fb/usb/pci/console etc. 2) The Xen shared-ring interface is older than virtio, and much simpler for pure PV guests such as Mirage (no PCI emulation to worry about). I do wonder what happened to that GSoC project from a few years to add virtio support to Xen though...I don't think any patches ever appeared.
      - djs55 12y ago
        s/added/currently trying to add/ :-) For HVM guests I hope that virtio-rng would work as-is (if it could be turned on via the control path). That's definitely worth a look. For PV guests like Mirage I'm currently plumbing through a Xen PV analogue of virtio-serial by hijacking^Wextending the existing PV console support. Since the backend for that is in qemu already it might be possible to hook up the entropy source (with all the rate limiting etc). I think the trick would be to get the guest to recognise the frontend for what it is -- I imagine the virtio-rng device in the guest presents itself as a magic hardware PCI device and 'just works'.

hoggle 12y ago

Are we finally approaching consensus in the field of systems programming that security is more important than performance (thanks to heartbleed)? Or put differently: have we reached the point where computers are fast enough so that we can move on and sacrifice some of those abundant MIPS and extra RAM for much improved clarity in our critical infrastructure code? OCaml could actually be a great choice for maintaining a solid TLS layer.

pdpi 12y ago
For the sake of moving things forward: every time we have this discussion, someone always points out that functional languages would make it easier to get correct behaviour from a crypto library, and someone always replies that garbage collection opens you up to side-channel (timing, in this case) attacks.
- lomnakkus 12y ago
  Isn't even C pretty vulnerable to timing attacks? (I'm thinking primarily through things like L1/L2 cache effects, etc.)
- hoggle 12y ago
  Interesting, I didn't know that. I always wondered why (non "functional") Ada doesn't get mentioned more often in these kinds of discussions: http://www.adaic.org/advantages/ http://www.adaic.org/advantages/ http://www.seas.gwu.edu/~mfeldman/ada-project-summary.html http://www.seas.gwu.edu/~mfeldman/ada-project-summary.html
  - pgeorgi 12y ago
    And it's "cousin" SPARK, which adds proof capabilities: http://git.codelabs.ch/?p=spark-crypto.git http://git.codelabs.ch/?p=spark-crypto.git
  - e12e 12y ago
    Last time it was brought up, there appeared to be some lingering confusion and issues with how the compiler and runtime was and is licensed. The latest version of Ada is available for a (large) fee from Adacore and for free under the GPL. There is also a version published as part of gcc, that trails the upstream version a little in terms of features -- but like the rest of gcc, the relevant parts are under LGPL, so not all binaries distributed to third parties need be distributed under the GPL, but can be under any licence one choose[1] -- without the need for a commercial licence from Adacore. It would appear the lack of an up-to-date, gratis, version of Ada was a real problem for adoption at some point -- and the impression of Ada being difficult to get access to outside of large contractors put a damper on its popularity (justified or not). [1] The "problem" with a compiler under GPL is that most compilers will have some kind of library code or language runtime that needs to be distributed with resulting binaries, thus forcing all projects to adopt GPL, rather than just the projects that build directly on the compiler.

richardwhiuk 12y ago

It looks like they have some odd cipher suite selection mechanic. https://tls.openmirage.org https://tls.openmirage.org negotiates TLS_RSA_WITH_RC4_128_SHA which is the second worse suite that Chrome 35 will offer by default. If I renegotiate, the server will suggets TLS_RSA_WITH_AES_256_CBC_SHA, so it looks like the server wants to change the cipher later, which seems odd. This means it doesn't support PFS or several other advantages in the newer protocols. I'd be very interested to know about side channel attacks which may be possible in OCaml, as opposed to in another languages - there doesn't seem to be any discussion of them here. They also refer to the Apple Goto fail bug as a memory safety issue - that's not true, it was a programming flaw that could be made in a GCed language. Finally, if I look at the issue tracker I see things like https://github.com/mirleft/ocaml-tls/issues/6 https://github.com/mirleft/ocaml-tls/issues/6 - closed, with no explanation and marked as a security concern - which gives me no confidence that the issue was addressed.

edwintorok 12y ago
The blogpost does mention that implementing more cipher suites is a work in progress. Edit: the server uses a random protocol version for testing purposes, so that might explain the odd renegotiations that you observed: https://github.com/mirleft/ocaml-tls/issues/159 https://github.com/mirleft/ocaml-tls/issues/159
pqwy 12y ago
Hey, (Disclaimer: one of the authors) We randomize the connection parameters on each connect to help us gauge the stack's behavior with various combinations (see https://github.com/mirleft/ocaml-tls/issues/159 https://github.com/mirleft/ocaml-tls/issues/159 ). Normally it uses first available from the list here: https://github.com/mirleft/ocaml-tls/blob/master/lib/config.ml#L24 https://github.com/mirleft/ocaml-tls/blob/master/lib/config..... (For some reason the RSA variant got on top; it should have been DHE_RSA, which does provide PFS.) Side channel attacks were a very big concern, and I invite you to read the entire series of articles we plan on publishing in the next few days, where we try to lay down our strategy and explain what we know and what we don't. Or even skim through the handshake code and check some of the comments there. We were already warned that CVE-2014-1266 CVE-2014-0224 are not memory safety issues. The article is badly worded there. What was meant is that they are, at least in our pretty firm opinion, issues with C (something we will elaborate in more detail in further articles, but in essence, you get regular control-flow in a functional language and you can encode state machines in a far more explicit manner). Working to update the post and clarify this. As for the issue #6, yes, its closing was not documented too well. This does not mean we didn't expend significant effort to actually address the points there :) . Thank you for the input and please have patience with us. We still have (at least) four more articles to publish!

olifante 12y ago

Security is too damn important to use languages that are insecure by default and that require rigorous discipline and extensive auditing, such as C and C++. The world needs to move its entire crypto and networking layer to functional languages focusing on immutability, thereby immensely reducing the surface of attack.

jude- 12y ago
Secure implementations require more than formal, logical correctness. They must also not leak information to adversaries--i.e. the must be free of side-channels. Unfortunately, ensuring this usually requires the developers to be aware of the low-level behavior of the underlying architecture, which is difficult in functional languages since unlike C, they abstract away behaviors of the underlying hardware that can leak information. I suppose you could extend the functional language's type system to tag data as e.g. needing to be compared to other data in constant time, or needing to be accessed in a particular way to avoid cache-timing attacks, and so on, but this just off-loads the problem to the compiler (i.e. the problem must still be addressed, and not in a high-level functional language). But if you're going to go that far, you might as well put the requisite safe code primitives into a shared library, so if you find bugs in them later (or discover new side-channels you didn't think about earlier), you can update the library without having to re-compile and re-deploy everything affected by it.

swordswinger12 12y ago

Any benchmarks? I am very interested in this, it looks really cool!

amirmc 12y ago

Just an additional note that this is the first in a series of posts about the OCaml TLS stack. More are coming in the next few days [1]. [1] https://github.com/mirage/mirage/issues/257 https://github.com/mirage/mirage/issues/257

Hello71 12y ago

it would probably be a good idea to make some mention of 1/n-1 record splitting, lest confusion arise regarding the apparent "new line" between G and ET in the HTTP requests

tenzing 12y ago

There's also miTLS http://www.mitls.org/wsgi/home http://www.mitls.org/wsgi/home - a verified reference implementation of TLS written in F#

wereHamster 12y ago

On one side I see the flaws in the existing openssl and other C-based libraries and when written languages such as OCaml or Haskell those just would not happen. On the other hand those existing libraries work. Which can not be said of the new ones. At least the Haskell TLS library has logic flaws in it that I'm wondering why it works at all. And a lot of Haskell projects use the native tls package instead of the openssl bindings. It is not fun at all having to spend two days to debug something that just works in literally every mainstream language. I hope ocaml-tls doesn't make the same mistake.

avsm 12y ago
The Conduit I/O library that we're building in Mirage/OCaml allows the application to select which SSL transport layer implementation that it's linking with. Both Lwt_ssl (which binds to OpenSSL) and OCaml-TLS will be supported when it's released for exactly this reason. There's a blog post due about this next week. As to your other complaint that OpenSSL "just works", note that numerous issues have been swept under the rug over the years (see the LibreSSL CVS logs for more pointers). I'd suggest reading this paper about the most dangerous code in the world for more background: http://crypto.stanford.edu/~dabo/pubs/abstracts/ssl-client-bugs.html http://crypto.stanford.edu/~dabo/pubs/abstracts/ssl-client-b... So when you're using the Haskell library and running into bugs, think of the time you're spending bugfixing and filing patches as a little social tax that contributes to fixing an important technical issue that threatens the stability of the Internet if it's not comprehensively addressed.