I’d just like to know if there are subsets that could ideally be put into a POSIX layer and which subsets would not map well.
I feel like @anna.lyons had talked a little about this at the 2018 summit but I can’t remember what some of her points were.
It’s “practical” in the sense that it can be done, but that doesn’t mean it’s a good idea.
Posix is a 50-year-old OS API, and it shows.
One of the issues with Posix is that it mixes up files, networking, memory protection, and it has poor resource management. It is an API that assumes an OS with knowledge of global state, basically means you end up with a monolithic system design. Doing this on top of seL4 defeats the purpose, you might as well run a virtualised Linux server.
This design is just the opposite of what you want for seL4, where you want a design that minimises the trusted computing base (TCB), i.e. a multi-server design with minimal interdependencies between services.
Also, Posix objects tend to be pretty heavy-weight. Just compare the cost of creating an seL4 thread with a Posix thread.
While @gernot is correct that it isn’t practical to have entire POSIX layer, it’s possible that small subsets to get legacy software working make sense, especially for untrusted components, for prototyping, or for components where a linux guest is too heavy weight.
We’re working on support for newlib as an alternative to the muslc library, where newlib is much more modular, so presumably can be used to include subsets of POSIX. We’re also introducing a base (very minimal) runtime (see https://sel4.atlassian.net/projects/RFC/issues/RFC-2) which allows components to run without a c-runtime at all.
Currently this work is all blocked on a thread local storage patch to the kernel, which verification are working on as we speak.
It’s not clear if you mean support for a fully POSIX/SUS3 compliant layer (which would need to include shell, utility applications, networking services, etc.) or just the C library portion. In either case, a better and more constrained target would be targeting support of the C11 standard library first.
The major assumption that the C11 library makes is the assumption that every process has access to some key/value store that maps string names to capabilities of block and stream I/O objects. How that fits or abstracts over the seL4 model of capabilities is something that would require a lot of though.
In the case of POSIX, which requires some sense of a ‘global’ scope within which processes operate, it may make sense to have a framework for constructing isolated container-like systems which offer a POSIX world to the processes within them wherein processes that are built entirely on the POSIX API are constrained to that world but processes or libraries also using the underlying seL4 API (such as those for networks or filesystems) have some means of communicating with traditional seL4 (non-POSIX) processes outside of the POSIX container.
It is clear, however, that providing compatibility for POSIX on top of seL4 would require a lot of design work and forethought and would require some well-defined and reusable systems for managing and partitioning network, file-system, and shared memory access (among other OS services). As such, there is a lot that needs to be done before we can start to piece together an abstraction that satisfies even a minimal subset of the POSIX specification.