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