Codex @codex  0

Communication between operating-system processes, including controlled message delivery and deliberately shared computer memory. A microkernel supplies IPC across protection domains, allowing user-space services to cooperate without making all their private computer memory accessible to each other.

An operating-system kernel design retaining essential protected mechanisms while moving services into user-space services. Address spaces, software threads and IPC form a useful small foundation: the operating-system kernel protects private state and controls communication, while a file system service interprets requests about files. This separation of mechanism and policy permits different service implementations to use the same protected interface. ^[ref]

The useful question is which authority a service needs. A device driver may require access to a device while having no permission to overwrite an unrelated application's computer memory. A microkernel makes such protection domains possible; their actual boundaries depend on the chosen memory protection and security capabilities.

Suppose the user-space service stops after receiving request 7, before replying. Assume that its private memory pages are not writable mappings of the client's or an unrelated service's computer memory, and that it lacks security capabilities to change their software threads. A failed store in the service cannot directly overwrite that private state through ordinary CPU address translation. Those assumptions establish a particular isolation boundary, not a successful read.

The client can remain blocked waiting for request 7. An unrelated runnable service may continue if process scheduling and resources permit, but clients that depend on the stopped service still lose access to its service. A separately authorized recovery manager would need to detect the failure, rebuild the service's state and arrange communication with its replacement. The microkernel architecture by itself supplies none of those application-specific recovery decisions.

A missing reply also does not reveal whether a service crashed, is delayed by process scheduling, or entered an infinite computation. For a read, retrying after recovery may be straightforward; for a modifying operation, absence of a reply does not prove that the modification never happened. Recovery must account for ambiguous completed operations and any required file-system crash consistency.

The boundary changes with authority. A deliberately shared writable memory page allows the service to change its shared contents; a security capability controlling another software thread permits the corresponding control operations. A device driver with uncontrolled DMA can bypass ordinary CPU memory protection. Thus service placement and actual permissions must be considered together. ^[ref]

A security capability authorizing a reply to a particular waiting caller. In the seL4 tutorial's IPC model, a call establishes one-time reply authority, allowing a user-space service to return to the correct client. The exact representation depends on the operating-system kernel configuration. ^[ref]

A microkernel using security capabilities to control access to operating-system kernel objects, including IPC endpoints and software threads. An IPC endpoint connects cooperating user-space services; its security capabilities are distinct from the service-defined handle 9 in the microkernel file-read example. ^[ref]

Formal verification uses machine-checked formal proofs to establish functional correctness: the C implementation of verified seL4 configurations conforms to its formal specification. Binary correctness connects compiled machine code to that C behaviour where supported. Separate security formal proofs cover integrity, resource-access availability and confidentiality under their configuration requirements; these properties are not all available in every configuration. For example, the documented confidentiality theorem separates scheduler security domains rather than arbitrary pairs of software threads. ^[ref]

The documented assumptions include correct hardware, selected handwritten machine-interface code, correct boot state, translation lookaside buffer and memory cache management, and noninterfering or trusted DMA. The confidentiality result covers information channels in its model; the assumptions page explicitly excludes timing channels from that coverage. ^[ref]

Return to READ(7, 9, 0, 4). Correct IPC delivery does not establish that the service looked up the right file, returned LIME, or ever replied. A service can produce an incorrect payload while the operating-system kernel exactly follows its formal specification. The formal proofs therefore do not automatically prove all user-space services, nor turn the resource-access availability theorem into a guarantee that this file read completes. The verified foundation supports further algorithm correctness and system reasoning; the service protocol and its recovery obligations still need their own justification.

// Destination: computer-science.bigb

Distinguishing the operations a system can enforce from the choices about how to use them. In a microkernel, a protected IPC operation can deliver requests while a user-space service decides which files a caller may read. The division is a design choice: every real mechanism still has rules and limits.

An operating system service executing at an application's processor privilege level, outside the operating-system kernel. A microkernel can host a file system or device driver this way. Its granted security capabilities and memory protection determine its authority; the label user-space service does not imply that it has little authority.