4 ms·

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 2y 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 2y 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 2y 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 2y ago
        Here is a good conversation on this subject: https://wiki.c2.com/?CapabilitySecurityDiscussion https://wiki.c2.com/?CapabilitySecurityDiscussion
• anthk 2y ago
  GNU Hurd. Also, why it's inadequate? "Unix 2.0" which is basically plan9/9front, uses namespaces, cpu, auth and so on 'servers' to authenticate users and even shared devices over the network.
  • sparkie 2y ago
    You could build a POSIX system on seL4, but it won't take advantage of the capabilities that seL4 provides, because capabilities are absent from the POSIX APIs. Consider for example: FILE *fopen(const char *filename, const char *mode) There's nothing in this function signature which specifies a capability to perform the open. Instead, there's an access control list somewhere else, where permission is looked up as to whether the file can be accessed by the current uid or whatever. Rule #1 of capabilities is: Don't separate designation from authority. Rather than a filename, a capability based API for opening files should take a capability argument instead of a filename, which both designates which file to open and provides the authority to open it, without attempting to look up that authority elsewhere. And notably, this capability cannot be forged - it can't be generated from a string containing the name of the file. So the first step to making a POSIX on seL4 is to get rid of the POSIX API and replace it with a better API based on capabilities. Then of course, it is no longer POSIX. The reason to use capabilities rather than ACLs is that ACLs are vulnerable to confused deputy attacks. Linux namespaces have numerous security vulnerabilities that could be avoided with capabilities. Also note that POSIX "capabilities" are not proper capabilities in the sense they're used in capability based security (as in seL4).
    • gnufx 2y ago
      Not arguing about the merits of capabilities and the open interface, but file handles are often cited as capability-like, and the ...at calls are in POSIX; but there's the global namespace. (Security in Plan 9 does say their capability system could be implemented for Unix, but I don't know if that's realistic and whether it provides proper capability security.)
    • anthk 2y ago
      Forget about POSIX under 9front. Also, Hurd does things differently.