-
Notifications
You must be signed in to change notification settings - Fork 4
Home
Vesper is a capability-based exokernel.
It tries to remain small and secure. To achieve this, kernel functionality is extremely limited - it provides only address space isolation and IPC via capabilities, after bootup kernel does not allocate any memory itself.
The kernel only provides the IPC calls necessary for safe transfer of control between protection domains.
Exokernel's distinctive trait is that it provides mechanisms but not policies. Vesper tries to move as many policy decisions as possible to the library OS.
-
IPC is a mechanism providing secure interaction between processes.
-
Capabilities are a mechanism providing access rights control and universal authority delegation for OS objects.
-
Interrupts come from hardware, usually in privileged mode and kernel is responsible for translating them into invocations of the device drivers' handlers.
-
Single-address-space is a mechanism for providing pointer transparency between processes. Sharing a buffer is nearly as simple as passing out its address. However, single-address-space could be implemented by mapping frames to same virtual addresses in different processes. Therefore, the SAS property is a policy, not mechanism and could be moved to library OS. Vesper therefore does not dictate specific address space arrangements.
The rest of the OS functionality is based on capabilities implemented by various servers in the library OS. Capabilities could be selectively interposed on to allow servers to implement custom memory allocation, scheduling and security policies.
Default "kserver" server provides basic root services for applications, including the dynamic loader/linker. (@sa OMOS).
A minimal virtual memory management primitive supported by kernel too (Untyped.Retype
).