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
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
Gernot for the Trustworthy Systems team