Introducing Transport Layer Security in pure OCaml
openmirage.org
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 - closed, with no explanation and marked as a security concern - which gives me no confidence that the issue was addressed.
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
(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 ). Normally it uses first available from the list here: 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!
I am very interested in the idea that ML can maintain security correctness under source line duplication.
It should be pretty easy to check for this condition too: for every line in every file, duplicate it. Discard instances where this causes invalid syntax; this will be most of them. Now either by running a test suite or inspection, see what the effect was on the program semantics.
But since by and large the lines we have are expression and not statements (the core handler is purely functional, using a monad to thread errors through), this amounts to type errors immediately.
We've looked into timing side channels attacks quite a bit, but decided to focus on the core protocol support before tackling the big issue of data-dependent control flow attacks See https://github.com/mirleft/ocaml-tls/pull/49 for discussion on the Lucky 13 mitigation that isn't merged in for example.
Editing the goto-fail reference to reflect that it's not purely memory safety (but of course we believe that more structured programming abstractions will help mitigate this class of errors). I've asked Hannes about the #6 issue as well, as that shouldn't have been closed with no explanation -- do feel free to post queries on such issues yourself as polling HN threads for feedback isn't reliable.
https://github.com/mirleft/ocaml-tls/issues/6#issuecomment-4...
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.
You can also run the library on Unix, of course, and there the RNG is periodically seeded from /dev/urandom.
The ENTROPY module type supports this sort of callback in 1.2.0: 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!)
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.
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'.
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.
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.
Back in the day everyone was paying for compilers, the prices were the normal ones for the target audience.
Rational Software first product was an advanced Ada Machine, providing an early 80's InteliJ experience. Which followed the same fate as all special purpose computers.
UNIX, mainframe and other enterprise OS vendors that eventually provided an Ada compiler, treated it as second class citizen in regard to their main systems programming language.
Home computers lacked the required hardware to implement a proprer Ada compiler.
A systems programming language really needs to be "the language" an OS vendor SDK requires, otherwise it becomes just another application language that can also go low level.
Besides Ada Core, there are a few embedded and real time OS vendors providing Ada compilers.
Could you elaborate? Are you thinking 80s home computers like the Amiga 1000, or more classical PCs?
On those days I and many older than me were still writing business applications in Assembly. Compilers for higher level languages were constrained in what they could achieve in the amount of memory that was available.
And Ada did required lots of it. Funny enough I would bet modern Ada compilers are less resource intensive than C++ ones.
Rust is probably the most trendy language offering linear types at the moment, although I'd say it much closer to being "a safer C" than "a linear OCaml", so it wouldn't really make things more functional (although it would be safer!).
ATS is descended from DependentML, but for some reason most ATS code I've seen is written in a "safer C" style too. Maybe that's just pragmatism, since ATS has very few native libraries, so it's usually easier to call out to C.
Linear Lisp might be a nice choice, but its dynamic typing may be a problem for security-critical code.
~/rust $ find -name '*.ml' | wc -l
72
~/rust $ find -name '*.ml' | grep -v ./src/llvm | wc -l
0
Say you're coding in a language with no garbage collection like C. If your code is not "symmetric" (more below), you still have timing attacks due to cache usage patterns, correct? After all, C hasn't been a very good model of any CPU designed since 1985.
Coming from the outside, I would think the way to tackle this would be to simple ensure your code is "symmetric"; that every legal code path through an algorithm perform the same operations, regardless of what data it is presented with, even if this means operating on fake data. That way the timing of any operation is always identical (barring uncorrelated noise).
It seems to me that this technique would apply equally to languages with and without garbage collection. Why is this not so?
Maybe; it uses GC and it's difficult to embed. I would much prefer something that compiles without a runtime (or with a minimal one for resource allocation).
A fun project that I discussed with the Rust devs at last year's OSCON would be to rewrite the OCaml GC in Rust. Get in touch with me if you're interested and want some guidance on how to go about this.
We already had safer systems programming languages around the time UNIX spread outside AT&T.
There is a quote from Hoare how engineers asked him to not allow to disable bounds checking in Algol, for example[0].
Also the rise in security exploits has helped Ada/SPARK to move outside their original niche into areas where human lifes are at risk, like medical equipments and train control systems. At least from the FOSDEM talks.
I am looking forward to the days when we can recover the systems programming security C took away.
[0] later compiler versions allowed it.
Looking forward to the next blogpost in this series.
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.
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.
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-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.