A new peer-reviewed paper is now available that describes the motivation, design, implementation and evaluation of our support for temporal integrity enforcement, as required for mixed-criticality systems (MCS).
We believe this makes seL4 the first real-world OS with temporal integrity enforcement that goes beyond the simplistic, and highly inefficient, strict time-and-space partitioning (TSP) approach. Furthermore, CPU access is now controlled by capabilities, just like access to spatial resources, resulting in a consistent approach to resource control that we believe is also unique, and will support formal reasoning about temporal system properties.
The new model is still in a branch, separate to mainline, until verification is complete, at which time it will supersede the present mainline version. Verification is in progress and should be completed sometime next year (but no guarantees yet). Compared to the earlier announcement (http://sel4.systems/pipermail/announce/2017/000017.html), the model has matured and is now fairly stable, we anticipate no major changes.
The paper will appear at next month’s EuroSys conference and is available from https://ts.data61.csiro.au/publications/csiroabstracts/Lyons_MAH_18.abstract...
Gernot for the Trustworthy Systems team