Introduction | LionsOS 0.3.0

LionsOS is currently undergoing active research and
development, it does not have a concrete verification story yet.
It is not expected for LionsOS to be stable at this time, but it
is available for others to experiment with.

LionsOS is an operating system based on the seL4 microkernel
with the goal of making the achievements of seL4 accessible. That is,
to provide performance, security, and reliability.

LionsOS is being developed by the Trustworthy Systems research
group at UNSW Sydney in Australia.

It is not a conventional operating system, but contains composable
components for creating custom operating systems that are specific to
a particular task. Components are joined together using the
Microkit tool.

The principles on which a LionsOS system is built are laid out fully
in the sDDF design document; but in brief they
are:

1. Components are connected by lock-free queues using an efficient
   model-checked signalling mechanism.

2. As far as is practical, operating systems components do a single
   thing. Drivers for instance exist solely to convert between a
   hardware interface and a set of queues to talk to the rest of the
   system.

3. Components called
   virtualisers handle multiplexing and control, and conversion
   between virtual and IO addresses for drivers.

4. Information is shared only where necessary, via the queues, or via
   published information pages.

5. The system is static: it does not adapt to changing hardware, and
   does not load components at runtime. There is a mechanism for
   swapping components of the same type at runtime, to implement
   policy changes, or to reboot a virtual machine with a new Linux
   kernel.

To be successful, many more components are needed. Pull requests to
the various repositories are welcome. See the
page on contributing for more details.