seL4

Development and Verification Roadmap

Below tables list our target dates for various parts of seL4 and Data61-supported parts of its ecosystem.

Where status is deferred, this relates to previously published version of this roadmap; in such a case, the date given here is our present (as of June 2017) estimate when we will deliver the feature.

Where we indicate that the feature will appear in master, it might possibly appear in a branch earlier. Features in branches will be merged into mainline at a later time, timing of this is determined by the verification schedule. The reason is our commitment to ensuring that at any time, mainline code for our verified platforms is actually verified. This means that a feature can only be pushed into mainline if it doesn't break the verified platform proofs. In some cases this is no problem, e.g. as long as we haven't completed verification of x86, then changes that only affect x86 can go into mainline (as long as the verifiers agree that they will not inhibit future verification). This is the main reason why the real-time scheduling features will remain in a branch for some time – they are relatively invasive and break many existing proofs.

Some features are in branches because they are of an experimental nature, and are released to the community to allow people to experiment with them, we will do the same. This means that such experimental branches may undergo significant changes on their way into mainline, if they ever make it there.

All dates are indicative and subject to change!

In many cases, we could possibly deliver earlier if we had enough people to do the work. If our recruiting is more successful than expected, we might be able to go faster. If you want to help accelerate this roadmap, help us to find the right developers!

Development Roadmap

Microkernel

Status       Date      Feature    Location
delivered in  Q2’16 ARMv8 support (32-bit only) master
delivered in Q2'16 ARM virtualisation support complete master
delivered in Q2’16 New scheduling model (supporting mixed-criticality real-time scheduling)   
Note: API changes!
branch
delivered in Q3'16 64-bit support for x86 (x64 support) master
delivered in Q4'16 full virtualisation support for x86 (32-bit) master
delivered in Q4’16 Multicore support for x86 master
delivered in Q4’16 Multicore support for x64 master
delivered in Q2’17 Multicore support for ARM master
deferred to Q4’17 Support for strict temporal partitioning (timing-channel protection)
Note: API changes!
branch
deferred to Q3’17 64-bit support for ARM (full ARM v8) master
deferred to Q3’17 Multicore for 64-bit ARM and x64 master

Low-level Userland

Status Date      Feature Location
deferred to    Q3’17 SMP-capable virtual-machine monitor (VMM)    master

CAmkES

Status Date      Feature Location
delivered in    Q3’16 CAmkES support for seL4 real-time scheduling model    master

Verification Roadmap

Microkernel

Status Date      Feature Location
delivered in Apr’17 ARM virtualisation support      
(excluding system MMU)
master
deferred to Q3’17 x64 support
(excluding virtualisation support)   
master
on schedule    Q2’18 New scheduling model master
TBD Multicore master

Low-level Userland

Status    Date      Feature Location
on schedule    Q4'16 libsel4       master

CAmkES

Status Date      Feature Location
delivered on    Q2’16 Generation of RPC glue-code and capDL proofs    master