Yeah, that's by far the most likely. Note that one of Gernot's non-goals is "Stopping you from shooting yourself in the foot": this is to be taken seriously. Th

Yeah, that's by far the most likely. Note that one of Gernot's non-goals is "Stopping you from shooting yourself in the foot": this is to be taken seriously. The userland libraries provided by SeL4 have no proof evidence at all, and IME look and feel like any other C codebase. It's very likely that they the same class of security problems. Further, it's /very/ difficult to build anything on SeL4 without using said libraries (ease of use is another non-goal, remember?), so I'd expect many real systems to be built on them and thus share some class if issues among them.