Repository navigation
Expand file tree
/
Copy pathroadmap.html
More file actions
144 lines (125 loc) · 5.4 KB
/
Copy pathroadmap.html
File metadata and controls
144 lines (125 loc) · 5.4 KB
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
---
# Copyright 2020 seL4 Project a Series of LF Projects, LLC.
# SPDX-License-Identifier: CC-BY-SA-4.0
title: Development Roadmap
sub: '
<p class="mb-4 sm:mb-8">
seL4's leading position keeps solidifying through an active, public
development community roadmap, both on the <a href="#systems">Systems</a>
side and the <a href="#verification">Verification</a> side. You
can <a href="#help">help accelerate or contribute</a> to this roadmap.
</p>'
img: '/images/roadmap.jpg'
img_class: "w-4/5"
alt: "Roadmap markers on an abstract path with a blue background"
layout: card
---
{% include section-start.html
heading='Systems Roadmap'
id='systems'
margins='pt-12 sm:pt-20'
intro='
<p class="mb-4 sm:mb-8">
On the Systems side, the roadmap includes further development for the kernel
itself, as well as updates to the expanding ecosystem
of <a href="tools.html">frameworks, tools, components, and
languages</a>.
</p>
'
%}
<div class="leading-7 sm:leading-8 text-base sm:text-lg mx-2 sm:mx-6">
<ul>
{% include green-roadmap-li.html
title='<a href="https://docs.sel4.systems/projects/microkit">seL4 Microkit</a>'
description='A simple operating systems framework for building systems on seL4.'
who='<a href="https://trustworthy.systems">UNSW</a>'
status='Ongoing research & development. Available for use. Detailed
roadmap
available <a href="https://docs.sel4.systems/projects/microkit/roadmap.html">here</a>.'
%}
{% include green-roadmap-li.html
title='<a href="https://trustworthy.systems/projects/drivers">seL4 Device
Driver Framework (sDDF)</a>'
description='A high-performance and secure driver framework for seL4.'
who='<a href="https://trustworthy.systems">UNSW</a>'
status='Ongoing research & development. Available for use. Find out
more <a href="https://github.com/au-ts/sddf">here</a>.'
%}
{% include green-roadmap-li.html
title='<a href="https://trustworthy.systems/projects/LionsOS">LionsOS</a>'
description='A secure, fast, and adaptable OS based on the seL4 Microkit.'
who='<a href="https://trustworthy.systems">UNSW</a>'
status='Ongoing research & development. An initial release containing a
non-trivial example system has been made. Find out
more <a href="https://lionsos.org">here</a>.'
%}
</ul>
</div>
{% include section-end-without-up-arrow.html %}
{% include section-start.html
heading='Verification Roadmap'
id='verification'
intro='
<p class="mb-4 sm:mb-8">
On the Verification side, the roadmap includes further extensions of the
seL4's <a href="Verification/proofs.html">formal proofs</a>.
</p>
'
%}
<div class="leading-7 sm:leading-8 text-base sm:text-lg mx-2 sm:mx-6">
<ul>
{% include green-roadmap-li.html
title='Verification of MCS Kernel extensions'
description='Functional correctness proofs for a new scheduling model to
support trustworthy mixed-criticality real-time systems.'
who='<a href="https://proofcraft.systems">Proofcraft</a>'
status='C verification completed for RISC-V, to complete for AArch64 Q3/27'
%}
{% include green-roadmap-li.html
title='Automated Platform Port Verification'
description='Reducing the need for verification experts for new platform
ports and expanding the set of supported configuration
parameters. Making the seL4 proofs applicable to a broader
range of platforms and applications without the need for
verification experts.'
who='<a href="https://proofcraft.systems">Proofcraft</a>'
status='Verification support for all Arm and RISC-V platforms platforms
now available. Further platform and configuration support ongoing.
Project to complete Q3/27'
%}
{% include green-roadmap-li.html
title='Multikernel Verification'
description='Specifications, verification tools, and proofs for
the multi-kernel configuration of seL4. Providing
gradually increasing assurance for multi-core seL4
systems as the verification progresses.'
who='<a href="https://proofcraft.systems">Proofcraft</a>'
status='Project scheduled to complete Q3/28'
%}
</ul>
</div>
{% include section-end.html %}
{% include section-start.html
heading='How to Accelerate or Contribute'
id='help'
%}
<ul class="mt-10 space-y-8 text-light text-base sm:text-lg">
{% include green-tick-li.html
text='In some cases, the roadmap could be accelerated with more funding for the
contributors who work on them, or by volunteering time. If
you are interested, email us at
<a title="foundation@sel4.systems"
href="mailto:foundation@sel4.systems">foundation@sel4.systems</a>.'
%}
{% include green-tick-li.html
text='
If you are working on a larger feature or addition to the seL4
ecosystem, possibly contracted to deliver it, and ideally with an
approved RFC to go with it, your contribution would be an ideal addition
to the roadmap. If you would like to add to the roadmap,
email us at
<a title="foundation@sel4.systems"
href="mailto:foundation@sel4.systems">foundation@sel4.systems</a>.'
%}
</ul>
{% include section-end.html %}