6 ms·

This seems like an important part that's buried > Compared to monolithic Linux, there is a small performance tradeoff because of the µ-kernel architecture. How

This seems like an important part that's buried > Compared to monolithic Linux, there is a small performance tradeoff because of the µ-kernel architecture. However, the initial L4Linux has been somewhat optimized, and on L4/x86 it has a very acceptable slowdown of less than 4 % for any relevant load. If it provided any additional security guarantees in trade for that 4%, I imagine it'll become a popular way of running Linux

monocasa 8y ago
It doesn't really provide extra security for processes managed by the Linux kernel, but it allows you to co locate Linux and some other code. I could see a model where you have an untrusted Linux land running next to some unikernel like rtos-esque components that are protected from the Linux side. The sel4 guys had a CTF where they ran hard realtime heleicopter software next to a Linux kernel on the same system, and gave you a root shell to the Linux side to start off with. That being said, last time I checked even sel4 wasn't really hardened against Spectre attacks.
- wahern 8y ago
  By exposing kernel memory Spectre diminishes the effectiveness of mitigations like kernel ASLR as well as makes it easier more generally to exploit kernel vulnerabilities. That's significant in the case of Linux as there's no shortage of Linux kernel bugs, not now nor for the foreseeable future. Even well written, bug free user space applications can't protect themselves from the kernel, AMD's and Intel's best efforts with SEV and SGX, respectively, notwithstanding. By contrast seL4 is effectively bug free. (Literally bug free for the most the part, but AFAIU some gritty details like TLB management remain outside the scope of the formal verification.) That means you can build a reliable security model for your own application. The guarantees that model can make about confidentiality may be weaker because of Spectre, but you're still in an infinitely better position than on Linux, Windows, or most anywhere else. seL4 is arguably even better than ARM's TrustZone. With TrustZone you're still stuck having to ensure you correctly manage transitions into and out of protected mode. Bugs in such code constitute a good chunk of kernel vulnerabilities more generally, so it's clearly not trivial. Doing this correctly is basically what seL4 is all about. Then consider the fact that people are trying to push so many tasks into the TrustZone (or secure enclaves in general) that it's common to run an OS in the TrustZone. People would do much better to run seL4 inside the enclaves than bug ridden TEE environments. And unless the enclave is a discrete processor rather than a protected mode as with TrustZone, you may as well just run seL4 as the only OS (or at least the host OS). Interestingly, Apple's T1 and T2 chips run an L4-based microkernel. AFAIU it's something of a cousin to seL4 but predates it. If seL4 was as mature then as it is now perhaps Apple would have started with seL4.
  - monocasa 8y ago
    > By exposing kernel memory Spectre diminishes the effectiveness of mitigations like kernel ASLR as well as makes it easier more generally to exploit kernel vulnerabilities. That's significant in the case of Linux as there's no shortage of Linux kernel bugs, not now nor for the foreseeable future. Even well written, bug free user space applications can't protect themselves from the kernel, AMD's and Intel's best efforts with SEV and SGX, respectively, notwithstanding. I mean, yeah, that's what I'm saying. There's some benefit to to running stuff on the side of the kernel, but you gain nothing by running your Linux processes on L4Linux. > By contrast seL4 is effectively bug free. (Literally bug free for the most the part, but AFAIU some gritty details like TLB management remain outside the scope of the formal verification.) That means you can build a reliable security model for your own application. The guarantees that model can make about confidentiality may be weaker because of Spectre, but you're still in an infinitely better position than on Linux, Windows, or most anywhere else. The sel4 guys are super careful not to make such strong statements. And it's weird that you'd minimize the consequences of reading out arbitrary memory. > seL4 is arguably even better than ARM's TrustZone. With TrustZone you're still stuck having to ensure you correctly manage transitions into and out of protected mode. Bugs in such code constitute a good chunk of kernel vulnerabilities more generally, so it's clearly not trivial. Doing this correctly is basically what seL4 is all about. Then consider the fact that people are trying to push so many tasks into the TrustZone (or secure enclaves in general) that it's common to run an OS in the TrustZone. People would do much better to run seL4 inside the enclaves than bug ridden TEE environments. And unless the enclave is a discrete processor rather than a protected mode as with TrustZone, you may as well just run seL4 as the only OS (or at least the host OS). TrustZone and a microkernel sel4 are totally orthogonal concepts. Your contrasting the two concepts doesn't really make sense. And you can absolutely run sel4 in Secure EL1, you just wouldn't want to run it in EL3 because it's a little heavyweight in its current incarnation for that (hence the guy below talking about how it cut their perf in half). > Interestingly, Apple's T1 and T2 chips also runs an L4-based microkernel. AFAIU it's something of a cousin to seL4 but predates it. If seL4 was as mature then as it is now perhaps Apple would have started with it. It's an extremely modified L4:Pistachio that has AFAIK nothing to do with sel4.
  - j16sdiz 8y ago
    seL4 is bug free in theory, not in paratice. It have been proved to follow the spec, but the spec can have error. Missing workaround for hardware bug can bite too. "Beware of bugs in the above code; I have only proved it correct, not tried it." -- Donald Knuth on the van Emde Boas construction of priority deques (1977)
- 616c 8y ago
  That sounds like a very neat CTF. I'll search but do you know if anyone wrote about it or documented it?
- rurban 8y ago
  The Australian sel4 is not yet Spectre fixed, but the Dresden L4Re is.
aey 8y ago
4% is meaningless measurement for an OS kernel. I worked with l4 and we had to throw it out because the microcernel overhead had a 2x performance hit on frames per second for animations on a 400mhz arm9. Are you going to see a 2x hit for disk IOps, or network packets per second, or IO latency?
- microcolonel 8y ago
  > I worked with L4, and we had to throw it out because the microkernel overhead caused a 2x performance hit on frames per second for animations on a 400MHz ARM9. Were you sending individual graphics commands and rasters over IPC or something, or was that just the cost of the flips, and maybe a second flip from a compositor (or blitter)?
  - aey 8y ago
    Userspace would render its local window and send the invalidated regions to the kernel. The problem was two fold. L4 ipc was just slower then a swi, and l4 driver model would lock the page table for every region instead of just checking every region all at once.
    - microcolonel 8y ago
      Which L4 was this, by the way? Did you replace it with an RTOS, a POSIX system?
      - aey 8y ago
        We had an internal bear metal implementation already. L4 was just pushed as the “hotness”, and ironically as a way to get around the linux GPL issues at the time. I don’t want to sound to critical. L4 is actually easier to build drivers for than Linux, and you are much less likely to shoot yourself in the foot. It’s a great microckernel. It’s just that 4% may all come from the most human sensitive application.
        8y ago
naasking 8y ago
> If it provided any additional security guarantees in trade for that 4%, I imagine it'll become a popular way of running Linux It did. This was the precursor to hypervisors and the first example of virtualization with low overhead, which is now everywhere.

monocasa 8y ago

It doesn't really provide extra security for processes managed by the Linux kernel, but it allows you to co locate Linux and some other code. I could see a model where you have an untrusted Linux land running next to some unikernel like rtos-esque components that are protected from the Linux side. The sel4 guys had a CTF where they ran hard realtime heleicopter software next to a Linux kernel on the same system, and gave you a root shell to the Linux side to start off with. That being said, last time I checked even sel4 wasn't really hardened against Spectre attacks.

wahern 8y ago
By exposing kernel memory Spectre diminishes the effectiveness of mitigations like kernel ASLR as well as makes it easier more generally to exploit kernel vulnerabilities. That's significant in the case of Linux as there's no shortage of Linux kernel bugs, not now nor for the foreseeable future. Even well written, bug free user space applications can't protect themselves from the kernel, AMD's and Intel's best efforts with SEV and SGX, respectively, notwithstanding. By contrast seL4 is effectively bug free. (Literally bug free for the most the part, but AFAIU some gritty details like TLB management remain outside the scope of the formal verification.) That means you can build a reliable security model for your own application. The guarantees that model can make about confidentiality may be weaker because of Spectre, but you're still in an infinitely better position than on Linux, Windows, or most anywhere else. seL4 is arguably even better than ARM's TrustZone. With TrustZone you're still stuck having to ensure you correctly manage transitions into and out of protected mode. Bugs in such code constitute a good chunk of kernel vulnerabilities more generally, so it's clearly not trivial. Doing this correctly is basically what seL4 is all about. Then consider the fact that people are trying to push so many tasks into the TrustZone (or secure enclaves in general) that it's common to run an OS in the TrustZone. People would do much better to run seL4 inside the enclaves than bug ridden TEE environments. And unless the enclave is a discrete processor rather than a protected mode as with TrustZone, you may as well just run seL4 as the only OS (or at least the host OS). Interestingly, Apple's T1 and T2 chips run an L4-based microkernel. AFAIU it's something of a cousin to seL4 but predates it. If seL4 was as mature then as it is now perhaps Apple would have started with seL4.
- monocasa 8y ago
  > By exposing kernel memory Spectre diminishes the effectiveness of mitigations like kernel ASLR as well as makes it easier more generally to exploit kernel vulnerabilities. That's significant in the case of Linux as there's no shortage of Linux kernel bugs, not now nor for the foreseeable future. Even well written, bug free user space applications can't protect themselves from the kernel, AMD's and Intel's best efforts with SEV and SGX, respectively, notwithstanding. I mean, yeah, that's what I'm saying. There's some benefit to to running stuff on the side of the kernel, but you gain nothing by running your Linux processes on L4Linux. > By contrast seL4 is effectively bug free. (Literally bug free for the most the part, but AFAIU some gritty details like TLB management remain outside the scope of the formal verification.) That means you can build a reliable security model for your own application. The guarantees that model can make about confidentiality may be weaker because of Spectre, but you're still in an infinitely better position than on Linux, Windows, or most anywhere else. The sel4 guys are super careful not to make such strong statements. And it's weird that you'd minimize the consequences of reading out arbitrary memory. > seL4 is arguably even better than ARM's TrustZone. With TrustZone you're still stuck having to ensure you correctly manage transitions into and out of protected mode. Bugs in such code constitute a good chunk of kernel vulnerabilities more generally, so it's clearly not trivial. Doing this correctly is basically what seL4 is all about. Then consider the fact that people are trying to push so many tasks into the TrustZone (or secure enclaves in general) that it's common to run an OS in the TrustZone. People would do much better to run seL4 inside the enclaves than bug ridden TEE environments. And unless the enclave is a discrete processor rather than a protected mode as with TrustZone, you may as well just run seL4 as the only OS (or at least the host OS). TrustZone and a microkernel sel4 are totally orthogonal concepts. Your contrasting the two concepts doesn't really make sense. And you can absolutely run sel4 in Secure EL1, you just wouldn't want to run it in EL3 because it's a little heavyweight in its current incarnation for that (hence the guy below talking about how it cut their perf in half). > Interestingly, Apple's T1 and T2 chips also runs an L4-based microkernel. AFAIU it's something of a cousin to seL4 but predates it. If seL4 was as mature then as it is now perhaps Apple would have started with it. It's an extremely modified L4:Pistachio that has AFAIK nothing to do with sel4.
- j16sdiz 8y ago
  seL4 is bug free in theory, not in paratice. It have been proved to follow the spec, but the spec can have error. Missing workaround for hardware bug can bite too. "Beware of bugs in the above code; I have only proved it correct, not tried it." -- Donald Knuth on the van Emde Boas construction of priority deques (1977)
616c 8y ago
That sounds like a very neat CTF. I'll search but do you know if anyone wrote about it or documented it?
rurban 8y ago
The Australian sel4 is not yet Spectre fixed, but the Dresden L4Re is.

aey 8y ago

4% is meaningless measurement for an OS kernel. I worked with l4 and we had to throw it out because the microcernel overhead had a 2x performance hit on frames per second for animations on a 400mhz arm9. Are you going to see a 2x hit for disk IOps, or network packets per second, or IO latency?

microcolonel 8y ago
> I worked with L4, and we had to throw it out because the microkernel overhead caused a 2x performance hit on frames per second for animations on a 400MHz ARM9. Were you sending individual graphics commands and rasters over IPC or something, or was that just the cost of the flips, and maybe a second flip from a compositor (or blitter)?
- aey 8y ago
  Userspace would render its local window and send the invalidated regions to the kernel. The problem was two fold. L4 ipc was just slower then a swi, and l4 driver model would lock the page table for every region instead of just checking every region all at once.
  - microcolonel 8y ago
    Which L4 was this, by the way? Did you replace it with an RTOS, a POSIX system?
    - aey 8y ago
      We had an internal bear metal implementation already. L4 was just pushed as the “hotness”, and ironically as a way to get around the linux GPL issues at the time. I don’t want to sound to critical. L4 is actually easier to build drivers for than Linux, and you are much less likely to shoot yourself in the foot. It’s a great microckernel. It’s just that 4% may all come from the most human sensitive application.
      - 8y ago

naasking 8y ago

> If it provided any additional security guarantees in trade for that 4%, I imagine it'll become a popular way of running Linux It did. This was the precursor to hypervisors and the first example of virtualization with low overhead, which is now everywhere.