Hi,
I am very interested in SEL4, partly because I was assured it was impossible to use Formal Methods in kernel development, partly because it's a fascinating project in its own right, but right now because there are some embedded applications that could do with the high level of reliability and security that provable correctness implies.
Unfortunately, said applications need a comprehensive network stack and a powerful packet filtering/mangling engine.
The latter could imaginably be done in the kernel, as it's deterministic, but I don't see any obvious value. Nonetheless, if someone has coded such a system as a third-party add-on, I would be very interested.
There are good arguments for why the former can't be done, in a way that can be proven, and I really want the correctness.
In terms of userspace, I believe I could use something like L4Linux (as long as it is still maintained), and I think there's one supplied, but are there other options? Has anyone ported OpenBSD to it?
To be honest, I'm not sure I need a multitasking userspace, but I do absolutely need the network stack and packet filter. Everything else can be ported, albeit with difficulty. However, network operating systems are thin on the ground and tend to be proprietary, exactly what I don't want.
For those curious, I'm looking to end up with a system with strong bounds on robustness and security, and that can handle things like multipath TCP, network failover, QoS and OpenFlow. However, all of these requirements boil down to a sequential process. Unnecessary complexity is where you end up with problems.
If current wisdom says that there's nothing suitable in userspace, then does anyone know if there are there any existing Coloured Petri Nets that I could use to build what I need into the kernel? Even if I can't get better than a quasi-guarantee, it would be something.
Hi Jonathan,
I am very interested in SEL4, partly because I was assured it was impossible to use Formal Methods in kernel development, partly because it's a fascinating project in its own right, but right now because there are some embedded applications that could do with the high level of reliability and security that provable correctness implies.
Unfortunately, said applications need a comprehensive network stack and a powerful packet filtering/mangling engine.
The latter could imaginably be done in the kernel, as it's deterministic, but I don't see any obvious value. Nonetheless, if someone has coded such a system as a third-party add-on, I would be very interested.
From what I understand you’re saying, nothing here would need extensions to the seL4 kernel. This is in line with the microkernel principle on which seL4 is based: the kernel provides fundamental mechanisms for resource management, access control and communication, everything else is in userland. In particular, all device drivers (except one timer driver the kernel needs for preemtion) and network stacks are usermode processes.
So, what you need is to port/implement a high-performance network stack as a native seL4 (i.e. most likely standalone) component, rest comes mostly down to architecture.
There are good arguments for why the former can't be done, in a way that can be proven, and I really want the correctness.
Correctness of what? I.e what are the specific requirements?
Note that you can achieve confidentiality and integrity even with a completely untrusted network stack by using encryption and signatures (thanks to the strong isolation seL4 provides). Only if you care about availability would you require a trustworthy stack. This could be achieved by a completely verified stack, I don’t think such a thing exists yet. Alternatively it might be possible to use model checking to make progress guarantees, although I’m not aware that such a thing has been achieved either to date. In general we are interested in the idea of verified protocol stacks, but aren’t currently working on it.
In terms of userspace, I believe I could use something like L4Linux (as long as it is still maintained), and I think there's one supplied, but are there other options? Has anyone ported OpenBSD to it?
L4Linux has always been a Fiasco-based thing. We had our own paravirtualised Linux (called Wombat) in the past, but we have stopped supporting that quite a while ago. There is no point really, given that all mainstream architectures now have virtualisation support that allows you to run unmodified guest binaries at minimal performance penalty. We routinely run Linux on seL4 using hardware-supported virtualisation. OpenBSD should be relatively straightforward.
We also have a student project on running BSD as a unikernel (aka library OS) on seL4. This has recently started kicking and will likely be running soon.
To be honest, I'm not sure I need a multitasking userspace, but I do absolutely need the network stack and packet filter. Everything else can be ported, albeit with difficulty. However, network operating systems are thin on the ground and tend to be proprietary, exactly what I don't want.
For those curious, I'm looking to end up with a system with strong bounds on robustness and security, and that can handle things like multipath TCP, network failover, QoS and OpenFlow. However, all of these requirements boil down to a sequential process. Unnecessary complexity is where you end up with problems.
All these things would be userland code in seL4.
If current wisdom says that there's nothing suitable in userspace, then does anyone know if there are there any existing Coloured Petri Nets that I could use to build what I need into the kernel? Even if I can't get better than a quasi-guarantee, it would be something.
Again, the kernel is the wrong place for such code in seL4. There is no benefit of moving stuff into the kernel, only the cost of losing all guarantees the kernel’s verification provide.
Gernot
On Sat, 27 Aug 2016 00:36:35 +0000, Gernot.Heiser wrote:
Hi Jonathan,
<snip>
In terms of userspace, I believe I could use something like L4Linux (as long as it is still maintained), and I think there's one supplied, but are there other options? Has anyone ported OpenBSD to it?
L4Linux has always been a Fiasco-based thing. We had our own paravirtualised Linux (called Wombat) in the past, but we have stopped supporting that quite a while ago. There is no point really, given that all mainstream architectures now have virtualisation support that allows you to run unmodified guest binaries at minimal performance penalty. We routinely run Linux on seL4 using hardware-supported virtualisation. OpenBSD should be relatively straightforward.
I disagree with this assessment - in particular, hardware virtualization comes with a large, un-verified, and poorly-secured TCB. This can be seen in the swathes of hardware-level vulnerabilities that have arisen from it:
The AMD bug called out at the bottom of the article is particularly nasty, as it allowed an unprivileged user in an unprivileged guest to cause arbitrary code execution in host Ring 0.
This would undercut seL4's entire security model.
As a result, I think it'd be _very_ prudent to continue looking at purely- software, paravirtualized hypervisor implementations, especially for high- assurance systems.
<snip>
On 30 Aug 2016, at 8:38 , Alex Elsayed eternaleye@gmail.com wrote:
As a result, I think it'd be _very_ prudent to continue looking at purely- software, paravirtualized hypervisor implementations, especially for high- assurance systems.
I think it’s an illusion to think one can partition hardware into trusted and untrusted bits. In the end, the OS is at the mercy of the hardware, if it’s faulty then you lose, there’s no way around it.
You may *think* that the manufacturers don’t make changes to the more conventional bits of the hardware, and thus they are “correct", but that isn’t true, of course. And on top of that we know that there are intentional backdoors in commercial hardware.
The only way around this is high-assurance hardware, and this doesn’t come at an affordable cost.
Gernot
On Mon, 29 Aug 2016 23:01:45 +0000, Gernot.Heiser wrote:
On 30 Aug 2016, at 8:38 , Alex Elsayed eternaleye@gmail.com wrote:
As a result, I think it'd be _very_ prudent to continue looking at purely- software, paravirtualized hypervisor implementations, especially for high- assurance systems.
I think it’s an illusion to think one can partition hardware into trusted and untrusted bits. In the end, the OS is at the mercy of the hardware, if it’s faulty then you lose, there’s no way around it.
You may *think* that the manufacturers don’t make changes to the more conventional bits of the hardware, and thus they are “correct", but that isn’t true, of course. And on top of that we know that there are intentional backdoors in commercial hardware.
The only way around this is high-assurance hardware, and this doesn’t come at an affordable cost.
Sure, and I don't disagree. It's part of why I'm so excited by the RISC-V work, especially MIT's progress on formal verification - that, at least, pushes the space problems can occur in down by one more level.
But to a certain extent, I think that there's value in reducing the amount of new API exposed. Furthermore, there's a large body of code exercising the "more conventional" bits in the wild, and a considerably smaller body of code exercising the newer bits. Bugs in the more conventional bits are thus more likely to break existing code - and thus be caught early.
It's not protection in the same sence as high-assurance hardware, no. But at least statistically, from looking at where severe hardware-based security vulnerabilities have cropped up, it seems to be better than the alternative of trusting the hardware virtualization to actually isolate.
On 30 Aug 2016, at 15:22 , Alex Elsayed eternaleye@gmail.com wrote:
On Mon, 29 Aug 2016 23:01:45 +0000, Gernot.Heiser wrote:
[…]
The only way around this is high-assurance hardware, and this doesn’t come at an affordable cost.
Sure, and I don't disagree. It's part of why I'm so excited by the RISC-V work, especially MIT's progress on formal verification - that, at least, pushes the space problems can occur in down by one more level.
But to a certain extent, I think that there's value in reducing the amount of new API exposed. Furthermore, there's a large body of code exercising the "more conventional" bits in the wild, and a considerably smaller body of code exercising the newer bits. Bugs in the more conventional bits are thus more likely to break existing code - and thus be caught early.
It's not protection in the same sence as high-assurance hardware, no. But at least statistically, from looking at where severe hardware-based security vulnerabilities have cropped up, it seems to be better than the alternative of trusting the hardware virtualization to actually isolate.
The problem is that you don’t really know how the hardware is internally structured, and how modularised what you see as a separate feature really is.
In the example you gave, if there’s a hardware bug that gives you privilege escalation from non-root Ring 3 to root Ring 0, what makes you think that the same bug doesn’t let you go from root Ring 3 to root Ring 0, which seems like a smaller step (switching only one mode instead of two)?
Root Rings 3+0 is exactly what you’re using when using para-virtualisation. I claim that you cannot have more than zero confidence that hardware that allows the first type of escalation won’t allow the second type.
Gernot
On Tue, 30 Aug 2016 05:44:52 +0000, Gernot.Heiser wrote:
On 30 Aug 2016, at 15:22 , Alex Elsayed eternaleye@gmail.com wrote:
On Mon, 29 Aug 2016 23:01:45 +0000, Gernot.Heiser wrote:
[…]
The only way around this is high-assurance hardware, and this doesn’t come at an affordable cost.
Sure, and I don't disagree. It's part of why I'm so excited by the RISC-V work, especially MIT's progress on formal verification - that, at least, pushes the space problems can occur in down by one more level.
But to a certain extent, I think that there's value in reducing the amount of new API exposed. Furthermore, there's a large body of code exercising the "more conventional" bits in the wild, and a considerably smaller body of code exercising the newer bits. Bugs in the more conventional bits are thus more likely to break existing code - and thus be caught early.
It's not protection in the same sence as high-assurance hardware, no. But at least statistically, from looking at where severe hardware-based security vulnerabilities have cropped up, it seems to be better than the alternative of trusting the hardware virtualization to actually isolate.
The problem is that you don’t really know how the hardware is internally structured, and how modularised what you see as a separate feature really is.
Sure, and that would be an argument against it providing yes/no hard assurance. But I'm talking about "empirically, this has been less likely to be a problem."
In the example you gave, if there’s a hardware bug that gives you privilege escalation from non-root Ring 3 to root Ring 0, what makes you think that the same bug doesn’t let you go from root Ring 3 to root Ring 0, which seems like a smaller step (switching only one mode instead of two)?
Mainly? That this bug was pretty-well characterized, and that despite people prodding at it pretty hard, no one managed to reproduce it without virtualization being active.
Root Rings 3+0 is exactly what you’re using when using para-virtualisation. I claim that you cannot have more than zero confidence that hardware that allows the first type of escalation won’t allow the second type.
I suppose this is where we disagree - I know full well that I can't _show_ that the first kind of escalation does not allow the second, but when a severe bug like this is revealed, the ensuing scrutiny has high chances of revealing bugs that are "nearby" in terms of causation.
And the vast majority of the virtualization-related bugs have not had such "nearby" discoveries in virtualization-free operation. If anything, that seems to imply that there _is_ some structural separation - otherwise, the odds of such "nearby" bugs being present (and found) would almost certainly be higher than demonstrated.
-
Alex Elsayed -
Gernot.Heiser＠data61.csiro.au -
Jonathan C Day