We're sorry but this page doesn't work properly without JavaScript enabled. Please enable it to continue.
Feedback

seL4 Microkernel Status Update

00:00

Formal Metadata

Title
seL4 Microkernel Status Update
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
Publisher
Release Date
Language

Content Metadata

Subject Area
Genre
Abstract
I will give an overview of where seL4 stands today in terms of functionality, verification, ecosystem, deployment and community. The focus will be on what has happened in seL4 land over the past 12 months, which is a lot: seL4 Foundation, RISC-V support and introducing time protection. The biggest news of the year is that we are in the process of setting up the seL4 Foundation, as an open, transparent and neutral organisation tasked with growing the seL4 ecosystem. It will bring together developers of the seL4 kernel, developers of seL4-based components and frameworks, and those deploying seL4-based systems. Its focus will be on coordinating, directing and standardising development of the seL4 ecosystem in order to reduce barriers to adoption, raising funds for accelerating development, and ensuring clarity of verification claims. I will report on the state of this. The other big development is that we are closing in on completing verified seL4 on the open RISC-V architecture. This includes the functional correctness proof (that guarantees that the kernel is free of implementation bugs), the binary correctness proof (which guarantees that the compiler did not introduce bugs) and the tranition to the new mixed-criticality scheduling model, which supports the safe co-location of critical real-time software with untrusted components, even if the latter can preempt the former. Finally, on the research side we have introduced the new concept of time protection (the temporal equivalent of the established memory protection) that allows us to systematically prevent information leakage through timing channels.
MikrokernelPhysical systemExterior algebraFigurate numberOperator (mathematics)Speech synthesisBitDisk read-and-write headProjective planeMultiplication signComponent-based software engineeringMathematicsComputer animation
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
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
Information securityARPANETPhysical systemProof theoryControl flowBit rateProjective planeReal numberSoftwareComputer hardwarePhysical systemMultiplication signAuthorizationCryptographyInformation securitySimilarity (geometry)Autonomic computingComputer animation
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
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
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
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
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
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
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
Game controllerDevice driverSoftwareAtomic numberCASE <Informatik>Revision controlComputer animation
Server (computing)Server (computing)Operator (mathematics)Multiplication signQuicksortCommunications protocolService (economics)Shape (magazine)Real-time operating systemNormal (geometry)Computer animation
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
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
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
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
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
Data structureConstraint (mathematics)Open sourceWhiteboardElement (mathematics)Self-organizationProjective planeDomain nameSound effectDomain nameComputer animation
NumberElement (mathematics)WhiteboardARPANETCybersexSelf-organizationCommutatorElement (mathematics)CodeMereologyGrand Unified TheoryDisk read-and-write headPay televisionImplementationWhiteboardQuicksortRight angleFormal verificationSpacetimePhysical systemReal numberLink (knot theory)Multiplication signECosCybersexComputer animation
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
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
Point cloudFacebookOpen sourceComputer animation
Transcript: English(auto-generated)