seL4

Contributing to the Project

General

We welcome contributions to the seL4 project. However, the copyright holders require us to have on file a signed Contributor Licence Agreement for all contributions.

The Licence agreement certifies:

Please sign the Contributor License Agreement, scan it and send it to us at licensing AT sel4.systems

The best way to contribute patches is through github pull requests. Alternatively you can send patches in plain text form with a changelog (use git format-patch) to the mailing list devel AT sel4.systems for review and comment. Please include an indication of which repository any patch is against.

Kernel

Diagram of development model The figure at the left indicates the kernel development model. There are two versions of the source tree: “experimental” and “master”. The name of the first is slightly misleading, as the code in there is quite mature. The difference is that the master version of the kernel is verified, while the experimental one isn't. The former therefore lags behind the latter in features and performance. (Actually not everything in master is verified, it also contains the unverified x86 port and some unverified platforms, but it is the code base that is verified for at least one particular ARM platform.)

Because of this, prerequisite for committing any change to experimental is an understanding that the code is feasible to verify, and a committment by our verification team to eventually do the verification. Note that “eventually” might be quite a while — it is strictly unbounded, as we may depend on external funding to do the work. So, you cannot rely on this verification to happen within weeks, months or even years, but if you can contribute money, then you can negotiate an actual timeline with us.

Implied in that model is that we will continue to act as gatekeepers for pushing patches into the public source in order to maintain the above invariants. Note that this applies to patches by CSIRO people as much as patches from externals.

User-level code

The story is different for most user-level code. While we are working on verifying some of this, and are likely to adopt a similar model as for the kernel for such components, most user-level code is not likely to be verified in the foreseeable future. Many of the user-level components are suitable for a truly open development model, and we will be happy to hand control to a suitable external maintainer for many of those. Our priority is on building an ecosystem and easing deployment of and with the system.

See Suggested Projects for suggestions on where to contribute.