On 1 Aug 2021, at 11:36, Jimmy Brush via Devel <devel@sel4.systems<mailto:devel@sel4.systems>> wrote: On 8/1/21, Gernot Heiser wrote: On 1 Aug 2021, at 10:12, William ML Leslie <william.leslie.ttg@gmail.com<mailto:william.leslie.ttg@gmail.com>> wrote: Wouldn't there be a risk that a Linux system call would present an argument that happens to look like a capability and not get intercepted if system calls were implemented by just catching the existing invalid-syscall exceptions? Not if you don't have any capabilities mapped into the address space. Correct, which would be a reasonable design for a legacy subsystem, it forces each syscall to raise an exception. Silly me for not pointing this out in the first place. I think there are some syscalls that a linux application could issue that would not trigger a fault: * The yield syscall takes no arguments * It looks to me like the non-blocking send syscalls do not raise exceptions I can confirm that "yield" is the only syscall in seL4 that does not need a cap[*]. That is probably something that should be changed. Cheers, Gerwin [*]: You can double-check this fairly easily by following https://github.com/seL4/l4v/blob/master/spec/abstract/Syscall_A.thy#L326 one or two layers down