4 ms·

What about seL4[1]? It isn't real-time, but it is small, performant, and formally verified. [1]: http://sel4.systems http://sel4.systems

• Animats 11y ago
  seL4 is quite good, but their approach to message passing has a problem. Messages are limited to a few bytes passed in registers. Anything bigger has to be done through shared memory between processes. This is great for the kernel; it never has to do a long operation like a big copy, so there's an upper bound on the time for each kernel operation. But with shared memory, one process may be able to mess up another. The usual library for L4 shared memory puts multiple "chunks" into one shared memory area, with an allocator. "A shared memory area can have multiple chunks."[1] Messing with the chunk structure or the wrong chunk from one process may adversely affect another one. That's a bad kind of attack surface. So, although the kernel is secure, server processes with higher privileges than their callers may not be. Since this is how processes talk to file systems and drivers, it's an obvious way to attack. QNX copies data from one process space to another. This adds copying overhead, but it's usually not too bad, because 1) most messages are short, and 2) if you just created a message and sent it, it's in the cache. In practice, the big overhead item today is context switching. [1] http://l4re.org/doc/group__api__l4shm.html http://l4re.org/doc/group__api__l4shm.html
  • xj9 11y ago
    Do you think anything could be done to mitigate or fix that? I've only recently started digging into seL4 so I don't know if this is an unavoidable problem (in terms of proving correctness) or if it even needs to be solved in-kernel.