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.
SeL4 Whitepaper [pdf]
11–20 of 31 posts
Re: SeL4 Whitepaper [pdf]
#12i've been working on and off (mostly off) on https://robigalia.org/ for five years now, and interned with the sel4 verification team. feel free to swing by freenode#robigalia if you you want to chat sel4 or trustworthy software, there's a small group collected over the years that would love to answer your questions :)
Thanks for posting. ~yearly I look at your site (idly, not likely to have anything to contribute) because Robigalia sounded very interesting when first discussed here at https://news.ycombinator.com/item?id=10848890
ty for the kind words! i'm hoping 2021 will bring a working demo of some basic goals :) the rust ecosystem has moved a long way since 2015, async/await finally being everywhere is a gamechanger because almost everything is async/await for us!
Re: SeL4 Whitepaper [pdf]
#13i've been working on and off (mostly off) on https://robigalia.org/ for five years now, and interned with the sel4 verification team. feel free to swing by freenode#robigalia if you you want to chat sel4 or trustworthy software, there's a small group collected over the years that would love to answer your questions :)
What’s your opinion on the scalability of formal methods? Isn’t it still the case that basically formal verification is impossible to do for larger code bases (like at least 10-100x that of sel4 in lines of code) and even sel4 took many many years and experts?
Re: SeL4 Whitepaper [pdf]
#14What 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.
Re: SeL4 Whitepaper [pdf]
#15In a past life, I pushed hard for more investment in seL4 for certain defense applications. The nuance isn't to be underestimated though – I can say from experience that it's often a hard sell to folks that aren't already versed in the ins and outs of formal methods, security, kernels/operating systems, etc. There are plenty of lower hanging fruit (like networking hardware) than the applications I worked on, yet commercial adoption still seems low. Maybe this is due to that nuance. To the credit of the folks at Trustworthy Systems and UNSW, they've done a great job producing literature that outlines the business case in a manner palatable to decision makers. This paper [0] in particular came in handy to me many times.
[0] https://ts.data61.csiro.au/publications/csiro_full_text/Klei...
Re: SeL4 Whitepaper [pdf]
#16What 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.
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.
Re: SeL4 Whitepaper [pdf]
#17Does anyone have more information about where sel4 is used in production?
Self driving cars via driveghost.com: "Ghost has assembled a team of leading experts in formal methods, an approach to software development that makes it possible to build complex software systems that can be proven to run without bugs or errors. Unlike existing systems built on error-prone platforms, Ghost will be the first to bring formal methods to the roadways with the world's only formally verified runtime built for your car, delivering you bug-free driving and unparalleled safety behind the wheel."
Re: SeL4 Whitepaper [pdf]
#18What 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 p…
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.
Re: SeL4 Whitepaper [pdf]
#19In a past life, I pushed hard for more investment in seL4 for certain defense applications. The nuance isn't to be underestimated though – I can say from experience that it's often a hard sell to folks that aren't already versed in the ins and outs of formal methods, security, kernels/operating systems, etc. There are plenty of lower hanging fruit (like networking hardware) than the applications I worked on, yet comm…
We had very similar 'discussions' about using Ada (or other 'safe' language) and/or TCSEC rated systems for security sensitive systems in the 80s and 90s. With abundant rationales for why that was a good idea. We've ended up with (mostly) C/C++ and COTS OSes, hopefully dressed up with a STIG (or similar) to close the really blatant holes.
I don't think the market has reached the point where the overhead of these technologies has been offset by the pain of endless security incidents. I don't even think we're close to being willing to take on a 'better way (YMMV)' instead of 'move fast and break things (no matter the cost to the consumer)'.
Re: SeL4 Whitepaper [pdf]
#20I wonder if seL4 would make a better basis for Qubes than the Xen it is on now.
In particular, does Xen provide anything seL4 doesn't?