6 ms·

From L3 to seL4: 20 years of L4 microkernels (2013) [video]

deleted 3y ago
[deleted]
defrost 3y ago
SOSP 2013 Proceedings of the Twenty-Fourth ACM Symposium on Operating Systems Principles November 2013 https://dl.acm.org/doi/10.1145/2517349.2522720 https://dl.acm.org/doi/10.1145/2517349.2522720
BSDobelix 3y ago
Question, and please don't get mad at me if I'm fundamentally wrong. Are there any projects trying to make a universal UNIX operating system with sel4? I know of Genode, but is there anything more simple/traditional? PS: Helios is also there but not based directly on seL4
- jacobgorm 3y ago
  I think one problem is that SEL4 lacks proper multi-core support. According to the FAQ it has not been formally verified, and it relies on a big lock for everything. This is fine when powering a security chip like T2, but not so fine if you are trying to replace UNIX.
- hresvelgr 3y ago
  Not Unix but Lions OS[1]. Also, why would you want to build Unix on top of seL4? I think we can have better ideas than that in today's state of the art. [1] https://trustworthy.systems/projects/LionsOS/ https://trustworthy.systems/projects/LionsOS/
  - TacticalCoder 3y ago
    > I think we can have better ideas than that in today's state of the art. And yet Unix is powering all the supercomputers, six of the seven magnificent seven, the AI revolution, nearly every single computer in all the datacenters around the world, billions of "small" devices, etc. Can we really do that much better or is it just hubris? At what point another approach, like the one Windows used, would be considered a failure? Once it's only powering the corporate world and not much else? And at what point another approach would be considered a success? Once it has replaced Unix on all the supercomputers and in all the datacenters? People like to snob Unix but the fact is: the world runs on Unix. P.S: I wrote "Unix" with an 'i' and not a star because I have no clue how to write a star in HN's powerful text editor ; )
    - onjectic 3y ago
      The world runs on Unix and as a consequence, computer viruses, malware, spyware and ransomware are all common vocabulary terms. We traded this security away for nothing. Linus Torvalds would have told you its system call performance, but Linux is also forced to solve these problems with things like futexes and io_uring, which carry over just as easily to microkernels. Nowadays the excuse is side-channel attacks make any attempts at security pointless anyways so the kernel has exploded in size and complexity. This is insane logic, not least of all because side-channel attacks are read-only and can’t embed themselves into your system permanently through a bug in a browser JIT. Linux is used purely because of all of its drivers and familiarity. Not on technical merits.
      - snvzz 3y ago
        >side-channel attacks Can be prevented[0][1][2]. 0. https://trustworthy.systems/publications/ https://trustworthy.systems/publications/ 1. https://trustworthy.systems/publications/papers/Sison_BMKH_23.abstract https://trustworthy.systems/publications/papers/Sison_BMKH_2... 2. https://trustworthy.systems/publications/papers/Buckley_SWMMKH_23.abstract https://trustworthy.systems/publications/papers/Buckley_SWMM...
    - hresvelgr 3y ago
      > People like to snob Unix but the fact is: the world runs on Unix. The world you are aware of runs on it. > Can we really do that much better or is it just hubris? Yes. Have a look at seL4[1] and Barrelfish too[2], even though that's no longer active. seL4 in particular is powering a lot of highly secure computing systems. There is a surprisingly large sphere outside of Unix/POSIX. [1] https://sel4.systems/ https://sel4.systems/ [2] https://barrelfish.org/ https://barrelfish.org/
    - pjmlp 3y ago
      You mean the world that is now full of hypervisors, containers and managed language runtimes, completely very much not UNIX?
  - BSDobelix 3y ago
    >Also, why would you want to build Unix on top of seL4? Thank you very much for the link, and yes you are absolutely right. I should have wrote unix'i or plan9'i or better just a universal operating-system, i meant with that not just a hypervisor but a "real/full" os on top of seL4.
- 4ad 3y ago
  The problem with Unix is the abstractions it provides, not its implementation. Basing Unix off seL4 changes nothing of what makes Unix inadequate in 2024.
  - tremon 3y ago
    The problem with Unix is that the abstractions don't match today's adversarial computing environment. If seL4 can provide kernel-level process (tree) isolation, which part of Unix is inadequate for 2024?
    - onjectic 3y ago
      It’s fundamentally full of concepts incompatible with capability based security principles, which are provably secure. Access control lists are provably insecure. POSIX resource management is archaic. It’s not possible to define “ownership” clearly on a Unix system. You could certainly write a Unix abstraction layer on top of seL4, or more commonly treat seL4 as a hypervisor, but you would not be able simply use a Unix interface to interact with seL4 and get all of it’s benefits. Capability based systems don’t magically carry their desired properties up the abstraction ladder, they have to be maintained and the designer has to be vigilant to avoid introducing ambient authority by using capability based design themselves. Genode is an example of a layer over seL4 that follows these principles.
      - gnufx 3y ago
        > Access control lists are provably insecure. If it's not too late to ask, where can we read about that? I've only ever seen ACL v. capability discussed in terms of trades-off as far as I remember.
        onjectic 3y ago
        Here is a good conversation on this subject: https://wiki.c2.com/?CapabilitySecurityDiscussion https://wiki.c2.com/?CapabilitySecurityDiscussion
  - 3y ago
adamretter 3y ago
That video is from 2013. Is anyone aware of an update for the last ten years which covers 2013 to 2023? I would like to understand if seL4 is still considered "current" or there have been newer developments since then that are worth considering. I have searched around a bit, and apart from Google's Fuscia Zircon, or Unikernel's like UniKraft, other L4 spin-offs and XNU I am not finding too much about newer modern microkernels.
- bregma 3y ago
  QNX 8.0 was just released. The version bump represents a rewritten microkernel.
  - speed_spread 3y ago
    Is QNX 8 seL4 based?
    - DoingIsLearning 3y ago
      QNX predates the first L4 release by at least 10 years. Unless they had a major rewrite I wouldn't assume so.
      - speed_spread 3y ago
        The comment I was replying to seemed to imply that QNX 8.0 is a full rewrite. I'm not sure how relevant that statement was here, unless the rewrite is seL4 based.
      - ahartmetz 3y ago
        Interestingly, QNX designers have learned and applied one of the same lessons as L4 designers: asynchronous messaging is messy regarding resource management and slower than well-executed synchronous messaging. QNX and L4 both use synchronous messaging for the vast majority of tasks.
        3y ago

deleted 3y ago

[deleted]

SOSP 2013 Proceedings of the Twenty-Fourth ACM Symposium on Operating Systems Principles November 2013 https://dl.acm.org/doi/10.1145/2517349.2522720 https://dl.acm.org/doi/10.1145/2517349.2522720

BSDobelix 3y ago

Question, and please don't get mad at me if I'm fundamentally wrong. Are there any projects trying to make a universal UNIX operating system with sel4? I know of Genode, but is there anything more simple/traditional? PS: Helios is also there but not based directly on seL4

jacobgorm 3y ago
I think one problem is that SEL4 lacks proper multi-core support. According to the FAQ it has not been formally verified, and it relies on a big lock for everything. This is fine when powering a security chip like T2, but not so fine if you are trying to replace UNIX.
hresvelgr 3y ago
Not Unix but Lions OS[1]. Also, why would you want to build Unix on top of seL4? I think we can have better ideas than that in today's state of the art. [1] https://trustworthy.systems/projects/LionsOS/ https://trustworthy.systems/projects/LionsOS/
- TacticalCoder 3y ago
  > I think we can have better ideas than that in today's state of the art. And yet Unix is powering all the supercomputers, six of the seven magnificent seven, the AI revolution, nearly every single computer in all the datacenters around the world, billions of "small" devices, etc. Can we really do that much better or is it just hubris? At what point another approach, like the one Windows used, would be considered a failure? Once it's only powering the corporate world and not much else? And at what point another approach would be considered a success? Once it has replaced Unix on all the supercomputers and in all the datacenters? People like to snob Unix but the fact is: the world runs on Unix. P.S: I wrote "Unix" with an 'i' and not a star because I have no clue how to write a star in HN's powerful text editor ; )
  - onjectic 3y ago
    The world runs on Unix and as a consequence, computer viruses, malware, spyware and ransomware are all common vocabulary terms. We traded this security away for nothing. Linus Torvalds would have told you its system call performance, but Linux is also forced to solve these problems with things like futexes and io_uring, which carry over just as easily to microkernels. Nowadays the excuse is side-channel attacks make any attempts at security pointless anyways so the kernel has exploded in size and complexity. This is insane logic, not least of all because side-channel attacks are read-only and can’t embed themselves into your system permanently through a bug in a browser JIT. Linux is used purely because of all of its drivers and familiarity. Not on technical merits.
    - snvzz 3y ago
      >side-channel attacks Can be prevented[0][1][2]. 0. https://trustworthy.systems/publications/ https://trustworthy.systems/publications/ 1. https://trustworthy.systems/publications/papers/Sison_BMKH_23.abstract https://trustworthy.systems/publications/papers/Sison_BMKH_2... 2. https://trustworthy.systems/publications/papers/Buckley_SWMMKH_23.abstract https://trustworthy.systems/publications/papers/Buckley_SWMM...
  - hresvelgr 3y ago
    > People like to snob Unix but the fact is: the world runs on Unix. The world you are aware of runs on it. > Can we really do that much better or is it just hubris? Yes. Have a look at seL4[1] and Barrelfish too[2], even though that's no longer active. seL4 in particular is powering a lot of highly secure computing systems. There is a surprisingly large sphere outside of Unix/POSIX. [1] https://sel4.systems/ https://sel4.systems/ [2] https://barrelfish.org/ https://barrelfish.org/
  - pjmlp 3y ago
    You mean the world that is now full of hypervisors, containers and managed language runtimes, completely very much not UNIX?
- BSDobelix 3y ago
  >Also, why would you want to build Unix on top of seL4? Thank you very much for the link, and yes you are absolutely right. I should have wrote unix'i or plan9'i or better just a universal operating-system, i meant with that not just a hypervisor but a "real/full" os on top of seL4.
4ad 3y ago
The problem with Unix is the abstractions it provides, not its implementation. Basing Unix off seL4 changes nothing of what makes Unix inadequate in 2024.
- tremon 3y ago
  The problem with Unix is that the abstractions don't match today's adversarial computing environment. If seL4 can provide kernel-level process (tree) isolation, which part of Unix is inadequate for 2024?
  - onjectic 3y ago
    It’s fundamentally full of concepts incompatible with capability based security principles, which are provably secure. Access control lists are provably insecure. POSIX resource management is archaic. It’s not possible to define “ownership” clearly on a Unix system. You could certainly write a Unix abstraction layer on top of seL4, or more commonly treat seL4 as a hypervisor, but you would not be able simply use a Unix interface to interact with seL4 and get all of it’s benefits. Capability based systems don’t magically carry their desired properties up the abstraction ladder, they have to be maintained and the designer has to be vigilant to avoid introducing ambient authority by using capability based design themselves. Genode is an example of a layer over seL4 that follows these principles.
    - gnufx 3y ago
      > Access control lists are provably insecure. If it's not too late to ask, where can we read about that? I've only ever seen ACL v. capability discussed in terms of trades-off as far as I remember.
      - onjectic 3y ago
        Here is a good conversation on this subject: https://wiki.c2.com/?CapabilitySecurityDiscussion https://wiki.c2.com/?CapabilitySecurityDiscussion
- 3y ago

adamretter 3y ago

That video is from 2013. Is anyone aware of an update for the last ten years which covers 2013 to 2023? I would like to understand if seL4 is still considered "current" or there have been newer developments since then that are worth considering. I have searched around a bit, and apart from Google's Fuscia Zircon, or Unikernel's like UniKraft, other L4 spin-offs and XNU I am not finding too much about newer modern microkernels.

bregma 3y ago
QNX 8.0 was just released. The version bump represents a rewritten microkernel.
- speed_spread 3y ago
  Is QNX 8 seL4 based?
  - DoingIsLearning 3y ago
    QNX predates the first L4 release by at least 10 years. Unless they had a major rewrite I wouldn't assume so.
    - speed_spread 3y ago
      The comment I was replying to seemed to imply that QNX 8.0 is a full rewrite. I'm not sure how relevant that statement was here, unless the rewrite is seL4 based.
    - ahartmetz 3y ago
      Interestingly, QNX designers have learned and applied one of the same lessons as L4 designers: asynchronous messaging is messy regarding resource management and slower than well-executed synchronous messaging. QNX and L4 both use synchronous messaging for the vast majority of tasks.
      - 3y ago