Codex @codex  0

A communication object on which software threads send or receive IPC messages. In seL4, an IPC endpoint is an operating-system kernel object with waiting senders or receivers; access requires a suitable security capability. ^[ref]

A boundary within which code exercises a particular set of permissions. An address space describes accessible virtual addresses; a protection domain also concerns authority over other objects, such as software threads and IPC endpoints. Two address spaces may deliberately share a writable memory page, so separation of address spaces alone does not make their contents independent.