7 ms·

Will it be possible to run a web browser on an SeL4 kernel some day, or is that completely beside the point? Obviously, formally verifying a modern web browser

Will it be possible to run a web browser on an SeL4 kernel some day, or is that completely beside the point? Obviously, formally verifying a modern web browser with a javascript engine and everything is a whole other undertaking, so I'll leave that aside. But the notion of using a very secure kernel as the base OS is appealing. Even if a hostile site broke out of the web browser, SeL4 should keep it sandboxed. Presumably, SeL4 could enforce isolation between different browser tabs. Is this something we can look forward to in the future, or are the performance expectations of modern javascript heavy web sites out of line with what SeL4 is likely to deliver? Anyway, there are plenty of other applications beside the web, so glad to see that SeL4 is being used in real world deployments.

wmf 7y ago
Technically, a capability-based desktop OS makes perfect sense. In practice, the microkernel people have been polishing their kernels and about to start on userspace next year... for 30 years. (One exception to this is QNX which was killed off by weird business decisions.)
- pjmlp 7y ago
  My Android devices running userspace drivers written in a mix of Java and C++ thanks to Project Treble seem like a step into the right direction. Or the new userspace device driver model introduced by Catalina. As per WWDC, for every new user space driver API, the old kernel one will be automatically marked as legacy and removed after one OS release, with the long term roadmap to replace all the kernel API extensions. Just like Windows 10 increases the amount of sandboxing with each bi-annual release.
  - StudentStuff 7y ago
    Userspace drivers permit upgrading the kernel to a certain point (depending on how kernel APIs change), but your forever trapped with the bugs and vulnerabilities in the userspace blobs. Its a step forward in kernel upgradability, but it also takes the pressure off vendors like Qualcomm and ARM to upstream their patches. I hope the kernel continues making significant changes that break out of tree, proprietary drivers. The harder it is for these players to act in bad faith, the sooner they'll collaborate with the kernel developers and mainline their code.
    - wmf 7y ago
      What if we pressure Qualcomm and ARM for 20 years but they still don't upstream anything? What about 50 years? Would you change your position?
      - StudentStuff 7y ago
        So long as they're spending most of their cash on maintaining out of tree patchesets for the Linux kernel, that is tens to hundreds of millions a year in wasted money on their part. Eventually the community will write their own drivers (as has happened with Mali) and the respective vendor will have a reckoning internally (like what happened with AMD's GPU driver) whereby those advocating for wasting money on out of tree code leave the organization with egg on their face for bilking the company out of significant R&D cash. It is very hard to claim that its worth it to develop a proprietary driver when a comparable performance driver already exists for your hardware in-tree. The in-tree driver will almost certainly be easier to use & break less often than out of tree code that the kernel devs don't think or care about breaking.
    - pjmlp 7y ago
      As proven by every other OS with proper driver ABI, this isn't an issue. And as proven by FOSS drivers that eventually got purged from kernel tree, having source available is meaningless if everyone just lets the code rotten to the point of being purged. As for pressuring vendors, the source code is available, and the license allows them to never upstream, it isn't as if Joe and Jane know what that is when buying a new phone.
      - StudentStuff 7y ago
        Windows has had multiple breaking changes to the driver ABI between Windows XP and present. There is no "proper" futureproof driver ABI, otherwise there would be a major OS using one.
        pjmlp 7y ago
        In almost 40 years, there were two breaking changes from 9X to NT family, from XP to Vista. Two. Linux? Who's counting anyway.
- garmaine 7y ago
  And Minix which runs inside every Intel CPU.
- ac29 7y ago
  > QNX which was killed off Are you sure? The latest version is only ~2 years old, and they still seem to be hiring: https://bb.wd3.myworkdayjobs.com/QNX https://bb.wd3.myworkdayjobs.com/QNX
  - wmf 7y ago
    It looks like the desktop version of QNX was killed off in 2014 although they stopped promoting it much earlier.
  - ahartmetz 7y ago
    There are some in-car infotainment systems and dashboards running on QNX. It's a fairly pleasant system to work with.
  - Matthias247 7y ago
    I was in the automotive industry. 10 years ago every infotainment System I had seen was either built on QNX or windows CE. When I left the industry later all systems I interacted with had moved to Linux. Why? Driver and off the shelf application support was a big reason. For QNX every driver had been ported, which is a huge task for something like a modern GPU.
- flo123456 7y ago
  Take a look at Genode. It‘s come quite far in that regard. https://genode.org/ https://genode.org/
snvzz 7y ago
To see what seL4 can do in practice in a desktop/workstation/server context, I suggest you take a look at Genode. Particularly, their recent dynamic system images.
nickpsecurity 7y ago
High-assurance security did do work on secure browsers. One prototype inspired Chrome's model. Here's an old thread where I listed some: https://news.ycombinator.com/item?id=9962444 https://news.ycombinator.com/item?id=9962444 One or more might be integrated into seL4. Alternatively, components in something like IBOS might be done with higher assurance like seL4 or Muen.
kragen 7y ago
You can run Linux under L4, as mentioned in the post. I understand this is a common thing to do on phones with Qualcomm chips, using OKL4. But that isn't to protect you from malicious software; it's to protect malicious software from you. Qubes is a similar system with more praiseworthy aims, but not using L4 as the hypervisor. Running a web browser directly on a microkernel is a reasonable thing to do, and it's likely that Fuchsia will end up doing it, but it will involve a lot of work. The performance expectations of JS generally do not have anything to do with the operating system, but as explained in the post, when it comes to fundamental OS services, seL4 is more than an order of magnitude faster than even other microkernels, much less FreeBSD, Linux, or Microsoft Windows. Microkernels generally need higher performance for those things because operations such as read(), which involve just a system call on a monolithic kernel, with context switches into and out of the kernel, involve a full context switch to a separate server process and back on a microkernel.
- michaelmrose 7y ago
  >...when it comes to fundamental OS services, seL4 is more than an order of magnitude faster than even other microkernels, much less FreeBSD, Linux, or Microsoft Windows. This seems to imply that seL4 is faster than FreeBSD, Linux, Windows is this what was intended to be conveyed?
  - kragen 7y ago
    Yes, but most of what you do on a computer isn't bottlenecked on the kernel—less still on a microkernel. So this doesn't necessarily mean the computer will feel faster or finish computing sooner.
    - michaelmrose 7y ago
      Questions about performance are often complicated affairs that involve considering all factors including hardware, software, data operated on, etc to get meaningful answers. That said I don't think data exists to show that SeL4 is faster than mainstream OS kernels just much faster than research microkernels which have always been much much slower than mainstream monolithic kernels. In fact one would reasonably suppose that it would be measurably slower due to increased overhead. This may well be well worth it but this doesn't mean we ought to engage in speculation not backed by data.

wmf 7y ago

Technically, a capability-based desktop OS makes perfect sense. In practice, the microkernel people have been polishing their kernels and about to start on userspace next year... for 30 years. (One exception to this is QNX which was killed off by weird business decisions.)

pjmlp 7y ago
My Android devices running userspace drivers written in a mix of Java and C++ thanks to Project Treble seem like a step into the right direction. Or the new userspace device driver model introduced by Catalina. As per WWDC, for every new user space driver API, the old kernel one will be automatically marked as legacy and removed after one OS release, with the long term roadmap to replace all the kernel API extensions. Just like Windows 10 increases the amount of sandboxing with each bi-annual release.
- StudentStuff 7y ago
  Userspace drivers permit upgrading the kernel to a certain point (depending on how kernel APIs change), but your forever trapped with the bugs and vulnerabilities in the userspace blobs. Its a step forward in kernel upgradability, but it also takes the pressure off vendors like Qualcomm and ARM to upstream their patches. I hope the kernel continues making significant changes that break out of tree, proprietary drivers. The harder it is for these players to act in bad faith, the sooner they'll collaborate with the kernel developers and mainline their code.
  - wmf 7y ago
    What if we pressure Qualcomm and ARM for 20 years but they still don't upstream anything? What about 50 years? Would you change your position?
    - StudentStuff 7y ago
      So long as they're spending most of their cash on maintaining out of tree patchesets for the Linux kernel, that is tens to hundreds of millions a year in wasted money on their part. Eventually the community will write their own drivers (as has happened with Mali) and the respective vendor will have a reckoning internally (like what happened with AMD's GPU driver) whereby those advocating for wasting money on out of tree code leave the organization with egg on their face for bilking the company out of significant R&D cash. It is very hard to claim that its worth it to develop a proprietary driver when a comparable performance driver already exists for your hardware in-tree. The in-tree driver will almost certainly be easier to use & break less often than out of tree code that the kernel devs don't think or care about breaking.
  - pjmlp 7y ago
    As proven by every other OS with proper driver ABI, this isn't an issue. And as proven by FOSS drivers that eventually got purged from kernel tree, having source available is meaningless if everyone just lets the code rotten to the point of being purged. As for pressuring vendors, the source code is available, and the license allows them to never upstream, it isn't as if Joe and Jane know what that is when buying a new phone.
    - StudentStuff 7y ago
      Windows has had multiple breaking changes to the driver ABI between Windows XP and present. There is no "proper" futureproof driver ABI, otherwise there would be a major OS using one.
      - pjmlp 7y ago
        In almost 40 years, there were two breaking changes from 9X to NT family, from XP to Vista. Two. Linux? Who's counting anyway.
garmaine 7y ago
And Minix which runs inside every Intel CPU.
ac29 7y ago
> QNX which was killed off Are you sure? The latest version is only ~2 years old, and they still seem to be hiring: https://bb.wd3.myworkdayjobs.com/QNX https://bb.wd3.myworkdayjobs.com/QNX
- wmf 7y ago
  It looks like the desktop version of QNX was killed off in 2014 although they stopped promoting it much earlier.
- ahartmetz 7y ago
  There are some in-car infotainment systems and dashboards running on QNX. It's a fairly pleasant system to work with.
- Matthias247 7y ago
  I was in the automotive industry. 10 years ago every infotainment System I had seen was either built on QNX or windows CE. When I left the industry later all systems I interacted with had moved to Linux. Why? Driver and off the shelf application support was a big reason. For QNX every driver had been ported, which is a huge task for something like a modern GPU.
flo123456 7y ago
Take a look at Genode. It‘s come quite far in that regard. https://genode.org/ https://genode.org/

snvzz 7y ago

To see what seL4 can do in practice in a desktop/workstation/server context, I suggest you take a look at Genode. Particularly, their recent dynamic system images.

nickpsecurity 7y ago

High-assurance security did do work on secure browsers. One prototype inspired Chrome's model. Here's an old thread where I listed some: https://news.ycombinator.com/item?id=9962444 https://news.ycombinator.com/item?id=9962444 One or more might be integrated into seL4. Alternatively, components in something like IBOS might be done with higher assurance like seL4 or Muen.

kragen 7y ago

You can run Linux under L4, as mentioned in the post. I understand this is a common thing to do on phones with Qualcomm chips, using OKL4. But that isn't to protect you from malicious software; it's to protect malicious software from you. Qubes is a similar system with more praiseworthy aims, but not using L4 as the hypervisor. Running a web browser directly on a microkernel is a reasonable thing to do, and it's likely that Fuchsia will end up doing it, but it will involve a lot of work. The performance expectations of JS generally do not have anything to do with the operating system, but as explained in the post, when it comes to fundamental OS services, seL4 is more than an order of magnitude faster than even other microkernels, much less FreeBSD, Linux, or Microsoft Windows. Microkernels generally need higher performance for those things because operations such as read(), which involve just a system call on a monolithic kernel, with context switches into and out of the kernel, involve a full context switch to a separate server process and back on a microkernel.

michaelmrose 7y ago
>...when it comes to fundamental OS services, seL4 is more than an order of magnitude faster than even other microkernels, much less FreeBSD, Linux, or Microsoft Windows. This seems to imply that seL4 is faster than FreeBSD, Linux, Windows is this what was intended to be conveyed?
- kragen 7y ago
  Yes, but most of what you do on a computer isn't bottlenecked on the kernel—less still on a microkernel. So this doesn't necessarily mean the computer will feel faster or finish computing sooner.
  - michaelmrose 7y ago
    Questions about performance are often complicated affairs that involve considering all factors including hardware, software, data operated on, etc to get meaningful answers. That said I don't think data exists to show that SeL4 is faster than mainstream OS kernels just much faster than research microkernels which have always been much much slower than mainstream monolithic kernels. In fact one would reasonably suppose that it would be measurably slower due to increased overhead. This may well be well worth it but this doesn't mean we ought to engage in speculation not backed by data.