4 ms·

I think at this point the argument for or against microkernels is becoming moot. The only way to provide fast, efficient and safe access to privileged services

I think at this point the argument for or against microkernels is becoming moot. The only way to provide fast, efficient and safe access to privileged services is via hardware mitigations. Software can only do so much. It's like the difference between a 80286 and a 80386: The latter added the hardware support for true multitasking that the former lacked. Since then there's been an ever increasing number of hardware-level protection mechanisms added, like those which enabled hypervisors. Apple in particular has been adding a bunch of stuff to their SOCs to protect the kernel, drivers and components at the chip level, as well as enforce privileges on running threads and when using pointers. [1] This doesn't mean the OS is impenetrable, but it's a lot more effective than a software only strategy of managing privileges. Seems to me that utilizing this stuff (or similar), the architecture of the kernel really isn't that important any more. Am I off base? 1. https://support.apple.com/guide/security/operating-system-integrity-sec8b776536b/web https://support.apple.com/guide/security/operating-system-in...

vacuity 2y ago
That doesn't seem right. Even with strong hardware protections, how is Linux's TCB comparable to a microkernel? Unless it just recreates the exact same protection domains, there will be more vulnerability in Linux. Rather, the thing about hardware is primarily that it makes things more efficient. For example, microkernels nowadays are already quite robust because they make good use of certain hardware: the MMU. Then the small TCB of a microkernel gives the kernel credibiity, so the kernel and hardware together make for a solid infrastructure. So really it's a matter of how much "cheating" we're allowed to do with hardware, but microkernels overall utilize the protection better. Or see exokernels.
MisterTea 2y ago
> Am I off base? Yes. There is still plenty of work to be done in the OS research space. There has to be software interfaces and API's to all this new hardware. I also think there is a lot to be learned from using micro/hybrid systems which are much more composable. e.g. Plan 9 is a great example of a hybrid system which makes use of a singular protocol, 9P, to serve all objects in the system to userspace. It is hybrid because some parts are in-kernel to avoid the overhead of system calls such as IP, and TLS. Another interesting design aspect is how the in-kernel drivers are minimal mostly acting as a 9P interface to the hardware logic. This way you A. turn a machine object like a pointer or record into a seekable file and B. secured that file using standard unix permissions and C. can easily distribute the components across machines via a network. Now you can securely push the driver logic into a userspace program. And 9p is network and architecture transparent meaning you can work across multiple machines running on Arm, x86, mips, etc. All this come out of the box. When I go back to Linux/Unix or Windows from Plan 9 its a sad and frustrating time. They're about as flexible as igneous rock. All the features are ad-hoc bolted on in mutually incompatible ways using a myriad of protocols that all do the same thing - serve files/objects. Ugh.
indolering 2y ago
The utility of microkernels is orthogonal to hardware/software co-design. From a practical engineering perspective, monolithic kernels were faster/easier/had more resources behind them and security is as robust as can be had with C (i.e. best effort and full of bugs). Lots of hardware has been introduced to try and mitigate that mess. But you theoretically wouldn't need a security co-processor with SeL4 because you have a very high degree of confidence that processes are isolated from each other and there are no root level exploits. So yes, hardware/software codesign is important! That being said, the team behind SeL4 has had to spend a lot of engineering resources on eliminating side channels from the hardware. Hardware is also faulty as the real world doesn't care about your physics simulation. The benefits of a microkernel here is that it is small enough for formal verification to be tractable. The proof itself is 10x the size of the kernel. Context switching on SeL4 is an order of magnitude faster than Linux, so the performance impact should be negligible. But if we magically could verify the millions of lines of a monolithic kernel, then it would still be faster to not do context switching. Indeed, the SeL4 team tried to move the scheduler to userspace but it cost too much in terms of performance. So it was kept in and added to the proof burden.
Narishma 2y ago
> It's like the difference between a 80286 and a 80386: The latter added the hardware support for true multitasking that the former lacked. I'm not sure this is a good comparison. The 286 did support true multitasking in protected mode, and it was used in many non-DOS operating systems. What the 386 added (among other things) is the virtual 8086 mode which allowed it to multitask existing real mode DOS applications that accessed hardware directly.
- russellbeattie 2y ago
  Sorry, I'm a bit late responding. You're right! I should have used 8086 and 80286 as the example. 386 added virtual memory and some other stuff. Thanks

vacuity 2y ago

That doesn't seem right. Even with strong hardware protections, how is Linux's TCB comparable to a microkernel? Unless it just recreates the exact same protection domains, there will be more vulnerability in Linux. Rather, the thing about hardware is primarily that it makes things more efficient. For example, microkernels nowadays are already quite robust because they make good use of certain hardware: the MMU. Then the small TCB of a microkernel gives the kernel credibiity, so the kernel and hardware together make for a solid infrastructure. So really it's a matter of how much "cheating" we're allowed to do with hardware, but microkernels overall utilize the protection better. Or see exokernels.

MisterTea 2y ago

> Am I off base? Yes. There is still plenty of work to be done in the OS research space. There has to be software interfaces and API's to all this new hardware. I also think there is a lot to be learned from using micro/hybrid systems which are much more composable. e.g. Plan 9 is a great example of a hybrid system which makes use of a singular protocol, 9P, to serve all objects in the system to userspace. It is hybrid because some parts are in-kernel to avoid the overhead of system calls such as IP, and TLS. Another interesting design aspect is how the in-kernel drivers are minimal mostly acting as a 9P interface to the hardware logic. This way you A. turn a machine object like a pointer or record into a seekable file and B. secured that file using standard unix permissions and C. can easily distribute the components across machines via a network. Now you can securely push the driver logic into a userspace program. And 9p is network and architecture transparent meaning you can work across multiple machines running on Arm, x86, mips, etc. All this come out of the box. When I go back to Linux/Unix or Windows from Plan 9 its a sad and frustrating time. They're about as flexible as igneous rock. All the features are ad-hoc bolted on in mutually incompatible ways using a myriad of protocols that all do the same thing - serve files/objects. Ugh.

indolering 2y ago

The utility of microkernels is orthogonal to hardware/software co-design. From a practical engineering perspective, monolithic kernels were faster/easier/had more resources behind them and security is as robust as can be had with C (i.e. best effort and full of bugs). Lots of hardware has been introduced to try and mitigate that mess. But you theoretically wouldn't need a security co-processor with SeL4 because you have a very high degree of confidence that processes are isolated from each other and there are no root level exploits. So yes, hardware/software codesign is important! That being said, the team behind SeL4 has had to spend a lot of engineering resources on eliminating side channels from the hardware. Hardware is also faulty as the real world doesn't care about your physics simulation. The benefits of a microkernel here is that it is small enough for formal verification to be tractable. The proof itself is 10x the size of the kernel. Context switching on SeL4 is an order of magnitude faster than Linux, so the performance impact should be negligible. But if we magically could verify the millions of lines of a monolithic kernel, then it would still be faster to not do context switching. Indeed, the SeL4 team tried to move the scheduler to userspace but it cost too much in terms of performance. So it was kept in and added to the proof burden.

Narishma 2y ago

> It's like the difference between a 80286 and a 80386: The latter added the hardware support for true multitasking that the former lacked. I'm not sure this is a good comparison. The 286 did support true multitasking in protected mode, and it was used in many non-DOS operating systems. What the 386 added (among other things) is the virtual 8086 mode which allowed it to multitask existing real mode DOS applications that accessed hardware directly.

russellbeattie 2y ago
Sorry, I'm a bit late responding. You're right! I should have used 8086 and 80286 as the example. 386 added virtual memory and some other stuff. Thanks