Mixed-criticality support in seL4

The world contains an increasing number of "cyberphysical systems" implementing various types of safety-critical functionality. Fly-by-wire systems for aircraft and factory automation systems are a couple of examples. These systems are subject to an expensive safety-assurance process with costs that scale linearly (at least) with each line of code. When one considers that an Airbus A380 jetliner contains around 120 million lines of code, one can understand that developing that code can be a costly business.

The traditional approach to safety-critical code has been physical separation, using a different microcontroller for each function. That is how cars and aircraft have been built for some time. But those controllers are not cheap; a microcontroller fit for deployment in an automobile must be waterproof, resistant to dust, grease, acids, and vibration, and be able to operate in a wide range of temperatures. Such controllers are expensive, and there were typically about 100 of them in a car even five years ago. They are heavy, require a lot of cabling, and use a lot of energy.

The problem is compounded by the increasing need for sensors. Many sensors in a car support a number of different functions, meaning that they must be shared across processors.

The answer to this problem is consolidation: get a bigger processor and put a number of functions on it. That reduces costs while allowing better integration between functionalities; that integration is absolutely needed for autonomous vehicles. But this approach loses the physical isolation between functions, so that isolation must be restored in some other way that can still achieve certification.

Getting there, Heiser said, "involves killing a lot of trees". Specifications and development documents must be written. Effort must be put in to attach every requirement in the specifications to the lines of code that implement it. This work is expensive, to the point that, for the highest safety levels, the cost is prohibitive for anything more than a few thousand lines of code.

The answer is to use software isolation to separate the safety-critical code (which must be certified) from everything else. This an old concept, "in use since the stone age", but there is a problem: operating systems are hopeless at providing this kind of isolation. They do things like put device drivers into the kernel. Anything in the system can affect anything else. This kind of operating system cannot be used for systems of any complexity, he said.

Isolation starts by defining the "criticality" of every task that the system must perform. There are several levels, based on the consequences that result if the system fails to do its job properly; they go from "harmless" to "catastrophic". On any system running tasks with varying criticality, no task may depend on anything at a less critical level.

Solving the problem with seL4

The system that can support mixed-criticality workloads, Heiser said, is seL4. It completely isolates all running components by default, but makes it possible to create communication channels between components where they are needed. Its core mechanism is called "capabilities", but they differ from the capabilities found on a Linux system. A seL4 capability is an access token: it contains a reference to some object and a set of associated access rights. Processes must present the necessary capabilities with any operation, and the system will make a decision as to whether to allow that operation. It adds up to a fine-grained access-control mechanism.

There are eight different types of capability-protected objects in seL4:

• Thread-control blocks (processes)
• Address spaces
• Endpoints (ports for communications between processes)
• Notifications (a sort of completion mechanism)
• Capability spaces (to store capabilities themselves)
• Frames (areas of physical memory that can be mapped into address spaces)
• Interrupt objects
• Untyped (free) memory

All of these object types are "spatial", he said; the lack of any concept of time is a longstanding seL4 issue (which he was to return to shortly).

The seL4 microkernel has been subjected to a set of formal proofs of its security and safety properties. It is based on an abstract model written in a mathematical notation that is used to generate the C implementation. There is a machine-checked proof that the C implementation actually holds to the specification, and another proof that things are not broken in the compilation process. Yet another set of proofs show that the model implements the needed confidentiality, integrity, and availability properties. SeL4 is, he said, the only operating system in the world that has been verified in this way.

There has also been a worst-case execution time (WCET) analysis of all kernel operations that, he said, shows that seL4 is the world's fastest microkernel. Aspects that have not yet been verified are the initialization process, some memory-management unit operations, and multicore operation — but that work is in progress.

Toward a certifiable mixed-criticality scheduler

Once again, he noted that all of this verification only applies to spatial isolation, but the WCET work is a good start on the temporal problem. Beyond that, there is a new scheduling model in the works that will ensure that low-criticality code cannot interfere with higher-criticality code. The existing seL4 scheduler is relatively primitive, based on round-robin realtime scheduling that rotates through the runnable processes with the highest scheduler priority; it is good, but not sufficient. Among other problems, this scheduler will let the highest-priority process monopolize the CPU for as long as it chooses to. (Here, as usual, "priority" is a value used by the scheduler to pick the process to run first; it is not the same as the criticality assigned to any given functionality, though high-criticality tasks tend to be given high priorities).

As an example, consider a network driver. It will not be the most critical task on the system, but it may still need to occasionally preempt a high-criticality control loop to avoid losing packets. With the current scheduler, that driver must be given a high priority and trusted to not hog the CPU.

Another problem is data structures that are shared between criticalities. A common solution is to encapsulate that data in a separate server, running in its own address space. Other processes then communicate with the server to access the structure. Priority-inversion problems can result, though, when processes with different priorities access the server. Use of the priority-ceiling protocol can help, but requires getting the priorities set right. There are still problems where one client can starve another by repeatedly invoking the data-structure server, though.

Improving the situation naturally involves another set of requirements. A new scheduler must provide certifiable spatial and temporal isolation. It must be able to guarantee deadlines for high-criticality tasks while being able to share resources across criticalities. It should run low-criticality processes during otherwise slack periods. Capabilities should be used for time control.

Getting there, Heiser said, is not that hard with the right model. The classic time slice has been replaced by a "scheduler context". That, when combined with a capability, can be used to assign a given CPU budget and period to each process. Any process that exceeds its CPU budget during a given period can be throttled. Processes that have shorter periods are given a higher priority by the scheduler, but the budget limits the amount of CPU time that even the highest-priority process can consume.

The scheduler works by always running the highest-priority thread that has a non-zero budget. Any thread that has consumed its budget waits until the next period begins. If there are multiple processes with the same priority, round-robin scheduling is used.

In this model, the shared data-structure server mentioned above has no scheduler context of its own. Instead, it will use the context of the clients that invoke it. That causes this server to run at a priority appropriate for the client it is serving while charging that client for the CPU time used. It's a neat solution, but there is one little problem: what happens if the client's budget runs out while the server is running? These servers are usually single-threaded to keep them simple and certifiable, so simply throttling the server would deny service to other processes that may need it.

There are a few options for dealing with this situation. One would be to require that such servers be multithreaded; adding concurrency adds complexity, though, so this is not a great solution. Another would be to throttle the server until another client comes along, then borrow that client's time to finish the first client's work. In this case, the wrong process is paying for the mistake, which is not a good thing. The solution chosen for seL4, instead, is to provide a mechanism called "timeout exceptions". They can respond in a number of ways, including resetting the server, providing an emergency CPU-time budget, or implementing priority inheritance "if they really need to".

This new scheduler solves the problem, but it does not come for free: interrupt latency increases by 11% and scheduling itself is 19% more expensive. In both cases, the need to reprogram hardware timers is the source of most of the slowdown. But, he noted, scheduling in seL4 is "still an order of magnitude faster than Linux".

He wound down by noting that this work is being used in some real systems now. There are a couple of autonomous trucks under development for the US Army that are using it, and Boeing is working on a full-size autonomous helicopter. Certainly, as that helicopter flies overhead, one would hope that seL4 is indeed living up to its guarantees.

The video of this talk is available on YouTube.

[Your editor thanks the Linux Foundation and linux.conf.au for assisting with his travel to the event.]