We have created the seL4 Foundation!
But what is the seL4 Foundation, and why did we create it?
In a nutshell, these are the reasons (I’ll expand on them below):
- Provide for the longevity of seL4 beyond support from any specific organization
- grow and integrate the seL4 ecosystem
- protect and promote the seL4 brand
- provide a platform for funding on-going engineering as well as sharing the cost of big-ticket verification items.
Ensure longevity of seL4
seL4 is a game-changer for safety- or security-critical systems. Being an OS microkernel, seL4 is at the bottom of any software stack. To use it properly and to achieve the strong security properties enabled by seL4, the system must be engineered for seL4. This may require a long-term commitment, requiring significant resources. You therefore want to make sure seL4 stays around, is well-supported, and continues to provide those guarantees.
The viability of seL4 is strongly tied to its developers, the Trustworthy Systems (TS) team, and especially the technical leadership of TS. This in itself is not a problem, because everyone knows how committed we are to the success of seL4. And because there are four technical leaders for the kernel (Kevin, Gerwin, June and myself), we have a degree of redundancy (although we do work best as a team!)
We believe that as an independent, nonprofit organization, the seL4 Foundation can make the seL4 story even stronger, and an even better choice for developers who build trustworthy systems. This is especially true if you consider a time-scale of decades, which is necessary for many of the early adopters of seL4 in the infrastructure, medical, and defense domains. By setting up an organizational framework that is supported by (and accountable to) adopters (subject to providing financial support, of course) we can plan for the future. Our Board of Directors will represent the voices of significant adopters, which will help keep the technical leadership aware and responsive to the needs of adopters.
Grow and integrate the seL4 ecosystem
Right now, the biggest barrier to uptake of seL4 is probably the lack of system components and tools. This includes board-support packages (BSPs), device drivers, file systems, networks stacks, high-level programming environments (something at the abstraction level of POSIX, but preferably based on a more suitable model), and configuration and development tools. Plus debuggers, IDEs etc.
Without some supporting organization, many of those missing bits will have to be (re) built by every adopter. This would a huge waste of effort better spent developing new trustworthy systems. Furthermore, I believe that there are plenty of people out there who would be happy to contribute if there were more guidance, active community engagement, and a clear shared direction forward, so that the contributor can be confident their input will make a difference for the long term.
We think that the way to address this is having a forum where the community, including developers, adopters, and researchers can meet and engage. The seL4 Foundation as an open and neutral entity , where the broader community is represented, and strategy is discussed openly, seems the right way to do this.
Protect and promote the seL4 brand
seL4 has become a recognized brand that is strongly associated with its unique properties – the world’s fastest and most advanced microkernel, with a powerful assurance story. Even ten years after we connected the original proofs, There is still no other general-purpose, non-toy OS kernel with a proof of implementation correctness . And on top of all this, seL4 is open source.
These properties drive the adoption of seL4, providing a competitive advantage to the developers of seL4-based products. But, of course, this creates expectations: a system based on “verified seL4” is expected to be more trustworthy than others. This trust could be undermined by adopters who modify the kernel. Let me explain why.
Mathematical proof provides the strongest assurance possible. But the guarantees it provides need to be thoroughly understood, in order to avoid being misleading the people who rely on them. Even mathematical proof can never cover everything: It always relies on a specific scope (eg. The assumption that the hardware behaves correctly). If these conditions are misunderstood, you might overestimate the guarantees that you get. In particular, the proofs are for very specific versions of the kernel and against a very specific specification. A seemingly trivial code change may invalidate the assumptions and thus void any assurance.
Adopters need clarity on this. Also, a company That sees a competitive advantage in having a verified system does not want this advantage undermined by others taking shortcuts and making unsubstantiated verification claims.
The Foundation will help by officially “blessing” the status of verified versions and precisely identifying the conditions under which they hold. This should help provide clear provenance, so seL4 adopters will be able to assign liability resulting from someone hacking an unverified version to where it belongs: to those providing such unblessed code.
In addition, it should be more visible what changes will affect proofs. That can informally happen with documentation, but a better solution will be a framework where adopters can run the proofs themselves, on the code base they are deploying, to confirm that the proofs still hold. Such a framework will, of course, also help contributors to identify whether adopting their changes will be straightforward (if they do not invalidate the proofs).
All this must go hand-in-hand with the promotion of seL4 and its benefits. The best way to achieve this is through a broad membership base. If you’re reading this, you clearly have some interest in seL4 – please join!
Fund on-going engineering and big-ticket items
seL4 is the result of big investments. Firstly by the Australian tax payers, who (through NICTA) funded its creation, and (through NICTA and then CSIRO’s Data 90) continued supporting it. Over the past 6 years, US taxpayers (mostly through DARPA, but also other parts of the DoD as well as DHS) invested a lot in completing and extending the verification story, as well as deploying on real-world systems. And most recently, HENSOLDT Cyber funded verification of the RISC-V port of the kernel. [Disclosure: I have an interest in HENSOLDT Cyber.]
These are awesome expressions of confidence in seL4 and the team behind it, and we are immensely grateful for this support. Yet, we need more.
On the one hand we need a revenue stream to fund on-going support of the community, maintenance of existing versions, improvements of the infrastructure (in particular the automation of the seL4 verification framework). We need support for what we call strategic engineering – evolving the kernel and, importantly, developing the ecosystem. While we hope that much of the latter will eventually be done by the community, we will for now have to keep showing the way, by providing reference designs and sample components. This is obviously needed to make seL4 an attractive platform for commercial systems.
On the other hand, we have a number of big-ticket items that are crucial to our aim of making seL4 the Linux of the embedded world . The biggest of these are:
- Verification of the – bit Arm kernel
- Verification of the multicore kernel
There are plenty of companies keen to see both of these (and a few others) done, and several of them are willing to put money on the table to make it happen. However, the investment required for these two is above the pain limit of what most companies can justify for an open-source project, where they cannot walk away with a bunch of proprietary IP. But most can see the value of enabling it as an an open-source platform.
So this is the third major goal of the Foundation: Provide on-going base funding, and bring these interested parties together and divide the required investment in a way that keeps individual contributions below the pain limit.
Together we can do it – we can change the world of critical systems, to achieve real security!
Obviously, the core function of the Foundation is to address the above four points, which were the rationale for setting it up in the first place. But how will this work in practice?
Community engagement
This is really the central mission: Engage and grow the community of seL4 developers and adopters, and direct and standardise the evolution of seL4 and its ecosystem.
There are several aspects to this. On the one hand there is the seL4 kernel and its proofs, on the other hand there is all the stuff around it that is essential to using it. And everyone who has had a serious look at seL4 will appreciate that the kLOC kernel is just the foundation – you need so much more to build a system on it!
As mentioned above, this is really the biggest barrier to uptake at the moment. There is not a lot of seL4-based userland that is ready to use, and there is very limited support through tools and development environments. Reality is that anyone who wants to deploy seL4 in a real-world system ends up developing much of this themselves.
This is obviously a waste! It will be to everyone’s benefit if at least the core components and tools are shared. Things like device drivers, network stacks, or core system services contain no IP of value but bear a significant cost. We need to reduce the cost by sharing those artefacts. There are two aspects here: Those who are developing such artefacts should share them with the community, and members of the community should adopt and maintain them.
The (highly simplified) diagram above indicates this with the “Core userland” box – these are basic system services everyone needs. In fact, these typically corresponds to components which Linux would have deep inside the kernel We (TS) see it as our job to provide some of the core userland infrastructure, such as the CAmkES component framework, and maintain it at least initially. And we need to provide at least examples of others, such as well-integrated device drivers. However, we want the community to contribute to this, and hope that an increasing number of such parts will be adopted by maintainers from the developer community. The lower in the stack a component resides, and the more unique it is, the higher will be the bar for such adoption. This is because such core components must be designed right, meaning that maintaining them requires a very thorough understanding of how seL4 and seL4-based systems operate. Ideally, such core components should also be verified, but it will be a while until that becomes reality.
Things get easier with more high-level components, developer tools, libraries, or drivers for yet another NIC, once a performing example of a similar NIC driver exists. Some are still low-level enough for their Linux equivalents to live inside the Linux kernel (device drivers, crypto libraries) or are part of the “OS environment” (programming-language runtimes, shells, etc). But their dependence on the seL4 model is less, or there are good templates. Furthermore, there may be benefits from competing components with similar functionality (eg libraries optimized for small IoT systems vs desktops vs servers). Here we see our (TS’s) responsibility as mostly “showing the way” by providing sample code or designs and putting them out for community adoption.
The kernel itself will for the foreseeable future continue to depend strongly on our expertise. Besides ensuring purity of the design, this has a lot to do with verification: Very few people understand how a (seemingly innocent) change to the kernel will affect verification, and even our experts sometimes grossly underestimate the cost of changes. And, of course, when the kernel has changed, the proofs need to be updated, and that again is something a few people can do at the moment. We do hope to get to the point where more non-TS community members can contribute proofs, but for the time being are committed to remain central to the kernel’s evolution.
We certainly welcome platform ports, and we are working on ways to make verification of a platform port easier, maybe semi-automatic. But that is still research!
And we do commit to an open process for evolving the kernel! This will be part of the duty of the technical steering committee of the Foundation, with representation of developers, which will run an open process for kernel evolution.
Structure
The seL4 Foundation is set up as a Project under the Linux Foundation (LF) and follows the established structure of LF. This has the advantage that it is a familiar setup that is used by hundreds of open-source projects. It also means that we benefit from LF’s existing infrastructure (organizational and legal) as well as their existing networks for recruiting members. The structure is shown in the figure.
In Line with LF, we clearly separate the Foundation’s governance from technical leadership and contributions. The Foundation has a Board that is responsible for the governance. In particular, it controls the “directed fund”, which is where membership fees go (minus a tax to LF). The directed fund can also receive extra contributions from members, it will especially be used to pool funds for the “big ticket” items I discussed above.
The technical activities are underneath the legal body of the “LF Projects LLC”, LF’s nonprofit company. Under it, the “seL4 Series LLC” is a virtual company for the seL4 Foundation. It holds the rights to the seL4 trademark and the (seL4.systems)
Membership and Board
Similar to the LF itself, the seL4 Foundation has different classes of membership, that model the LF’s. Note that to become a member of the seL4 Foundation, an individual or organization must first be a member of good standing in LF (and pay their membership fees as well).
Fees for regular members are tiered by size, similar to LF, although our fees are lower than LF’s for small companies and somewhat higher for large ones. Premium members (who can be regular members of LF) pay extra in exchange for the privilege of having a guaranteed Board seat. Individuals and non-profit organizations (such as universities or other open-source foundations) can join for free as associate members . The Trustworthy Systems team, as the creators of seL4, have a special status as premium members without paying membership fees for five years.
(seL4 Foundation membership and Board.
The Board is composed of three members from TS, and one from each premium member. In addition, all regular members together elect a further Board Member. Finally there is the Technical Steering Committee, which is composed of committers and Technical Leaders (such as the non-commit leaders of TS) and is responsible for setting technical directions for the seL4 ecosystem. It has a chair, who is an ex-officio member of the Board.
The high representation of TS on the Board shows our commitment to making the Foundation work. We are not merely dumping this on the community and moving back to research. We are staying engaged, and have committed our resources for a minimum of 5 years. We chose this model in response to specific feedback from adopters.
Contributors, Committers and Technical Leaders
The C ontributors make up the seL4 community – people who contribute code, documentation, tools etc to the seL4 ecosystem . A selected subset of Contributors are designated as C ommitters , these are the ones who can directly commit to the repository and accept pull requests.
Initially, the Committers are TS members who commit to seL4 code, proofs, docs, or userland code. We anticipate (in fact sincerely hope!) That we will soon be able to appoint a significant number of Committers from the community for non-kernel components. These will be approved by the Technical Steering Committee (TSC), which is made up of Committers and Technical Leaders.
One particularity of seL4 is that it has Technical Leaders who don’t commit code, but provide leadership on design and implementation issues (this includes yours truly). This is a very small number of people, who have the same say as Committers, including being part of the TSC, except the right to commit code.
The TSC elects a Chair, who is an ex-officio member of the seL4 Board, to represent the technical community.
Not at all! We at TS will continue to do research that will feed into seL4, to ensure it remains the most advanced OS technology . In particular, our work on
time protection as a principled way to prevent information leakage through timing channel has still a fair bit to go until it is production-ready and can make it into the mainline kernel.
This is in addition to research on architecture of secure systems, and tools and languages that make it easier to build high-assurance (ideally verifiable) components on top of seL4. This cluster of research will be an enabler for achieving our vision of not only a verified kernel, but verified core system components. One aim for the next few years will be to be able to build at least some simple systems with a completely verified trusted computing base.
We see this research as a central part of our on-going contributions to the seL4 ecosystem. And we hope that the Foundation will also lead to more collaboration in seL4-related research.
The interim Foundation web site provides more details on how to join, including the full set of legal documents and a link to the LF interface for becoming a member.
But we need not only members, we also need active contributors, whether they are companies or individuals. If you want to be one of them, look at the Contribute page for projects looking for help, which can range from ports via enhancements to people becoming committers.
And if you want to deploy seL4 to secure your product, check out retrofitting and transitioning to seL4 for ways of doing this and the list of available userlevel infrastructure . And contact us (if you are looking for commercial support for seL4, we can link you up with one of the growing number of companies providing this.
GIPHY App Key not set. Please check settings