Securing the Unikernel | Hacker News Reader

Securing the Unikernel

roscidus.com

84 pointslelf11 comments

This article touched on something that's bothered me about Xen: We don't have a secure dom0 OS. It'd be encouraging if there were some work to take something more secure than the average OS (for some value of secure, anything from Minix 3 to seL4 would probably be much better than what we have now) and make it a full-featured dom0 option.

Dom0 disaggregation has the potential to help, but there's going to have to be a tremendous amount of wheel reinvention in safe languages to provide the safety and features everyone needs.

The lack of an effect system in OCaml is annoying. Exceptions, which are widely used, are an idiot-proof recipe for resource leaks, combined with the lack of a 'finally' statement. Even something like basic checked exceptions would help.

On the other hand, the lack of 'finally' itself is not such a big issue, considering that you are going to end up using either Lwt or Core.Async as soon as you start doing something non-trivial with IO.

The "building block" APIs that Mirage use tend to be exception free, for example:

https://github.com/mirage/mirage/blob/master/types/V1.mli#L2...

     type error = [
        | `Unknown of string (** an undiagnosed error *)
        | `Unimplemented     (** operation not yet implemented     in the code *)
        | `Is_read_only      (** you cannot write to a read/only instance *)
        | `Disconnected      (** the device has been previously disconnected *)
  ]

    val read: t -> int64 -> page_aligned_buffer list -> 
       [ `Error of error | `Ok of unit ] io

This lets the larger scale module assembly fit together with explicit checking that each device driver connected and initialised ok, and is the equivalent of basic checked exceptions. Completely checked exceptions are something of a pain to work with...

How exception-free are they, really? I find in practice that "exception-free" OCaml code relies largely on eyeballing + trusting underlying libraries, which isn't too reassuring.

It's OK, but it's a lot like the old "programmers with enough discipline can use footguns safely" argument.

The thing to remember with exceptions is that they're for exceptional situations. We check explicitly in the return value for "common" errors such as a read failure, and higher level control flow catches exceptions that bubble up and log them and/or kill that particular thread.

This works pretty well in practise, and is quite similar to Erlang's monitor model. It's verbose and undesirable to handle _all_ exceptional cases in a distributed system explicitly via checked exceptions, and using monitors to catch exceptions that we're not expecting and do a process kill/log/restart is a good model in my mind.

OCaml gives the language flexibility to migrate to this as well, which is nice (since, as you note, we'll never get all the third-party code we depend on to be exception-free, and nor do I think that is a desirable goal). Core and Async from Jane Street also exhibit this split: Core tends to use On_error to explicitly handle errors, and Async (being used for distributed programming) instead adopts a "raise-exception-and-catch-it-in-a-monitor" model. Theres more on that in the Async chapter in RWO: https://realworldocaml.org/v1/en/html/concurrent-programming...

This sounds reasonable. Thank you for the overview.

Note that the Lwt syntax extension (often used in Mirage) adds a try_lwt..finally construct. Doing anything at all with IO in Mirage will be asynchronous (there are no blocking operations anywhere).

However, people generally use various "with" functions to manage resources. That's better than try..finally because the allocation can't get separated from the try bit.

I never found Java checked exceptions much use for resource leaks, since unchecked exceptions are always still possible.

> Note that the Lwt syntax extension (often used in Mirage) adds a try_lwt..finally construct.

That's what I wanted to say, but reading back, it was a bit unclear. Though I'd recommend lwt.ppx over its camlp4 ancestor...

> However, people generally use various "with" functions to manage resources.

Which I assume are usually implemented via try/finally if using Lwt :)

> I never found Java checked exceptions much use for resource leaks, since unchecked exceptions are always still possible.

It's not fool-proof, but having a codebase where most exceptions are checked exceptions still protects you in many cases. And of course, try-with-resource is a good way to guarantee against resource leaks in the majority of cases.

https://github.com/0install/0repo-queue/blob/master/unikerne... is this safe? Coming from my haskell background, I'd expect a check for failure here; how does ocaml handle it? Exceptions?

You're right. OCaml will throw an exception here. Many of the functions in the standard library throw exceptions when it would be better to return an option type (newer libraries are usually better).

The exception will be caught and logged in the "callback" function below. It then rethrows it, but the unikernel will continue serving requests.

Yes.

Reply on news.ycombinator.com