The linked thread was one of the few times I made a counterpoint on HN followed by the author showed up saying the counterpoint was effectively the roadmap. It was good as I was just passing on what Dresden & NICTA had already done. Less surprising he was working at NICTA on seL4. ;) In any case, I later discovered Redox was using some similar techniques with them in much more production form but with less security at foundations. There might be opportunities for the projects to work together if they’re not already. The components for one might be reusable in the other if the OS/microkernel-level stuff is hidden in modules well.
I also agree with Nagle that this has potential for use in things like routers. The reason being message routers, guards, and VPN’s were first things the security kernels were used for. They did well during evaluation. Separation kernels and security-focused microkernels followed them with seL4 being highest in development assurance. It also has a Linux layer & ARM support. Gives this project extra potential in medium-high assurance security if they just do their components well. Code from Netbricks could be ported to it for first appliance.
EDIT: Author of project posted same story at link below. You might want to glance at it Wednesday in case the author adds any interesting details by then.
Thanks for pointing me to this! I have a lobste.rs account but I don’t tend to use it very often. Indeed our first “usecase” is network appliances. But it’s a ways down the road. I’d personally love to see a seL4 implementation of Xen’s hypercall interface, and slowly start replacing a Linux etc dom0 with high-quality isolated seL4 components. My primary motivation for working on this project is that I think it’s fun, I’ve been learning a lot, and I have the time while I’m still in school.
[Comment removed by author]
Writing ~all the drivers necessary for a specific HW platform (say, a specific family of HP servers with two or three NICs, one or two HBAs) wouldn’t be terribly challenging and might be valuable for some usecases. Could probably even mostly-synthesize them with Termite. How heterogeneous is something like AWS? How much do Xen vulnerabilities cost them?
Don’t forget DDEkit. The work in CompSci that inspired seL4 includes Dresden’s TUD:OS team that did DROPS, Nitpicker, and L4Linux. I think it was them that devised the following idea: include just enough of Linux kernel to re-use the drivers but they get accessed by shims in the user-mode apps. You can put a driver in native process on microkernel, put driver(s) in driver VM to isolate them (for reliability) a bit with real VM’s using virtual drivers, or put drivers in real VM’s. Gave plenty of flexibility to product developers. OK Labs, formed out of NICTA’s research, did something similar with their OKL4 and OK Linux. Commercialized with user-mode VM’s for many mobile OS’s until General Dynamics acquired them.
Same strategy could be reused here. I figure it might be close to what dom0 does already if it’s a really stripped Linux. Just gotta make sure all code is removed that’s unnecessary for the drivers or multiplexing. Don’t even put management code in that one. Put it in another one or as native processes. I’d also use OpenBSD, which happened for Xen once I think, as the base for the drivers or filesystem as they’ll have lowest 0-days of FOSS code. Not sure how easy it is to strip as my last attempt was long before my memory loss. It’s worth trying, though, as an OpenBSD stripped to just drivers, filesystem, and maybe networking is already beneficial for security appliances.
“significant ongoing work AKA funding would be required for keeping up with and testing the on-going changes. ”
This could be why the project was talking about “desperate need” for help. It being labor intensive. The commercial deployments were on specific pieces of hardware that didn’t get updated much. Seems to support your point.
“NetBSD is I’m sure the version you’re thinking about”
I misremembered. NetBSD was the Xen one. OpenBSD was ported to L4. Still relevant given we’re talking about a port that lets drivers get reused. So, a DDEkit-like thing would need to be built-in to OpenBSD kernel.
“for OpenBSD’s BDFL doesn’t like the hypervisor concept”
They’ve changed their mind. Adoption-driven reasons I think. They’re actively working on an official hypervisor. I plan to compare it to VAX VMM and modern NOVA microhypervisor given their claimed skill about security & cleaner architecture. Those are the exemplars in each. You might enjoy watching him say it is quite different from the cocky style I saw when he dismissed it in the past. Cringed a little, too.
“it looks like NetBSD is still playing the Xen game, and I hope the rump kernel game as well, that might be the most fruitful way to get a bunch ‘o drivers designed for isolation.”
Yeah, they’re all over that. It’s still open for debate if it’s the best way to go. They are differentiating on it, though.
Well, by all means keep doing the work for fun and enlightenment. Always justified. :)
Not sure if Xen’s stuff will be securable since it wasn’t designed for it from start. If API is, then that implementation could benefit in that all kinds of stuff targeted to Xen would be immediately usable. That includes MirageOS.