Re: [MirageOS-devel] kernel and security guarantees

[Thomas Leonard <talex5@xxxxxxxxx>]

On 24 February 2015 at 21:03, Stefan Xenon <stefanxe@xxxxxxx> wrote:
> Hi!
> I have two questions on MirageOS' general security:
>
> I understand a significant portion of MirageOS and the entire Xen are
> written in type-unsafe C. Even though Ocaml has strong guarantees, how
> much does it help as long as the kernel is potentially unsafe?

Hi Stefan,

For the Xen version of Mirage, the C code that runs in the guest is roughly:

- Mini-OS (prink, malloc, assert, assembler boot code, interrupt handler)
- openlibm (standard maths functions, sin, cos, etc)
- OCaml runtime (the garbage collector basically)
- OCaml C bindings for Mini-OS, memory barriers, etc

There's no libc. Some OCaml libraries may pull in more C code. e.g.
ocaml-tls requires libgmp to provide fast big ints for crypto stuff.

It's unlikely there's much you could remove from here. In terms of
security problems from C code, the Linux dom0 is likely to be the
weakest point. It is possible to move some of these functions (network
drivers, USB drivers, etc) into their own Xen guests, as Qubes does,
which should help a lot.

> What is
> the impact on practical system security? Is there any track record of
> exploitable bugs which could help to compare it with other systems?

I'm not aware of any.

> The micro kernel "seL4 (formally) Verified" has been released as open
> source. It sounds like a potentially powerful combination with Mirage.
> Would it be feasible to port MirageOS to seL4? Are there any plans to do so?

As far as I know, the process for porting Mirage goes something like this:

1. Get the OCaml runtime working on the target (enough to run hello
world). You'll need to provide malloc for this, although it doesn't
need to be very good (OCaml will just allocate some large blocks of
memory for its GC pool). You'll want some kind of debug interface so
printing debug messages works.

2. Implement a Lwt event loop (checking for events from the host
system and sleeping if there aren't any). The main loop function you
provide is normally called OS.Main.run.

3. Start writing libraries, implementing the Mirage interfaces (e.g.
make a mirage-console-sel4 library implementing the CONSOLE module
type). Once you have a few low-level ones done, the higher-level
libraries should work automatically (e.g. once you implement NETWORK,
you should find TCP/IP works).

4. Update the mirage tool to generate a suitable main.ml for your
platform when invokes as "mirage configure --sel4".

Your biggest problem will likely be drivers for the physical hardware.
You'll probably want to start with some existing C ones and run them
as separate sel4 processes.


-- 
Dr Thomas Leonard        http://0install.net/
GPG: 9242 9807 C985 3C07 44A6  8B9A AE07 8280 59A5 3CC1
GPG: DA98 25AE CAD0 8975 7CDA  BD8E 0713 3F96 CA74 D8BA

_______________________________________________
MirageOS-devel mailing list
MirageOS-devel@xxxxxxxxxxxxxxxxxxxx
http://lists.xenproject.org/cgi-bin/mailman/listinfo/mirageos-devel