4 ms·

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

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

cheez 11y ago
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.
- agentultra 11y ago
  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)
  - cheez 11y ago
    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?
    - agentultra 11y ago
      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. update update s/SSL/TLS/
- Ericson2314 11y ago
  It seems to me that most security issues we hear about with that stuff are stupid memory issues, not higher level bugs. Also formal methods should work better with unikernels, opening up the door for them to lead the way on proving various properties/invariants.
  - cheez 11y ago
    Maybe only because the more protocol-specific bugs are already ironed out in those stacks, leaving the buffer over/underruns
    - Ericson2314 11y ago
      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.
- nickpsecurity 11y ago
  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.
sgrove 11y ago
Well, yes and no. The surface area for memory-unsafe problems is much smaller, but it's still there. To @cheez's point, Mirage did contain a very dangerous vulnerability (see https://www.somerandomidiot.com/blog/2014/07/09/how-to-set-the-evil-bit/ https://www.somerandomidiot.com/blog/2014/07/09/how-to-set-t...). 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 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!
- nickpsecurity 11y ago
  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. :)
AlfredBratterud 11y ago
Performance was our main goal :-)
- nickpsecurity 11y ago
  Then MenuetOS/KolibriOS people are still waiting on you to catch up. Might be language choice. :P

cheez 11y ago

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.

agentultra 11y ago
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)
- cheez 11y ago
  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?
  - agentultra 11y ago
    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. update update s/SSL/TLS/
Ericson2314 11y ago
It seems to me that most security issues we hear about with that stuff are stupid memory issues, not higher level bugs. Also formal methods should work better with unikernels, opening up the door for them to lead the way on proving various properties/invariants.
- cheez 11y ago
  Maybe only because the more protocol-specific bugs are already ironed out in those stacks, leaving the buffer over/underruns
  - Ericson2314 11y ago
    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.
nickpsecurity 11y ago
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.

sgrove 11y ago

Well, yes and no. The surface area for memory-unsafe problems is much smaller, but it's still there. To @cheez's point, Mirage did contain a very dangerous vulnerability (see https://www.somerandomidiot.com/blog/2014/07/09/how-to-set-the-evil-bit/ https://www.somerandomidiot.com/blog/2014/07/09/how-to-set-t...). 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 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!

nickpsecurity 11y ago
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. :)

AlfredBratterud 11y ago

Performance was our main goal :-)

nickpsecurity 11y ago
Then MenuetOS/KolibriOS people are still waiting on you to catch up. Might be language choice. :P