> A DNS service built with IncludeOS results in a 158K disk image (for comparison, the MirageOS DNS server image came in at 200K).
A 42K difference and OCaml buys you memory safety and the ability to embed an invariant in your type system; further restricting the allowable executions of your program.
That is the point of MirageOS. They chose a functional language because they wanted a trusted computing base (or something as practically close to trusted as one can get).
I don't think size is going to be the big determining factor for people choosing competing unikernel implementations.
The problem I see with these unikernels is that they all necessarily have to reimplement things that have had decades of testing like TCP/IP stacks. This could be problematic and contain MORE vulnerabilities than the alternative.
So I would say that the factors in a decision to use a unikernel are likely:
1. Speed/cost
2. Space
3. Security (or lack thereof)
I would guess that the cost difference needs to be so convincing that people will be willing to work around potential security issues.
I don't technically have a horse in the unikernel race but have only been following the MirageOS team.
From what I understand unikernels or "operating system as a library," are not not a new idea. The cost of implementing an entire TCP/IP stack for every unikernel ecosystem is probably what kept them from being adopted early on. However we have some good specifications these days and battle-hardened implementations to test new ideas against. I think the idea behind MirageOS is that they see C/glibc/etc as a liability.
So building a TCP/IP stack in a pure-functional language is an interesting idea. Just because we have a reliable system now doesn't mean we can't make it more robust by experimenting with new ideas.
One certainly needs to take more care building unikernel infrastructure than a typical web application or script. I'd only touch them in production with verifiable formal specifications and a strongly-typed functional language implementation... but that's light-years ahead of what a typical gnu/linux VM guarantees.
(Also the reason why I don't think size will matter here is that they all aim to be pretty small and in a cloud, 42KB difference on HVs with >64GB of RAM doesn't make much of a difference)
It's true that unikernels, if done right, give you the possibility of formal verification. So that would be a definite selling point for MirageOS as opposed to IncludeOS. Can they do it, though?
Probably... many of the people behind MirageOS are Cambridge-educated people. I have no university degree and I'm picking up TLA+ as my first foray into formal methods quite well. The amazing thing is that for correctness the maths behind TLA+ is really easy to understand. I think many people involved in systems-level programming could pick it up with just a couple of weeks' training.
I don't think they have done it though... which makes reading through their TLS implementation rather difficult, IMO. The type system of OCaml will give some guarantees but it has a hard time catching high-level design errors that TLA+ and formal methods will.
update This also doesn't preclude them, or anyone with an interest, in creating specifications for these systems. Amazon started using formal methods and found bugs in several AWS services after the fact.
Are you arguing with or against my claims? Since we're talking about reimplementing existing protocols, problems with the spec are either fixed our not our fault. Thus, high- and low-level bugs are ruled out, leaving...not much.
You have a good point in the first sentence. They're probably going to run into trouble. Might be worth it in the long run but I see stuff happening.
That said, clean-slate TCP/IP from separation kernel vendors and Secure64's DNS resisted attack much better than common stacks with no failures detected even under high, random load. So, it can go the other way, too.
I'm optimistic that long term it's a great and obviously worthwhile tradeoff, even though the new stack (and all of https://nqsb.io really) is going to need a lot of real-world usage and examination.
Also, size and startup time are definitely pretty cool metrics (or at least fun metrics), and I'm happy to see both decrease!
The tech IncludeOS builds on had a lot more than that in its lifetime. No telling what IncludeOS will have once people start digging into it. There's an order of magnitude difference in host compromises between safe and unsafe code. That's the point.
The language also has advantages in further analysis (eg type system), safe extension, and maintenance. So, even an apples to oranges comparison of the two on size looks in Ocaml's favor as you get more for you KB. :)
It's not a machine, exactly; it's not an OS in the way you are used to thinking of it. It's a library you link against, which gives you a single, statically linked, bootable image, which you can then launch inside a VM. There is no shell, unless your application includes one; there is no filesystem, unless your application implements one; there are no other processes, unless your application chooses to manage them.
I wrote the bootloader and first kernel sketch using Bochs exclusively, due to the nice GUI for register inspection, instruction-by-instruction stepping etc. But it hasn't been tested on bochs for ages, so now I don't know. In particular I have never done any networking with bochs; my guess is that if it has virtio it would be pretty easy to support it. Go ahead and try, let's know how far it gets and we'll help you out :-)
20 comments
[ 2.9 ms ] story [ 78.4 ms ] threadAlso Linux is GPL, while includeOS is Apache licensed. As a library, the syscall exception may well not apply with using Linux as a unikernel.
- switched from GCC to LLVM/Clang-based toolchain
- switched from EASTL to LLVM’s libc++
- read-only FAT file system
- exceptions implemented
- working TCP
[0] http://blog.acolyer.org/2016/02/22/includeos/#comment-6419
A 42K difference and OCaml buys you memory safety and the ability to embed an invariant in your type system; further restricting the allowable executions of your program.
That is the point of MirageOS. They chose a functional language because they wanted a trusted computing base (or something as practically close to trusted as one can get).
I don't think size is going to be the big determining factor for people choosing competing unikernel implementations.
So I would say that the factors in a decision to use a unikernel are likely:
I would guess that the cost difference needs to be so convincing that people will be willing to work around potential security issues.From what I understand unikernels or "operating system as a library," are not not a new idea. The cost of implementing an entire TCP/IP stack for every unikernel ecosystem is probably what kept them from being adopted early on. However we have some good specifications these days and battle-hardened implementations to test new ideas against. I think the idea behind MirageOS is that they see C/glibc/etc as a liability.
So building a TCP/IP stack in a pure-functional language is an interesting idea. Just because we have a reliable system now doesn't mean we can't make it more robust by experimenting with new ideas.
One certainly needs to take more care building unikernel infrastructure than a typical web application or script. I'd only touch them in production with verifiable formal specifications and a strongly-typed functional language implementation... but that's light-years ahead of what a typical gnu/linux VM guarantees.
(Also the reason why I don't think size will matter here is that they all aim to be pretty small and in a cloud, 42KB difference on HVs with >64GB of RAM doesn't make much of a difference)
I don't think they have done it though... which makes reading through their TLS implementation rather difficult, IMO. The type system of OCaml will give some guarantees but it has a hard time catching high-level design errors that TLA+ and formal methods will.
update This also doesn't preclude them, or anyone with an interest, in creating specifications for these systems. Amazon started using formal methods and found bugs in several AWS services after the fact.
update update s/SSL/TLS/
Also formal methods should work better with unikernels, opening up the door for them to lead the way on proving various properties/invariants.
That said, clean-slate TCP/IP from separation kernel vendors and Secure64's DNS resisted attack much better than common stacks with no failures detected even under high, random load. So, it can go the other way, too.
I'm optimistic that long term it's a great and obviously worthwhile tradeoff, even though the new stack (and all of https://nqsb.io really) is going to need a lot of real-world usage and examination.
Also, size and startup time are definitely pretty cool metrics (or at least fun metrics), and I'm happy to see both decrease!
The language also has advantages in further analysis (eg type system), safe extension, and maintenance. So, even an apples to oranges comparison of the two on size looks in Ocaml's favor as you get more for you KB. :)
Does it include a filesystem?
Does it allow to execute other processes?