Language Support

Language Support #

If you browse the LionsOS code and the various sub-projects that it uses such as libvmm and sDDF, you will notice that everything is written in the C programming language.

One of the benefits of having isolated components is that, as long as the standard interfaces across components are held, any number of programming languages can be used within a single system.

For example, if you had a client that used the network sub-system, perhaps the client could be in Rust while the virtualiser components are in C and the driver is some third language. As long as the queue structures follow the same memory layout, everything will “just work”.

At the moment, we do not have any examples of this kind of setup. The Kitty reference system is all written in C code (with some MicroPython scripts).

C #

C will most likely remain as the the most common language of LionsOS components due to it being amenable to formal verification and because our current verification tooling is intended for C.

Standard Library (libc) #

One of the considerations we need to make when using C is what standard library we want to use. Unfortunately there is no standard C library that works across all operating systems unlike other languages.

We do not necessarily want to use the full extent of a libc (in particular slow POSIX APIs such as read and write) but understand that large or legacy clients cannot reasonably change to use the asynchronous APIs that we mostly use.

Currently, we provide a libc for LionsOS systems based on a fork of musllibc. For more information, please see the page on libc usage guidance.

MicroPython #

For ease of experimentation and certain client components, we make use of the MicroPython interpreter to allow Python scripts to run on LionsOS. MicroPython is a slimmed down version of Python, intended for embedded use cases.

Our current support for MicroPython allows serial, networking, I2C, and file system access. MicroPython can be used either as a REPL or as an interpeter for a specific script upon boot.

It should be noted that not all Python programs will work with MicroPython out of the box and there may be some porting necessary, see their website for details on compatibilty.

Pancake #

Pancake is a new programming language, developed at Trustworthy Systems in co-ordination with other researchers, with the goal of creating verified device drivers. It is a low-level systems langauge, with a similar syntax to C.

Pancake is not yet mature but is receiving internal use for writing and formally verifying drivers.

You can find out more about the Pancake project here.

Rust #

Rust is becoming popular within the embedded space and now with first-class Rust support for seL4 it is fairly easy to write Rust programs for an seL4 environment.

At this stage, we have only used Rust to write certain device drivers but are interested in providing Rust bindings for LionsOS APIs in the future as well as providing a port of the Rust standard library.

WebAssembly (WASM) #

LionsOS includes experimental support for running WebAssembly applications. This is achieved by porting the wasm-micro-runtime to LionsOS, allowing WASM modules to execute inside a LionsOS component.

Currently, our focus is on applications targeting WASI, as WAMR provides a POSIX-based implementation of WASI APIs. This makes WASM a useful driver for building out LionsOS’s libc and POSIX functionality. A test system demonstrates file system access (via FAT) and TCP networking (IPv4) from a WASM application running under WAMR.

WASM modules should be compiled using the WASI SDK. The following WASI capabilities are currently supported:

  • Filesystem: File and directory operations via a filesystem conforming to the LionsOS FS protocol
  • Sockets: TCP client/server (IPv4 only, no UDP)
  • Time: Clock access and sleep functions
  • Memory: Anonymous memory allocation

Each WASM component in a LionsOS system links to its own copy of the runtime, leveraging seL4 to enforce isolation between the different native or WASM applications.

At present:

  • Execution is limited to interpreter mode, but support for JIT and AOT compilation is planned.
  • Any WASM module can theoretically run, provided the required host functions are provided and imported.
  • Integration is highly experimental and primarily intended for research and development.

Looking ahead, we aim to:

  • Provide deeper LionsOS-native bindings for WASM components.
  • Explore asynchronous interfaces as WASI evolves, enabling more efficient interaction with LionsOS APIs.