22 ms·

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.

simcop2387 6y ago
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.
- kjs3 6y ago
  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.
- technion 6y ago
  Would a good first target here be SDN switches? In general, their own networking is mostly for remote access.
snvzz 6y ago
A possibility would be for Genode to actually go through their roadmap. They had a "Use case: Genode-based network router" target for May, but it is still outstanding.
aidenn0 6y ago
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.
microkerneldude 6y ago
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...

simcop2387 6y ago

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.

kjs3 6y ago
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.
technion 6y ago
Would a good first target here be SDN switches? In general, their own networking is mostly for remote access.

snvzz 6y ago

A possibility would be for Genode to actually go through their roadmap. They had a "Use case: Genode-based network router" target for May, but it is still outstanding.

aidenn0 6y ago

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.

microkerneldude 6y ago

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