I understand how using type-safety and streamlined modular systems might be good for security, but I fail to see the point in letting developers be closer to the bare metal. All the security abstractions built into traditional OSes are not there for no reason. Why should I trust the OCaml stack more than the alternatives?
This looks like something a really educated/disciplined company could use for creating some crazy cool infrastructure. It's hard to see it taking off for the average Joe.
I think you answered your own question (to some extent). Rewriting the necessary protocols/libraries in a type-safe manner already provides an improvement over the current systems. In addition, (with the standard approach) it's quite hard for a developer to reason about the whole stack they're using and privilege escalation bugs are particularly irksome. Writing the applications with the approach Mirage takes means that there is less code to reason about.
An anecdote I use when describing the benefits is the story of a smart fridge that got hacked and became part of a botnet sending spam emails. Why did that fridge even have code that allowed it to send email? It wasn't necessary for its functioning. We should write software differently if were going to be deploying it to 10x the number of devices compared to today.
More personally, I worry about the software that's going to find it's way into the embedded health devices of the future (cf pacemakers). These devices will inevitably be 'connected' and I want to make sure that the code they use is safe and secure.
> Why did that fridge even have code that allowed it to send email?
If it has a remote code execution vulnerability, it's trivial to make it send spam (or do all kinds of things) whether a MUA was already present or not.
OP here. The Unikernel paper someone linked about has more, but I think the main ideas are: incidental complexity mitigation and performance.
It's much easier to reason about a bunch of OCaml code, so say the authors, than it is to understand the interaction between independently changing pieces of your "stack" that are written in different languages and integrate in disparate ways.
This looks like something a really educated/disciplined company could use for creating some crazy cool infrastructure. It's hard to see it taking off for the average Joe.