Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Introducing Transport Layer Security in pure OCaml

openmirage.org

Post reply on HN
Print view View original

21–30 of 44 posts

Re: Introducing Transport Layer Security in pure OCaml

#21

Post by avsm »

duaneb wrote: post #13
hoggle wrote: post #4

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…

> OCaml could actually be a great choice for maintaining a solid TLS layer. 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).

The OCaml runtime is very easy to embed, as runtimes go. We've got it compiling in Mirage as a standalone kernel, as a FreeBSD kernel module, and others have had it running on 8-bit PIC microcontrollers: http://www.algo-prog.info/ocaml_for_pic/web/index.php?id=oca...

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.

Re: Introducing Transport Layer Security in pure OCaml

#22

Post by ctz »

pqwy wrote: post #15
richardwhiuk wrote: post #5

It looks like they have some odd cipher suite selection mechanic. 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 n…

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 ). 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 pro…

> What was meant is that they are, at least in our pretty firm opinion, issues with C

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.

Re: Introducing Transport Layer Security in pure OCaml

#23

Post by amirmc »

avsm wrote: post #18
richardwhiuk wrote: post #5

It looks like they have some odd cipher suite selection mechanic. 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 n…

Well done on noticing the slightly random cipher negotiation. That was actually deliberately put into the demo server on tls.openmirage.org to help us get more test coverage from visitors to the site (see the https://github.com/mirleft/ocaml-tls/tree/demo-random branch). We've mitigated most of the commonly known client incompatibilities, but there are no doubt obscure cipher-specific mitigations remaining, and the o…

Clicky link to the reply is:

https://github.com/mirleft/ocaml-tls/issues/6#issuecomment-4...

Re: Introducing Transport Layer Security in pure OCaml

#24

Post by chriswarbo »

pdpi wrote: post #7
hoggle wrote: post #4

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…

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.

Interesting. Maybe an area where linear types can shine?

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.

Re: Introducing Transport Layer Security in pure OCaml

#25

Post by colanderman »

pdpi wrote: post #7
hoggle wrote: post #4

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…

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.

I know nothing about crypto, but I know a bit about languages. I don't really get this.

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?

Re: Introducing Transport Layer Security in pure OCaml

#26

Post by pqwy »

ctz wrote: post #22
pqwy wrote: post #15

Earlier quoted context omitted.

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 ). 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 pro…

> What was meant is that they are, at least in our pretty firm opinion, issues with C 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 inspectio…

Sounds like a nice exercise, I'll try it.

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.

Re: Introducing Transport Layer Security in pure OCaml

#27

Post by pjmlp »

hoggle wrote: post #4

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…

I hope so.

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.

Re: Introducing Transport Layer Security in pure OCaml

#28

Post by lomnakkus »

pdpi wrote: post #7
hoggle wrote: post #4

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…

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.

Isn't even C pretty vulnerable to timing attacks? (I'm thinking primarily through things like L1/L2 cache effects, etc.)

Re: Introducing Transport Layer Security in pure OCaml

#30

Post by rwmj »

avsm wrote: post #19
edwintorok wrote: post #6

Earlier quoted context omitted.

One thing that concerns me is the entropy source in Xen guest domains, but hopefully that'll be worked out for the final version.

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/…

/me grumbles about virtio-rng and reinventing ABIs ...
Post reply on HN