L4 Literature

  • Wikipedia:

    Fiasco.OC L4HQ - The L4 Kernel Family; L4HQ - Manuals; Rev 6.
    One L4 worker’s 2007 bookshelf,


    My notes
    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.