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

31–40 of 44 posts

Re: Introducing Transport Layer Security in pure OCaml

#31

Post by avsm »

rwmj wrote: post #30
avsm wrote: post #19

Earlier quoted context omitted.

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 ...

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

Re: Introducing Transport Layer Security in pure OCaml

#32

Post by djs55 »

avsm wrote: post #31
rwmj wrote: post #30

Earlier quoted context omitted.

/me grumbles about virtio-rng and reinventing ABIs ...

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

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'.

Re: Introducing Transport Layer Security in pure OCaml

#33

Post by steveklabnik »

chriswarbo wrote: post #24
pdpi wrote: post #7

Earlier quoted context omitted.

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

Fun bit of trivia: Rust was originally implemented _in_ OCaml, and takes a lot of cues from it.

Re: Introducing Transport Layer Security in pure OCaml

#34

Post by e12e »

hoggle wrote: post #9
pdpi wrote: post #7

Earlier quoted context omitted.

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, 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.seas.gwu.edu/~mfeldman/ada-project-summary.html

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.

Re: Introducing Transport Layer Security in pure OCaml

#37

Post by pjmlp »

e12e wrote: post #34
hoggle wrote: post #9

Earlier quoted context omitted.

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.seas.gwu.edu/~mfeldman/ada-project-summary.html

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

More than price, what really hindered Ada was lack of adoption by popular OS vendors and hardware requirements for the early compilers.

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.

Re: Introducing Transport Layer Security in pure OCaml

#38

Post by e12e »

pjmlp wrote: post #37
e12e wrote: post #34

Earlier quoted context omitted.

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

More than price, what really hindered Ada was lack of adoption by popular OS vendors and hardware requirements for the early compilers. 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, ma…

> Home computers lacked the required hardware to implement a proprer Ada compiler.

Could you elaborate? Are you thinking 80s home computers like the Amiga 1000, or more classical PCs?

Re: Introducing Transport Layer Security in pure OCaml

#39

Post by wereHamster »

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.

Re: Introducing Transport Layer Security in pure OCaml

#40

Post by klibertp »

steveklabnik wrote: post #33
chriswarbo wrote: post #24

Earlier quoted context omitted.

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

Fun bit of trivia: Rust was originally implemented _in_ OCaml, and takes a lot of cues from it.

I saw a bit of OCaml code in Rust code-base recently, can you say what it's used for? I know that Rust is self-hosting now, but I swear I saw some .ml files there...
Post reply on HN