4 ms·

Well, I guess nothing qualifies then, because you can't have a WCET on commodity hardware. You'd have to have a CPU without any kind of cache (branch history, T

by burfog 7y ago

Well, I guess nothing qualifies then, because you can't have a WCET on commodity hardware. You'd have to have a CPU without any kind of cache (branch history, TLB, etc.) and without any kind of instruction scheduling. You couldn't even have two cores sharing a bus, either on chip or on the motherboard. Due to the above, security is also in question. Spectre and related troubles take care of that. Most people have a very different idea of "general purpose operating systems". It includes Linux. Microkernels have huge problems. Reality disagrees with Andrew S. Tanenbaum. Simplification of components does not come free. Those simple components can have fiendishly complex interactions with each other. Some proven-secure microkernel systems are really insecure because all the buggy code has been shoved into parts that don't count for the security audit. Practical data structure choices become very limited, killing performance. Context switches have always been costly, and the situation has suddenly gotten far worse because we now require Spectre mitigation. Remember also that performance problems are energy use problems. You might be willing to tolerate slowness, but consider battery life and the power fed into huge server farms.

snvzz 7y ago
>Most people have a very different idea of "general purpose operating systems". It includes Linux. A popular misconception is still a misconception. >all the buggy code has been shoved into parts that don't count for the security audit. I hate to repeat myself, but as explained above, at least the microkernel multiserver design has a chance of being secure, because it doesn't run more code than needed in supervisor mode, and isolates components individually. A monolith cannot, because it has an excessively large trusted computer base, which makes cost of proof impractical. >Microkernels have huge problems. Reality disagrees with Andrew S. Tanenbaum. I refer you to the last installment of the Linus-AST debate[0]. >killing performance. I recommend this article[1]. >Well, I guess nothing qualifies then, because you can't have a WCET on commodity hardware. You'd have to have a CPU without any kind of cache (branch history, TLB, etc.) and without any kind of instruction scheduling. You couldn't even have two cores sharing a bus, either on chip or on the motherboard. seL4 has WCET for x86. It simply assumes the worst case for all of this. And it's still a good WCET. I recommend you read the paper[2]. [0]: http://www.cosy.sbg.ac.at/~clausen/PVSE2006/linus-rebuttal.html http://www.cosy.sbg.ac.at/~clausen/PVSE2006/linus-rebuttal.h... [1]: https://web.archive.org/web/20200216184858/https://blog.darknedgy.net/technology/2016/01/01/0/ https://web.archive.org/web/20200216184858/https://blog.dark... [2]: https://www.cse.unsw.edu.au/~cs9242/15/papers/Blackham_SCRH_11.pdf https://www.cse.unsw.edu.au/~cs9242/15/papers/Blackham_SCRH_...
- burfog 7y ago
  So here is how it actually works with formal security audits, for example with an OS certified to EAL6 (Semiformally Verified Design and Tested). The OS vendor produces a boot loader and a simple task switcher that can pass messages. This is somewhat badly proven to be free of bugs. It's unimpressive because there is almost no code or functionality. Things like filesystems and TCP/IP stacks are full of security holes. None of that counts. All that buggy code gets linked into the user's app. Practically speaking, the app serves as a kernel without memory protection and the super-secure (Verified! Proven!) task switcher serves as a hypervisor. OK, so maybe nobody can hack into the simple task switcher that is supposedly an OS but actually a hypervisor. The big fat juicy app, containing most of a kernel, is as secure as VxWorks 5 or MacOS 9. It's not a good sign if you need to copy-and-paste the code for an old BSD network stack into your app. Maybe the theory is different, but in actual practice the above is really how the world of secure microkernels gets stuff done.
  - snvzz 7y ago
    Yes, that is terrible. But fortunately, what you've described is not the multiserver approach. This[0] is the kind of work done around seL4. [0]: https://ts.data61.csiro.au/projects/TS/SMACCM/ https://ts.data61.csiro.au/projects/TS/SMACCM/

by burfog 7y ago

snvzz 7y ago

>Most people have a very different idea of "general purpose operating systems". It includes Linux. A popular misconception is still a misconception. >all the buggy code has been shoved into parts that don't count for the security audit. I hate to repeat myself, but as explained above, at least the microkernel multiserver design has a chance of being secure, because it doesn't run more code than needed in supervisor mode, and isolates components individually. A monolith cannot, because it has an excessively large trusted computer base, which makes cost of proof impractical. >Microkernels have huge problems. Reality disagrees with Andrew S. Tanenbaum. I refer you to the last installment of the Linus-AST debate[0]. >killing performance. I recommend this article[1]. >Well, I guess nothing qualifies then, because you can't have a WCET on commodity hardware. You'd have to have a CPU without any kind of cache (branch history, TLB, etc.) and without any kind of instruction scheduling. You couldn't even have two cores sharing a bus, either on chip or on the motherboard. seL4 has WCET for x86. It simply assumes the worst case for all of this. And it's still a good WCET. I recommend you read the paper[2]. [0]: http://www.cosy.sbg.ac.at/~clausen/PVSE2006/linus-rebuttal.html http://www.cosy.sbg.ac.at/~clausen/PVSE2006/linus-rebuttal.h... [1]: https://web.archive.org/web/20200216184858/https://blog.darknedgy.net/technology/2016/01/01/0/ https://web.archive.org/web/20200216184858/https://blog.dark... [2]: https://www.cse.unsw.edu.au/~cs9242/15/papers/Blackham_SCRH_11.pdf https://www.cse.unsw.edu.au/~cs9242/15/papers/Blackham_SCRH_...

burfog 7y ago
So here is how it actually works with formal security audits, for example with an OS certified to EAL6 (Semiformally Verified Design and Tested). The OS vendor produces a boot loader and a simple task switcher that can pass messages. This is somewhat badly proven to be free of bugs. It's unimpressive because there is almost no code or functionality. Things like filesystems and TCP/IP stacks are full of security holes. None of that counts. All that buggy code gets linked into the user's app. Practically speaking, the app serves as a kernel without memory protection and the super-secure (Verified! Proven!) task switcher serves as a hypervisor. OK, so maybe nobody can hack into the simple task switcher that is supposedly an OS but actually a hypervisor. The big fat juicy app, containing most of a kernel, is as secure as VxWorks 5 or MacOS 9. It's not a good sign if you need to copy-and-paste the code for an old BSD network stack into your app. Maybe the theory is different, but in actual practice the above is really how the world of secure microkernels gets stuff done.
- snvzz 7y ago
  Yes, that is terrible. But fortunately, what you've described is not the multiserver approach. This[0] is the kind of work done around seL4. [0]: https://ts.data61.csiro.au/projects/TS/SMACCM/ https://ts.data61.csiro.au/projects/TS/SMACCM/