4 ms·

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

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

by cheez 11y ago

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.