seL4 Microkernel Status Update
This is a modal window.
The media could not be loaded, either because the server or network failed or because the format is not supported.
Formal Metadata
| Title |
| |
| Title of Series | ||
| Number of Parts | 490 | |
| Author | ||
| License | CC Attribution 2.0 Belgium: You are free to use, adapt and copy, distribute and transmit the work or content in adapted or unchanged form for any legal purpose as long as the work is attributed to the author in the manner specified by the author or licensor. | |
| Identifiers | 10.5446/47396 (DOI) | |
| Publisher | ||
| Release Date | ||
| Language |
Content Metadata
| Subject Area | ||
| Genre | ||
| Abstract |
|
FOSDEM 2020208 / 490
4
7
9
10
14
15
16
25
26
29
31
33
34
35
37
40
41
42
43
45
46
47
50
51
52
53
54
58
60
64
65
66
67
70
71
72
74
75
76
77
78
82
83
84
86
89
90
93
94
95
96
98
100
101
105
106
109
110
116
118
123
124
130
135
137
141
142
144
146
151
154
157
159
164
166
167
169
172
174
178
182
184
185
186
187
189
190
191
192
193
194
195
200
202
203
204
205
206
207
208
211
212
214
218
222
225
228
230
232
233
235
236
240
242
244
249
250
251
253
254
258
261
262
266
267
268
271
273
274
275
278
280
281
282
283
284
285
286
288
289
290
291
293
295
296
297
298
301
302
303
305
306
307
310
311
315
317
318
319
328
333
350
353
354
356
359
360
361
370
372
373
374
375
379
380
381
383
385
386
387
388
391
393
394
395
397
398
399
401
409
410
411
414
420
421
422
423
424
425
427
429
430
434
438
439
444
449
450
454
457
458
459
460
461
464
465
466
468
469
470
471
472
480
484
486
487
489
490
00:00
MikrokernelPhysical systemExterior algebraFigurate numberOperator (mathematics)Speech synthesisBitDisk read-and-write headProjective planeMultiplication signComponent-based software engineeringMathematicsComputer animation
00:51
Kernel (computing)Physical systemInformation securityAsynchronous Transfer ModeMathematical analysisMikrokernelFormal verificationRun time (program lifecycle phase)Slide ruleOperating systemImplementationOpen setCodeMikrokernelComputing platformMathematicsReal-time operating systemCategory of beingFunctional (mathematics)Mixed realityAsynchronous Transfer ModeArithmetic meanCASE <Informatik>Information securityProof theoryPhysical systemLogicMathematical analysisOrder (biology)Open sourceSign (mathematics)Mathematical modelKernel (computing)Line (geometry)Forcing (mathematics)Computer animation
02:02
Kernel (computing)Kernel (computing)ChainPhysical systemProof theoryLogicMultiplication signMathematical analysisSemantics (computer science)Information securityBinary codeCodeRun time (program lifecycle phase)Operating systemCASE <Informatik>Model theoryLatent heatNeuroinformatikOrder (biology)Line (geometry)Functional (mathematics)Translation (relic)Proper mapHypothesisLimit (category theory)INTEGRALSpacetimeMoment (mathematics)Category of beingClassical physicsSpeech synthesisVirtual machineMenu (computing)Computer animation
03:49
Information securityARPANETPhysical systemProof theoryControl flowBit rateProjective planeReal numberSoftwareComputer hardwarePhysical systemMultiplication signAuthorizationCryptographyInformation securitySimilarity (geometry)Autonomic computingComputer animation
04:29
ARPANETInformation securityPhysical systemTime domainReduced instruction set computingMultiplication signPublic key certificateComputer hardwarePhysical systemAuthorizationSoftwareForestMoment (mathematics)NumberDifferent (Kate Ryan album)Open sourceMatching (graph theory)Enterprise architectureCybersexKernel (computing)QuicksortComputer animation
05:24
Core dumpAriana TVCybersexReduced instruction set computingCoprocessorChainLogicEncryptionControl flowPhysical systemKernel (computing)Trojanisches Pferd <Informatik>Computer hardwareReal numberBuildingProduct (business)Operating systemLogic gateFormal verificationCoprocessorSoftwareInformation securityMereologyEnterprise architectureSpacetimeOrder (biology)Open sourceProcess (computing)EncryptionChainQuicksortCore dumpPoint (geometry)Data storage deviceDependent and independent variablesComputer animation
07:07
SpacetimeAddress spaceAsynchronous Transfer ModeRoundness (object)Figurate numberArmOperator (mathematics)BitCycle (graph theory)Standard deviationService (economics)MikrokernelOrder (biology)Physical systemOcean currentForm (programming)Extreme programmingComputer hardwareQuicksortInformation securityLengthComputer animation
08:09
Address spaceExtension (kinesiology)TrailAddress spaceNormal (geometry)ArmDomain nameComputer hardwareMoment (mathematics)Figurate numberSpacetimeBranch (computer science)NumberImplementationRevision controlAsynchronous Transfer ModeACIDLine (geometry)State of matterQuicksortCoprocessorModel theoryMultiplication signProcess (computing)Context awarenessPoint (geometry)Drop (liquid)Computer animation
10:28
Formal verificationReduced instruction set computingData integrityPlanningQuicksortFormal verificationValidity (statistics)Translation (relic)Chemical equationCASE <Informatik>Table (information)1 (number)Different (Kate Ryan album)Multiplication signProof theoryChainBitBinary codeVideo gameEvent horizonFunctional (mathematics)GodMoment (mathematics)Run time (program lifecycle phase)Kernel (computing)Arithmetic progressionImplementationArmComputer animation
12:25
Reduced instruction set computingEnterprise architectureFormal verificationWeb pageTable (information)Asynchronous Transfer ModeExtension (kinesiology)Virtual machineGame controllerAsynchronous Transfer ModeVirtual machineFormal verificationState of matterEnterprise architectureOrder (biology)MereologyView (database)Point (geometry)Moment (mathematics)CodeRevision controlHoaxReferenzmodellStorage area networkSeitentabelleModel theoryWordBitExtension (kinesiology)CASE <Informatik>Computer hardwareVideo gameImplementationInformation modelLie groupRing (mathematics)IntelLevel (video gaming)Default (computer science)Exception handlingSemantics (computer science)Instance (computer science)System callProcess (computing)OrthogonalityOrder of magnitudeSoftware developerCore dumpSoftwareEmulatorNumberGoodness of fitDevice driverInformation securityLatent heatKernel (computing)Set (mathematics)Formal languageAdditionStudent's t-testComputer animation
18:17
Loop (music)Device driverMixed realityInterrupt <Informatik>Scheduling (computing)BitFormal verificationPhysical systemControl systemModel theoryComputer hardwareProcess (computing)FrequencyDevice driverGame controllerOperator (mathematics)Multiplication signDependent and independent variablesServer (computing)Order (biology)Bit ratePerturbation theoryGroup actionDisk read-and-write head2 (number)Contrast (vision)Mortality rateSpacetimeReal-time operating systemInternational Date LineSoftwareTotal S.A.Computer animation
20:06
Game controllerDevice driverSoftwareAtomic numberCASE <Informatik>Revision controlComputer animation
20:59
Server (computing)Server (computing)Operator (mathematics)Multiplication signQuicksortCommunications protocolService (economics)Shape (magazine)Real-time operating systemNormal (geometry)Computer animation
22:07
Attribute grammarThread (computing)Scheduling (computing)Computer multitaskingContext awarenessBefehlsprozessorInternet forumFrequencyModel theoryThread (computing)Context awarenessMultiplication signProgram slicingScheduling (computing)Shooting methodObject (grammar)Parameter (computer programming)Physical systemWindowLimit (category theory)Kernel (computing)1 (number)Band matrixMechanism designRepresentation (politics)BefehlsprozessorGame controllerFrequencyMixed realityNumberNP-hardBitFormal verificationDifferent (Kate Ryan album)Computer animation
23:59
Formal verificationKernel (computing)ArmRevision controlHüllenbildungObject (grammar)BitKernel (computing)Complex (psychology)Mixed realityState of matterPhysical systemMoment (mathematics)Formal verificationBranch (computer science)Enterprise architectureModel theoryReduced instruction set computingClosed setPhysical lawLine (geometry)MathematicsOperator (mathematics)Functional (mathematics)Multiplication signComputer animation
25:49
Kernel (computing)Formal verificationMereologyTheoryMathematicsFunctional (mathematics)Control systemWordServer (computing)Context awarenessProcess (computing)Physical systemWorst-Case-LaufzeitMultiplication signScaling (geometry)Kernel (computing)Spherical capClient (computing)Software developerMathematical analysisMixed realityNichtlineares GleichungssystemCivil engineeringDivisorOffice suiteLink (knot theory)State observerNumberRun time (program lifecycle phase)CASE <Informatik>WhiteboardReal-time operating systemSpacetimeShape (magazine)PredictabilityComputer animation
28:37
Information securityReduced instruction set computingEnterprise architectureFeedbackExtension (kinesiology)Stress (mechanics)Open sourceCASE <Informatik>Latent heatInformation securityTask (computing)QuicksortBitGroup actionProcess (computing)Open setComputer hardwareCache (computing)Disk read-and-write headOperator (mathematics)Data managementCoprocessorMultiplicationFeedbackMultiplication signEnterprise architectureMachine visionNP-hardSpacetimeDependent and independent variablesGoodness of fitPhysical systemState of matterWeb pageComputer animationSource code
31:48
Reduced instruction set computingInformation securityExtension (kinesiology)FeedbackStress (mechanics)Enterprise architectureFingerprintPattern recognitionSoftware developerPhysical systemKernel (computing)Proof theoryService (economics)Computing platformElectronic mailing listEmailIdeal (ethics)Open sourceDirection (geometry)ArmRevision controlFormal verificationDevice driverData managementKernel (computing)QuicksortSoftware developerCASE <Informatik>Physical systemoutputNumberDecision theoryHacker (term)10 (number)BitGrand Unified TheoryOrder (biology)TheoryLevel (video gaming)CuboidPlanningStability theoryBuildingCore dumpMoment (mathematics)Real numberPhysical lawSpacetimeImplementationComputer animation
36:35
Data structureConstraint (mathematics)Open sourceWhiteboardElement (mathematics)Self-organizationProjective planeDomain nameSound effectDomain nameComputer animation
37:39
NumberElement (mathematics)WhiteboardARPANETCybersexSelf-organizationCommutatorElement (mathematics)CodeMereologyGrand Unified TheoryDisk read-and-write headPay televisionImplementationWhiteboardQuicksortRight angleFormal verificationSpacetimePhysical systemReal numberLink (knot theory)Multiplication signECosCybersexComputer animation
39:57
Sample (statistics)Moment (mathematics)Level (video gaming)Formal verificationRevision controlSystem callSign (mathematics)MereologySound effectAdditionForm (programming)MathematicsEmailCodeMultiplication signSampling (statistics)Core dumpComputing platformElectronic mailing listQuicksortKernel (computing)Proof theoryBuildingData structureComputer animation
41:48
Heat transferWhiteboardWebsiteData structureSystem programmingElectronic mailing listEmailBus (computing)Level (video gaming)WindowAssembly languageSoftwareCompilerCodeMereologyCuboidFrequencyMoment (mathematics)Proof theorySpacetimeComputing platformTerm (mathematics)Multiplication signBinary imageLine (geometry)Software engineeringScripting languageInvariant (mathematics)Kernel (computing)DivisorSoftware bugComputer hardwareFormal languageFormal verificationPoint (geometry)WebsiteEmailTheoremElectronic mailing listResultantComplex (psychology)Revision controlOperator (mathematics)BitTranslation (relic)Total S.A.Web 2.0ImplementationCompilation albumEstimatorFlagInsertion lossProcess (computing)Physical systemBinary codeChainCanonical ensembleInteractive televisionObject (grammar)AuthorizationWhiteboardHeat transferForcing (mathematics)Principal idealGoodness of fitGame theoryString (computer science)Information securityVirtual machinePhysical lawTheoryKeyboard shortcutMathematical optimizationSampling (statistics)Phase transitionSoftware testingControl flowMenu (computing)High-level programming languageWorkstation <Musikinstrument>Right anglePredictabilityCASE <Informatik>Form (programming)Set (mathematics)HypermediaLimit (category theory)Source codeComputer animation
50:19
Point cloudFacebookOpen sourceComputer animation
Transcript: English(auto-generated)
00:06
Welcome to the microphone and component-based operating system, Death Room. This is the, I'm not sure of how many iterations, but I think we've done that a lot, and I'm very happy to see that it's still growing and so many people come. Thanks. Our first speaker is Ganot Heiser.
00:23
You know him, he's the head of the SEO4 project for many years now, and he's going to give a project update. Thank you. Nice to see a few familiar faces. This is the third time I'm speaking at Fostev, but the first time I'm actually physically here, so that's really a nice change.
00:41
Okay, I'd like to give a bit of an update on where SEO4 is, and a lot of interesting things have happened over the last year. So just, who is familiar with SEO4? Who is not? Okay, so the next few slides are not completely wasted,
01:03
but I'll go through them quickly. So SEO4 is a system that is designed from the beginning for highest assurance, with the strength of mathematical proof. So it was the first operating system with a proof of implementation correctness, and then following proof of that
01:20
it enforces security properties. It's the first, and in at least as far as the open literature goes, only protected mode OS with a complete and sound worst case execution time analysis, which is what you need for hard real time. It's got what I claim is the world's most advanced mixed criticality features
01:41
for combining critical real-time functionality with untrusted code on the same platform. And besides all that, it's the fastest general purpose microkernel. It's been designed for real-world use from the beginning. And of course it's open source, because otherwise it would not be here. And quick rundown what the verification story means.
02:04
So we have a kernel that's implemented in C. It's of the order of 10,000 lines of code. And we have a mathematical, a model of the kernel's functionality in a mathematical logic called high-order logic hole. And we have a formal mathematical machine-checked proof
02:23
that under the semantics of the C language, all the behaviors possible by that code base are captured by the specification. So the kernel is, it's impossible for the kernel to operate out of spec. So that's a very strong sense of being bug-free.
02:41
And further, there is a proof chain that proves that the binary is a correct translation of the C. So that means the compiler's out of the trusted computing base, as well as our assumptions on C semantics, which is important because C doesn't have a well-defined semantics. And then there is proofs that the abstract model of the kernel is able to enforce
03:01
the classical isolation properties, the CIA properties, confidentiality, integrity, and availability. And together, this means this is the only operating system where you can actually say with a clean conscience that it is secure in the sense it can guarantee security of systems built on top.
03:21
There's a, and then we have the worst case execution time analysis. And there's a few limitations still. So for truth in advertising, there is, we are still working on verifying the kernel initialization. There's a few, particularly the MMU that's abstracted, but there's a PhD thesis just completed
03:41
that does that properly. And at the moment, there's no proofs about any timing channels. That's enough to use it in real world systems. So this is what we did in a DARPA project a couple of years ago, where we had military vehicles. You should think they are secure.
04:02
Turns out this Boeing, this is an autonomous helicopter built by Boeing. The red team took about two weeks to completely own it. We transferred that onto, we put SEO4 underneath basically. And in the end it was, the red team couldn't break in. Similar with these autonomous army trucks.
04:20
And there's other systems that are actually in defense use already, like this secure crypto stick that's approved for defense use up to secret. It was actually the first time software enforced isolation was by a military certification authority
04:43
he considered to be equivalent to hardware air gabbing. So this was a major step in development for high assurance systems. So what's going on at the moment? The hottest thing in town is RISC-V.
05:01
And of course, RISC-V being an open architecture is sort of a really good match for an open source kernel. And of course there was a whole deaf room yesterday on RISC-V as I know it is. People I assume are familiar with it. And it has a number of other advantages for us. And this is why at the moment we are investing a lot
05:23
or actually a company called Hensault Cyber is investing a lot on getting SEO4 verified for RISC-V. So I need to disclose, I've got an interest in that company based in Munich and what they're building is a secure hardware software stack, basically on open technology.
05:42
They're producing their own processor chip. This is based on the open source Arian RISC-V core from ETH Zurich. And combine that with a supply chain security story, basically encryption of the logic circuit
06:02
so they cannot be tampered with in the production process. So this is against an untrusted fab inserting a Trojan into the hardware. And this is then combined with an operating system based on SEO4. And so in order to achieve this, they needed a verified kernel on SEO4, on RISC-V.
06:24
And so they're funding our RISC-V development, which is pretty cool for us. And their aims are basically anything where security or safety is critical. So defense obviously, but also critical infrastructure, automotive, avionics, et cetera.
06:42
And there's sort of leads in all these spaces. So this is the actual first product will be ready next quarter probably. And then it will be deployments will start in real world critical systems. So this is awesome. The RISC-V, there's two parts to this story.
07:00
There's actually the port of the kernel to the RISC-V architecture and then the whole verification. And the first one is relatively straightforward. We've done that a couple of years ago. And just to give you an idea of how it works, these are the performance figures for SEO4 on X86 on ARM, standard X86 on ARM platforms,
07:21
32 and 64 bit mode. And you can see it's of the order of six, 700 cycles. This is the cost for a round trip IPC operation, which is the fundamental operation you perform in a microkernel based system. So the operation you need for invoking any service.
07:40
And this is cheating a bit in the favor of X86 because we disabled the, jumped too far, disabled the meltdown workaround. Of course, Intel is shipping broken hardware and you need to go to extra lengths in order to work around the security implications. So if you actually enable a meltdown defense, then the performance gets much worse.
08:01
But this is sort of the baseline, which is fairly comparable to ARM. And then how does RISC-V look like? Jumping too far. You can see if you just compare the intra-address-based performance figures, which are generally useless. Anyone who published intra-address-based IPC,
08:20
I think I just laugh because it's meaningless. You don't need that normally. But I put it up as a baseline. You can see that we are pretty much on par with ARM slightly faster. The thing that really counts is an IPC across address spaces, so across protection domains. There we are significantly slower at the moment,
08:41
but this is because we used one of the first actual RISC-V hardware. And this is the Hi5 Unleashed from Sci5. And it doesn't support hardware AC attacks on the TLB. And therefore you need to flush the TLB on every contact switch. And this is why you get the degraded performance. With a RISC-V processor that had ACID support,
09:05
you should see exactly the same latency as intra-address-based as you see it on ARM. So it's basically the same model. So this is why the 690 is sort of the relevant number. The other is basically hardware-inhibited, if you like.
09:21
By the way, if you have any question, ask any time. Just interrupt me, raise your hand or whatever. Okay. So this is nice. Obviously, the RISC-V spec is in development. The base privilege spec has just been ratified a few months ago,
09:41
but a lot of the other things you need are still in development, in particular hypervisor support. So support for hypervisor mode is basically still in draft state. It just got upgraded to draft version C. 0.5 about a month ago or so. And we have implementation for hypervisor mode in there.
10:04
But because the spec is still in flux, we have it in a branch rather than a main line. But we're basically tracking the branch. Or rather, we are tracking whatever QEMU supports. And QEMU is fairly good in tracking the draft.
10:20
But it actually works. On this version in QEMU, we can run Linux on top. And the support is pretty straightforward. Now, the other side, of course, is the verification side. How are we doing there?
10:40
The present status is that we are not quite there yet. I was really hoping I would be able to announce that we are done. And we sort of planned to be done by the end of last year. But things, resources got shifted to other things. And so it slowed down a bit. So we are not quite done yet. At the moment, the functional correctness proof is due first quarter, this quarter.
11:05
And we're really hoping for next month. No, actually end of this month. Next month would be the end of the quarter. And so this is the functional correctness, the proof that the C implementation satisfies the spec. And in parallel, we are working on adapting the translation validation toolchain to RISC-V.
11:26
There's actually two things. It's only so far been used for 32-bit ARM. So it needs to be adapted to 64-bit binaries and the RISC-V instruction set. And it's not quite trivial because it uses SMT solvers.
11:41
And for them, 32 and 64-bit makes a big difference. But this is in progress. And it's supposed to finish next quarter and the target date is really end of April. And then we have a verified kernel on RISC-V. We're also working, but that's a background activity
12:02
because so far no one's put money on the table for it. It's the worst case execution time balance of the binary. There's actually a lot of overlap between that toolchain and the translation validation so it will benefit, the one will benefit from the other. So, yep, we're getting pretty close, which is exciting.
12:24
And what did we learn from working with RISC-V? Turns out it's actually all pretty straightforward. It's a simple, clean architecture. We didn't run into any real issues.
12:40
There was some instances where a few things were a bit more complicated than R, mostly because there's less semantics in the page tables and page tables tend to be a big part of the verification story. But basically, I think the first port was running in two weeks or so and the verification story is always an order of magnitude or two bigger,
13:02
but it's ongoing. And definitely, yes, the cleanness of the architecture really helps verification. The hypervisor extensions, at least in the draft spec as they are and they're not going to change massively, are even simpler. It's really just a few small features
13:21
and the student did that more or less over the weekend. There's this M mode. I'm not sure how familiar you are with RISC-V. RISC-V has three execution modes, user and supervisor, of course. And underneath is M mode, which is really meant for firmware. So this is basically, in Intel you have the four rings,
13:45
really only two, three and zero, which is user and kernel. And then underneath you have another three, four, five, six, seven, whatever rings that contain privileged code that can do anything underneath you and you have no clue what it does and it's all very scary.
14:02
In RISC-V, this is very clean. There's just one other more privileged level. This is M mode for machine mode and that does everything that's not done by the hardware. And the typical way to use that one is, there's really two purposes. The one is initializing the hardware
14:22
and the other is instruction emulation because RISC-V has a few, a fair number of APIs, let's say, that may or may not be implemented in hardware. The architecture promises they are there but they may not be supported in hardware,
14:40
in which case they get emulated in firmware. So that's part of the M mode code. From our point of view, obviously it's security critical so eventually it will have to be verified. At the moment, we're not working on that. But from our point of view, we keep it as simple as possible. We just use it as part of the initialization code that basically configures some hardware
15:02
and delegates everything it can up to supervisor mode and then SEO4 is in control. This is one of the really nice things about RISC-V. It has a lot of privileged features that by default are restricted to M mode, but they can all be delegated upwards. And typically to S mode, but sometimes even to U mode,
15:22
including support for user level drivers and all that stuff. It's really done very neatly and cleanly. And then with the hypervisor support, it's a bit Intel-like and orthogonal thing, which they tend to call HS mode for hypervisor S mode. So this is where the hypervisor then runs.
15:42
It looks pretty much like S mode, except it has access to some additional state in order to do world switches. And when we run SEO4 as a hypervisor, it runs in HS mode, just the kernel, which all it knows about hypervisor support is there's certain exceptions,
16:01
and it forwards them upwards to VU mode. So this is the model Nova pioneered years ago, and we've been using it in SEO4 for all of our architectures. So the actual virtual machine monitor runs in VU mode, and then the rest runs in the normal mode.
16:22
There's some issues that because the ISA is quite extensible that this could lead, diversity can be good and can be bad, and if it leads to fragmentation, then it's obviously bad, and there's some concern there. The RISC-V foundation is pretty aware of that, and so they try to avoid fragmentation
16:41
by making it clear what you should and shouldn't be doing. We'll see how that works out. There's no guarantee it will work. And it has now a BLAST formal specification. So there is a formal model of the RISC-V instruction set. And this will be the reference model.
17:01
So far, the reference model has been an informal model, and so in the future, everything will be developed as well as tested and verified ideally against this formal spec. And the formal spec, it's the sales spec from Peter Sewell at Cambridge, is actually very readable.
17:23
Even idiots like me can read it, which is the developers actually find that very useful. Our core OS developers, they're not formal methods people. We work very closely together, but most people only understand one side or the other, and they find it useful to actually look at the formal spec
17:42
because it's much more precise than the normal English version. And it's readable enough to be useful for general kernel developers, so that's really good. And, of course, there are people working on verifying RISC-V core implementation against that spec, and that will be really awesome
18:01
when we can get something that actually hangs together the hardware and the software verification by this formal spec. Any questions? Good. Next thing I want to talk about is mixed criticality, just a bit of an update.
18:21
I actually talked about this last year at Fostem. Some of you may have been there. Some of you may even remember some of it. I don't make any assumptions, but I just give a quick repetition of what it's about because it's also in verification. So the idea is we have mixed criticality systems. We're in the same process.
18:41
You have highly critical stuff as well as untrusted stuff. So this is a very simplified model of an autonomous vehicle. You have a control loop which controls the vehicle and therefore is highly critical. It is a hard real-time system that needs to deliver a response by a hard deadline,
19:03
but it runs at a very low rate, so typically order of 10 to 100 Hz, and then it runs for a millisecond or so. And then you have untrusted stuff that runs on the same hardware but is more time critical. Think of an Ethernet driver. An Ethernet driver needs to be able to serve packets
19:22
at microsecond rates, and if you just gave this one the higher priority, it would log out the Ethernet driver for milliseconds, and then you would lose packets, et cetera, where, of course, you know that you've got enough headspace on your processor, so this would be a stupid design. So instead, we give the untrusted driver a higher priority
19:44
so it can preempt the control loop but have support that ensures that we can guarantee enough time to the control loop. And we do this by having a notion of budgets that allows us to constrain the driver to just a short period of operation and allows us to reason
20:01
about the timeliness of the whole thing. So this is the basic idea. There's some challenges behind it. For example, you need to be able to share. The typical way a thing happens, you have a vehicle control. You have some navigation software that talks to maybe a UI if it's a car with a driver
20:21
or a base station if it's a totally autonomous vehicle with some remote control, and so the navigation will update waypoint data, which the vehicle control uses for navigation. And so they need to share this data set, and obviously there are some atomicity requirements
20:40
where the vehicle control must only see consistent data. It's not required that it always sees the absolute latest version. If it sees the update a millisecond later, who cares? But it needs to see consistent data. So there's some locking requirement. And the way this is typically done
21:00
is by a so-called resource server. So you encapsulate this shared data into a server. It runs as a protected process, and that gets invoked by both the highly critical and the low critical. And now you need to make sure that the less critical thing, which is not trusted, cannot stop the timely operation of the critical thing,
21:22
and this is sort of a challenge. And so you need to be able to have these servers that are shared across criticalities. And the nice thing, if you do this, then if you give the server the ceiling priority, it implements the immediate priority ceiling protocol, which is a very efficient, nice, behaved protocol
21:41
for real-time locking. The question is, okay, who pays for the server time? Because if the server executes on behalf of one of the clients, then, well, in the standard setup, it would consume its own time and its own priority, and this, for example, this untrusted thing
22:01
could just toss the trusted thing by keeping invoking the server with expensive operations, and we need to avoid that. And so the solution, and I won't go through all the implications, but the basic solution is we have this original model which consists of priority and a time slice as the scheduling parameters, and we replace this time slice by a generalized notion
22:23
of a time slice, which is a scheduling context. So the thread now has a capability to a new kernel object called a scheduling context, and a scheduling context contains a number of things, but the critical ones are a budget and a period, and the guarantee is that over any window
22:41
that is less than or equal the size of the period, it cannot consume more than the budget. So this is a very hard bandwidth limitation thing, and this is the basic mechanism. It's a pretty straightforward mechanism. It's actually very tricky to implement and immensely difficult to verify, as we find out,
23:01
but this is the basic mechanism that allows us to reason about timeliness in these mixed criticality systems. So we have different scheduling contexts that give different bandwidth. So this one has a period of three and a budget of two, so it can consume up to two-thirds of CPU time,
23:21
and this one has a period of 1,000 and a budget of 250, so this could be representative of our control loop, and this could be the Ethernet driver, and we can show that, well, together they use less than 150. They cannot use more than 100% of CPU bandwidth,
23:41
and actually it's a bit lower for various reasons, but basically this allows us to guarantee that this one will always meet its deadlines, even if this one is running at a higher priority, so it's a very cool thing. And as I said, this is the design
24:01
for enabling this mixed criticality system. And so this is also now being verified. So we finished the model about almost two years ago, and since then we've been working on verification, and it turns out this is a really hard thing because it increases kernel complexity a fair bit.
24:20
In the past, any kernel operation had only to deal with up to two kernel objects at a time, and this one, with this model, we have to deal with up to five kernel objects at a time, and that's really blown out verification and also the effort on verifying this thing.
24:41
So the state of the play is we have the mainline kernel, which on ARMv7 is completely verified. We have the RISC-V version of the mainline kernel, which I just talked about before, so that's close to being finished. And then we have the mixed criticality kernel,
25:02
which at the moment we are verifying on ARM. And originally we were hoping to have this finished by about now, but as I said, it turned out to be way more complicated, so it will take us most of this year to finish that one. And then we'll have the mixed criticality kernel branch verified on ARM,
25:24
and then we will merge that together, and this merge is, we expect that to be fairly straightforward, probably take us a few weeks, because the features in the mixed criticality kernel are mostly architecture independent, so merging this ARM verification with the RISC of MCS
25:42
with the RISC-V mainline verification, we expect to be straightforward and also be finished this year. And then we will place this one as the mainline, the old thing will become legacy, and the MCS features will be the properly supported kernel,
26:00
which is fine because it's a forward compatible change. The MCS kernel can fully emulate the functionality of the old kernel. Cool. Any questions? Yeah? Would you have a word of caution for the developers of the control loop in your mixed criticality session?
26:22
Well, now, taking two sensor values, for example, may spawn 100... Yeah, yeah. There's sound, so the question is, be careful when you do these mixed criticalities. Yes, there's actually sound shetling theory behind it. It's a well-explored space, and people are still writing papers about it,
26:44
but most of them are fairly useful. But the basic shetling theory has been established a while ago and is fairly straightforward. Yes? Once you have scalability for such devices,
27:04
you will lose everything. So, okay, how does that scale if you have a lot of activities? Well, as part of, and again, this is well-established real-time shetling theory. As part of your shetling ability analysis, you need to analyze the worst-case pre-emptions,
27:21
number of pre-emptions, and you need to factor in the cost of these pre-emptions, which in SA04 is possible because we actually have a worst-case execution time analysis. We know how long a pre-emption can worst-case take. There's no other system around that where you can do that. Okay, yep?
27:47
You cannot have more than one-time capability. A process can have, at most, one-time capability. Otherwise, if it doesn't have one, it is not runnable. But one of the nice features,
28:00
it can run on a borrowed time cap. So if you invoke a server, we can have a notion of a passive server that doesn't have a shetling context and is, as such, not runnable. But if you invoke it, you pass your shetling context onto the server, and then the server runs on yours, and this is how the charging of server time against the client happens.
28:22
So the client basically needs to provide the time to the server. I'm happy to talk about it in more detail about that. I didn't want to go into this in much detail here in the talk. My last main topic is community. I assume there's a lot of interest here,
28:41
and there's two aspects of that. The one is how did we engage in some other community, which in this case was RISC-V. This is an open-source community. It's an open spec community, really, but it's an open development process. In RISC-V, there is the RISC-V Foundation, which owns the thing, and it has what's called standing committees.
29:05
It used to have one for security. Now it has one for the ISA specification, and under the standing committees are task groups, which work on particular aspects of the spec. The privileged spec used to be a task group.
29:21
It just split into multiple task groups and became a standing committee. There are people who work on, say, cache management operations and the MMU specification and all that sort of thing. We engage with them. For doing the RISC-V port,
29:40
we didn't have to engage very much, but if I have time, I'll talk about what we do about timing channels, and there we did have to engage a fair bit. It was a very good experience. People are basically open. They listen. They are open to suggestions. Of course, most of them get knocked on their head
30:01
because they don't fit the philosophy. That's normal. We do the same because you really need to make sure that everything is properly aligned with an overall vision, et cetera, to keep it clean, but they are definitely very open, particularly the security standing committee. They pulled me in originally about nine months ago,
30:20
no, over a year ago, a year and a half ago because of the work we are doing on timing channels, and they were very keen to have RISC-V being recognized as the world's most secure process architecture. I found the engagement there very positive. I'm getting what I need to make it secure, basically.
30:43
And then the PRIF spec, our engagement there was mostly providing feedback on the hypervisor spec, and we did a five-page paper discussing our experience with a spec and circulated around and said, these are the problems where we think there should be something better support, et cetera,
31:02
and the reaction was very positive, and the person who is in charge of this spec group made a suggestion on a very elegant way to fix it, and so this is likely to appear in the spec. So that was a pretty good experience.
31:23
What I needed for making the processor or the system secure against timing channels, that was a bit of a harder push, convincing the hardware people that this is a real problem and you need to solve it, et cetera, and there was a lot of support from the security standing committee, and now we're in the process
31:41
of someone actually speccing out the operations which I need to provide real security. So that's all cool. It has all the good and the bad sides of an open-source community, right? It's sort of, yes, they are very cooperative, very open, but also things work slowly.
32:02
If you have one expert just designing everything, that's much faster, but of course, there's a risk of them overlooking something, and so this is why it will be at least a year until we have a finalized hypervisor spec, for example, but it's moving in the right direction. So the other thing is our community,
32:21
the SEL4 community, and you may have heard if you're on the mailing list that we're setting up an SEL4 foundation under the Linux Foundation, and there's a number of drivers for that. The one is that people are sort of worried, the company's betting basically the company on SEL4.
32:43
They're building, SEL4, if you use it, is really at the innermost guts of your system. Everything depends on it, and if SEL4 fails, then you have a problem, a very serious problem, and so companies are basically investing heavily in SEL4-based technologies, investing tens of millions in systems
33:02
that are intimately tied to SEL4, and they want to see some stability, and they're nervous that we are in an open, in a public sector research lab, so that's better, a bit more reliable than being in a startup, but still, right, we depend on decisions that are made at high management level, and in theory,
33:22
it's unlikely to happen in the foreseeable future, but in theory, they could pull the plug, and then what happens with SEL4? If the trustworthy systems group, which is behind SEL4, goes away, SEL4 will be dead, and that's, of course, a real danger, and so this is one of the reasons for the foundation to address this. This will be able to give us stability.
33:43
There will be companies involved in funding the whole thing. If the worst case happens, we could just set up somewhere else and keep on getting the support from the foundation to keep on working, so it's a reinsurance for those who are investing on SEL4, but it's also very important to grow the ecosystem,
34:03
and we open-sourced SEL4 about five and a half years ago, and there is an ecosystem of developers around it, but it hasn't grown anywhere near as fast as I hoped for, and having this open-source foundation, we hope will really help develop this ecosystem faster
34:23
and so enable more participation, et cetera, and then we have a kernel. We know what the kernel does and what it should be, but then in order to deploy it in a real-world system, you need much more of that. You need the actual system, and at the moment, that's extremely rudimentary,
34:43
and it will definitely benefit from developer input in specifying higher layers of this ecosystem and implementing and maintaining, et cetera, so that's the third motivation. The fourth was to protect the brand, and this is a critical one
35:01
because SEL4, its value is the verification. Its value stands and falls with the verification, and the one scenario that really worries us is someone takes the kernel, hacks it, deploys it somewhere, claims this contains verified SEL4, and because they hacked the kernel, they introduce the bug,
35:21
and our experience is anything that's not proven correct is buggy, so we know people have hacked the kernel, and because of that, we have to assume that they have a buggy kernel, and they deployed it and said it contains verified SEL4, and that is really scary because if someone hacks that one, we know they didn't hack our kernel, but the reputational damage could be massive,
35:41
and so we see the foundations of WaveBull walking that. And the other really, and all these are sort of equally important. We have a few verification items which are too big for anyone. Everyone wants them, but they are really big-ticket items. One is ARM 64-bit, ARMv8,
36:03
and the other is the multicore version. We have a high-performance multicore implementation, but it's not verified, and everyone wants that one, but the cost of doing that is too high for everyone who wants it, and the foundation will give us the opportunity to get people together
36:21
and pool the expense for everyone's benefit and hopefully make that happen. So I'm confident that within a year or so, we'll be able to line up through the foundation funding for one or hopefully both of these big-ticket items. So how does the foundation work? It's a standard setup of the Linux Foundation,
36:42
so under the Linux Foundation, there is the SEO4 Foundation. It has a board, and it has the directed fund where the member contributions go to, whether it's the membership fees or extra contributions, and the board is mostly responsible for deciding where this money is spent. And there's a fund charter, which is the legal document that says what the constraints are.
37:04
And then there is the actual open source community, so this is the SEO4 project, which is under the Linux Foundation Projects LLC, so that's a company, a nonprofit organization, and the SEO4 LLC will be a virtual company under the Linux one,
37:22
and it owns all the artifacts. So it owns the SEO4 trademark, the GitHub, the domain name, et cetera, and it has a technical charter that defines what it's supposed to do, and then there's a technical project, and all the contributors are members of that one. And the governance is, okay, there's members,
37:45
and it's a tiered membership, so there's premium members, and then there's regular members, which the fees depend on the size of the company, very similar as Linux. We made it cheaper at the low end and more expensive at the high end. And then there's also associate members,
38:02
any nonprofit organization or individuals can join us as associate members, and they pay no fee. And then there's the technical steering committee, which is made up of the committers and some technical leaders. We have this notion of technical leaders because there's people, me, for example,
38:21
who never commit any code to SEO4. I may commit to documents, but not to the real guts. I leave that to the people who actually understand all the details. I understand the design. Other people understand the implementation way better. And so people like that, the technical heads should be also a part of this technical steering committee.
38:43
And then there is the board, and it gets elected by members. So we will have three seats on the board for the time being. This is initially an arrangement for five years. Premium members get the right to a board seat, and the rest of them, the regular members together, elected a board member,
39:02
and the head of the technical steering committee will also be in the board. And remember, the board's sole role is to determine where the money goes, how to invest the membership fees, basically. And this is the initial board. So the three leaders from Trustworthy Systems will be on there.
39:21
John Launchby was a great supporter of SEO4. He was director in DAPA and did a lot for getting visibility in the defense space. He's now back in his company, Galois, who does all sorts of work. Sascha Keikweis is from Hands-On Cyber, the company which, as I said, is funding the RISC-V verification.
39:43
He's the CTO there. And then Daniel Potts from Ghost Locomotion. Ghost is an autonomous driving company. They are betting heavily on SEO4, and so they make up the initial board. And how is the community supposed to work?
40:02
So there's different levels of artifacts. First, of course, there's the kernel, which contains of code and proofs. And for the time being, we will need to be in charge of evolving the kernel because any change to the kernel, you need to understand what effect it has on the verification
40:21
and how it can be verified and it needs to be verified, et cetera, and ensuring that it fits the philosophy. But, of course, we hope to get contributions from the community, certainly in form of platform ports. And just last week, there was a discussion on the mailing list on someone suggesting additional kernel features.
40:43
And after some discussion, we came up with a much simpler version of that, and that may get into the kernel. So this is another form of community contribution. And then there is what I call core user land. So this is what you absolutely need to build anything sensible on SEO4. And at the moment, this is all dependent on us,
41:03
and that's a bad thing. And obviously, we need to provide at least initial versions of that. But then we really hope the community to contribute and even adopt some of these pieces. And then, and of course, the core user land. So this is all stuff which in Linux will be part of the kernel.
41:21
And then there's the what I call other user land, which is in Linux would also partially be in the kernel, partially be user level. And there we want to sort of step back as much as possible, probably provide samples to give people an idea of what the right way is to structure something, architect something. But we really want this all to be owned by the community.
41:41
And over time, we would hope the community engagement will get deeper and deeper. So status of this is we have just last week got the final sign off from everyone involved on the legal documents. So they are now final. They should probably go up on our web interim website tomorrow.
42:04
And the trademark is ready for transfer. We have an initial board. We have an initial website that contains these documents and pretty much what I said here. And literally I think we're probably days away from being able to actually sign up members.
42:23
If you're interested, follow the mailing list or just send mail to the foundation. And this is the initial website for the foundation, which basically contains a version of what I said here. And I'm getting towards the end of my time slot so I won't be able to talk about the time protection
42:43
principle timing channel defense work. So I'll leave that for next year then, I guess. Questions? Could you talk a little bit about tooling? You mentioned the problem of other people taking your kernel and then hacking away and selling it as SEL4.
43:05
So we will have to face the problem of a canonical compilation eventually, so building an image, a binary image that can be compared against another compilation process. Was it a problem of compiling? Yeah, so, okay, the question is,
43:22
what do we have in tooling and how dependent we are on it? In terms of the verification story, that's not actually a big deal. I mean, there's a standard setup. It comes with a build process. You just build with the right flags and it does everything using GCC. It's a bit fiddly with the GCC version because the kernel depends very strongly
43:43
on some micro-optimizations and some GCC features and they may break, et cetera. But basically, that's not really the issue. And in the end, when you have a binary, it is a bit of experience with these formal methods tools, but it is possible in principle to actually run the binary,
44:02
the translation checker against that and against the formalized C code that falls out of the theorem prover, et cetera, and check the tool chain yourself once you build a binary. I want to sign a binary. I want to sign it to you and you should have the same result.
44:22
Yeah, okay. Yeah, you don't need me to sign a binary. If you want me as the authority that you trust, then yes, we can do that. And at the moment, this would be... No, we don't actually have binary downloads. But yeah, this is probably something we want eventually.
44:42
And of course, it wouldn't be me. It would be the foundation who does that. And so this is probably part of the job of the foundation, yeah. Other questions? Yeah. How do you deal with platforms where certain devices
45:01
have to be configured the right way to have platform security, like DMA capable stuff? So as the system MMU at the moment is not part of the verification story, and that's of course a big hole. I should actually have that in my yellow box. I forget about that. It's in the other privileged stuff.
45:23
Yeah, this is something we're working on, but that's not completed yet. But it's clear for a complete story if you have any DMA capable bus mastering device on your system, then you need the IOMMU to make sure it doesn't do anything it shouldn't be doing. Otherwise, all guarantees go out of the window.
46:07
Three, four hundred cycles? Not on x86? No. So the question was about the IPC latency on x86. No, this is the best you can get.
46:26
I've never seen anything faster, and we analyzed it to death. We know we are at the hardware limit.
46:47
Okay, so that's a really good question. To give you an idea, for the 10,000 lines of C, the initial proof was 200,000 lines of proof script. The total proof base has now grown to over a million lines.
47:00
Of course, once you've done a proof, then you can at any time run it through the proofer again, and it will just say yes or no, which is nice if you maintain. If you do, say, micro-optimizations on the code, sometimes you gain proof performance by just moving things around so the compiler can infer invariants that are not obvious from the code otherwise.
47:22
Sometimes, if they are semantic neutral, the proof may still go through. In other cases, it will fail, but at least it points you exactly to the point where something fails, and then either you introduce the bug or you violate it, or some invariant may still be valid,
47:40
but the proof cannot prove it anymore, and then you have to reprove. There's some of this work, and typically it's probably somewhere between a factor of 5 or 10 more verification efforts than implementation effort. With the MCS kernel,
48:00
the ratio turned out to be much bigger. We completely underestimated the effort required there. This was because of the complexity I mentioned earlier, that operations involve so many kernel objects, and you have to prove so many more invariants that the complexity really massively increased.
48:20
We had one example before where we introduced a new kernel object where experience was similar. There was much more effort to reprove. We took that into account, and still it was worse because we underestimated how the interactions actually worked. In terms of more straightforward things, for example, platform ports, we are very good in estimating the cost.
48:42
Our estimate for the RISC-V verification, for example, turned out to be conservative. We probably make a profit on what they've given us, but we make a huge loss on the MCS verification. It's a bit of a black art, but it's actually encouraging that at least
49:01
some of the space we can reasonably predict. Proof engineering is basically where software engineering was 50 years ago. Repeat after me,
49:21
kernel should not be written in anything but C, period. As a simple reason, if you want a high-performance kernel, you need to know what the code is doing. Assembler is too low a level. C is basically the kernel assembler. If you read some C,
49:40
you know what code is going to fall out. With a high-level language, there's too much stuff hidden, and you get inefficiencies. You get surprises. The compiler may do stuff you never imagined, et cetera, and then leave alone managed language. You never want anything like that near the kernel.
50:02
But anything higher up, C should under no circumstances be used. Actually, I think it's professional misconduct to develop higher-level software in C. It just shouldn't be done. Thank you very much.