What will it take for there to be a sel4 router/firewall I can build/buy? Anything directly connected to the internet needs these kind of security guarantees.
The two big things are a network stack that can act as a router (SeL4 has no network stack at all) and drivers. I;d imagine that a decent portion could be ripped from another open source operating system and run in userspace in SeL4 and get some benefits, but I'm not aware of any real effort to do that. Otherwise the usual way to use SeL4 as a hypervisor and just run linux under itm which gets you some benefits but probanly not the ones you'd want for a router to be as secure as possible.
This. Unfortunately, we haven't progressed much beyond Windows NT getting a TCSEC rating: first, remove networking. And then the floppy/cdrom. Then go down the list of other things you can't have.
Simpler versions of such devices exist, eg HENSOLDT Cyber markets a secure VPN gateway that is built on seL4. Over the years we've been in on-and-off discussions with vendors of networking equipment, it's always a battle between those in the company who take security seriously and those resisting any rocking of the boat. Having said that, we're presently in such a discussion again and it's looking promising so far.
However, it's entirely possible that someone has already done it and is not talking about it...
Is there a use case for a microkernel firewall? If you compromise just the tcp/ip stack, you can send and receive arbitrary packets, which is exactly what you would use a root exploit on a monolithic kernel to do.