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