3 ms·
> And yes, for a really critical system I might consider taking something much simpler and potentially slower but formally proven correct, like seL4. One of se
by Ieghaehia9 5y ago
> And yes, for a really critical system I might consider taking something much simpler and potentially slower but formally proven correct, like seL4.
One of seL4's points is that security can still be fast, no?
From https://docs.sel4.systems/projects/sel4/frequently-asked-questions.html https://docs.sel4.systems/projects/sel4/frequently-asked-que...
>To the best of our knowledge, seL4 is the world’s fastest microkernel on the supported processors, in terms of the usual ping-pong metric: the cost of a cross-address-space message-passing (IPC) operation.
- nine_k 5y agoYes. But within the Linux kernel, you might not need that cross-process IPC at all, so if you're into squeezing every last microsecond of latency, you likely want your entire app running as a monolith in kernel mode. But if you want security more than top speed, seL4 + a few daemons you write for other OS needs must be fine.