L4HQ - The L4 Kernel Family;
L4HQ - Manuals;
One L4 worker’s 2007 bookshelf,
Development and Verification Roadmap,
seL4: Formal Verification of an OS Kernel,
seL4 specification and proofs
Optimizing IPC in L3
but callee ID is an unprotected name in L3.
ID of caller is reliably delivered to callee who is supposed to decide on legitimacy of request from the ID of the caller.
L3 is not caps.