Re: [seL4] seL4 design principles

On 2020-03-11 03:00, Heiser, Gernot (Data61, Kensington NSW) wrote:

On 11 Mar 2020, at 12:46, Demi Obenour mailto:demiobenour@gmail.com> wrote:

...

1. Are high-level, hardware-independant libraries that wrap the low-level API planned?

Not only planned, they already exist to a degree. For example, CAmkES abstracts architecture, our userlevel libraries (mostly) abstract architecture.

Good to know!

...

2. Will it be possible to build a conventional (from an application perspective) OS on top of a multikernel, such that the application does not need to be aware that it is running on a multikernel?

In principle yes, a clustered multikernel would appear as a NUMA system. But presently we provide no user-level frameworks for this (as practically all of our present use cases are in the embedded space where multicores are closely clustered).

What would the overhead of this be? I would prefer to allow direct sharing of user-level memory. Since the kernel does not rely on the integrity of user-level memory, this should be fine if this memory is reserved at system startup, unless I am missing something. How well would seL4 handle systems like the Ampere Altra, which have 80 tightly-coupled cores on a single die? This seems to be the worst-case scenario: a big lock limits scalability, while there is no natural cluster size that I can think of.

...

3. What are the broken parts of POSIX mentioned?

I/O interfaces that force data copying.

For other Posix brokenness, see eg https://dl.acm.org/doi/abs/10.1145/3317550.3321435?casa_token=k6pcqUKP1doAAA...

Is Linux’s new io_uring interface a better one? In my experience, avoiding copies across trust boundaries creates a high risk of double-fetch and TOCTOU security vulnerabilities. Some that come to mind are XSA-155, XSA-166, and QSB#23. A filesystem that checksums data must copy the data before creating the checksum, since a malicious applications cannot cause the filesystem to be corrupted. On single-core systems, it might be possible to prevent untrusted code from executing while the checksum is made, but that won’t work on multicore. Sincerely, Demi