Processes

Documentation relating to development processes and how to get help or get involved in seL4 can be found on this page. Note that these are generalisations and may be different for a particular project/repository.

The processes described here are managed by the seL4 Foundation.

Development processes

Developing trustworthy systems requires identifying critical, trusted, system components and ensuring that they:

• are isolated from non-critical, untrusted, components
• have assurance of their trustworthiness

Determining appropriate system designs that clearly separate trusted from untrusted components and using this separation to achieve security and safety properties is beyond the scope of this section. However, given such a design, the seL4 ecosystem tries to provide components, infrastructure, and tools to implement it in a trustworthy way.

What we work on

As a microkernel, seL4 intends to provide the smallest amount of mechanisms required to enable securely multiplexing hardware. A full system requires many more components than only the microkernel. We typically try and reuse existing components when possible, but below is a list of projects that are currently maintained to support the seL4 ecosystem:

• seL4: The seL4 microkernel.

• seL4 verification: formal specifications and proofs for the seL4 microkernel.

• Build system and tooling: Tooling, system configuration and building used to build seL4 projects using mostly CMake.

• Elfloader: For preparing the hardware for seL4 on ARM and RISC-V.

• seL4 Run-time: A minimal runtime for running a C or C-compatible process in a minimal seL4 environment.

• User environment libraries: Userlevel libraries on seL4.

• seL4 testing framework: Test suite for seL4.

• seL4 benchmarking framework: sel4bench contains benchmarking applications and a support library for seL4.

• CAmkES framework: Component Architecture for microkernel-based Embedded Systems.

• CapDL: Collection of tools for generating, parsing and loading capdl specifications of systems.

• Virtualization with camkes-vm: x86 and Arm Virtual Machines built as a CAmkES component.

• sel4-tutorials: Collection of tutorials for learning to use seL4 and its ecosystem.

• Dockerfiles: Dockerfiles defining the dependencies required to build seL4, CAmkES, and L4v.

• seL4 webserver reference application: A reference for implementing applications on seL4.

• Hardware components: Various bits and pieces to enable easier use of our hardware.

Supported platforms

This all needs to be deployed on hardware components. The Supported Platforms page has a list of currently supported platforms.

How we choose what we work on

Primarily, what we work on gets prioritised by externally funded projects and what is long-term strategic. The strategic roadmap can be found on the seL4 development and verification roadmap page.

Some priority is also given to the maintained projects and repositories which involves responding to breakages and reported issues as they arise. Raising a GitHub issue on a relevant repository is the best way to get an issue acknowledged. Alternatively, the devel mailing list or the seL4 Mattermost can be used to ask about potential issues.

Additionally, the RFC process is intended as a way to provide input on longer-term priorities as well as a way to promote a collaborative design process on new kernel features before larger effort is invested into their development. More information is provided on the RFC page above.

Where we work on things

The code documented on this site is available from two GitHub organisations:

• https://github.com/sel4/: the seL4 kernel itself and the core repositories around it, managed by the seL4 Foundation.

• https://github.com/sel4proj/: additional tools, libraries, and projects around seL4, managed by the by the Trustworthy Systems group at UNSW.

Each project has a list of which repositories it contributes to on its documentation home page. Alternatively, the README.md of each repository should indicate what its purpose is.

Communication about what is being developed can occur on any of the channels listed below. In particular:

• The devel mailing list, seL4 Mattermost and seL4 Discourse are for general development discussions.
• Discussions about proposed changes can reach a point where an RFC is created. Further discussion then happens on the RFC pull requests in the RFC repository.
• GitHub issue and Pull-request comment sections can also be used.

The seL4 development and verification roadmap page lists major features and projects that someone has committed to deliver.

Contact

We use the following communication mechanisms:

• Mailing lists: For email-based discussions, for asking for help, reporting issues or general seL4 communication.
• seL4 Discourse forum: Forum for seL4. Attempting to build up useful knowledge-base.
• seL4 Mattermost. seL4 chat platform (Sign-up link can be found on seL4 Discourse with a valid account).
• GitHub issues: Reporting issues or creating pull requests on repositories located in the seL4 GitHub org.
• RFCs: for reading and creating new seL4 features or larger ecosystem changes.
• Websites: Websites containing information about seL4.
• seL4 Jira: archive for old issue tracking on seL4, CAmkES, and formal verification before GitHub development.

Contributing

We welcome your contributions to code, documentation and this website. To ensure a collaborative environment, we expect all contributions and interactions to fall within our Code of Conduct.

In addition to following the development process that is outset below, most of the software projects generally follow the following conventions:

• Style Guide
• Git Conventions
• Pull requests

Additionally, each project may have a slightly augmented processes for contributing:

• docs.sel4.systems
• seL4 Proofs