LionOS is currently undergoing active research and development, with no solid validation story yet. LionOS is not expected to be stable at this time, but is available for others to use.
LionOS is an operating system based on the seL4 microkernel that aims to make the achievements of seL4 accessible. That is, providing performance, security and reliability.
LionOS is being developed by the Trusted Systems Research Group at UNSW Sydney in Australia.
It is not a traditional operating system, but includes composable components to create custom operating systems that are specific to a particular task. The components are assembled together using Microkit tools.
The principles on which the LionOS system is built are fully set out in the SDDF design document; But in short they are:
-
Components are connected to lock-free queues using an efficient model-checking signaling mechanism.
-
As far as practical, operating system components perform the same function. For example, drivers exist only to talk to the rest of the system between a hardware interface and a set of queues.
-
components called
virtualizer Handle multiplexing and control, and conversion between virtual and IO addresses for drivers. -
Information is shared only where necessary, through queues, or through published information pages.
-
The system is stable: it does not adapt to changing hardware, and does not load components at runtime. There is a mechanism for swapping components same type At runtime, to apply policy changes, or to reboot the virtual machine with a new Linux kernel.
Many other components are required to be successful. Pull requests to different repositories are welcome. See the Contributing page for more details.