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

RedLeaf: Isolation and Communication in a Safe Operating System

00:00

Formal Metadata

Title
RedLeaf: Isolation and Communication in a Safe Operating System
Title of Series
Number of Parts
287
Author
Contributors
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
At least since the final Multics report in 1977, researchers identified the ability to isolate kernel subsystems as a critical mechanism for increasing the reliability and security of the kernel. Unfortunately, despite many attempts to introduce isolation to the kernel, modern systems remain monolithic. Historically, software and hardware mechanisms introduce a prohibitively high overhead for the isolation of subsystems with the tightest performance budgets. Today, however, the balance of isolation and performance is starting to change with the development of Rust, arguably, the first practical programming language that achieves safety without garbage collection. RedLeaf is a new operating system developed from scratch in Rust with the goal to explore the impact of language safety on operating system organization, and specifically on the ability to utilize fine-grained isolation and its benefits in the kernel. In contrast to commodity systems, RedLeaf does not rely on hardware address spaces for isolation and instead uses only type and memory safety of the Rust language. Departure from costly hardware isolation mechanisms allows us to explore the design space of systems that embrace lightweight fine-grained isolation of kernel subsystems. We develop a new abstraction of a language-based isolation domain that implements a unit of information hiding and isolation of faults. Domains can be dynamically loaded and cleanly terminated. Building on RedLeaf isolation mechanisms, we demonstrate the possibility to implement end-to-end zero-copy, fault isolation, and transparent recovery of device drivers. To evaluate the practicality of RedLeaf abstractions, we implemented a subset of the POSIX interface as a collection of RedLeaf domains. RedLeaf's isolation mechanisms allow us to support the transparent recovery of device drivers. To demonstrate that Rust and fine-grained isolation introduce a practically-acceptable overhead, we develop efficient versions of 10Gbps network and PCIe-attached solid state-disk NVMe device drivers that match the performance of carefully-optimized kernel-bypass device drivers used in modern network and storage processing frameworks.
System programmingDampingStudent's t-testReliefProcess (computing)Device driverFaculty (division)File systemOperator (mathematics)Operating systemMikrokernelImplementationSemiconductor memoryKernel (computing)Computer hardwareMechanism designProgramming languageType theorySpacetimeContrast (vision)SeitentabelleLimit (category theory)Device driverComputer animationDiagramEngineering drawingMeeting/Interview
Shared memoryModel theoryConnectionismSemiconductor memoryBefehlsprozessorGame controllerInterface (computing)Computer networkKernel (computing)Device driverLine (geometry)System programmingNumberWater vaporBit rate40 (number)Computer programmingAssembly languageCodeCore dumpSystem callComputerMathematicsImplementationProgramming languageHigh-level programming languageRadical (chemistry)UsabilityMikrokernelDataflowDecision theoryEnterprise architectureMereologySoftware bugSoftware developerTypsichere SpracheInformation securityNumeral (linguistics)Computer animationSource code
ForceOffice suiteInformationSystem programmingExplosionAddress spaceComputer hardwareSoftwareWeb pageTable (information)Overhead (computing)BefehlsprozessorIntelDevice driverCore dumpDevice driverBit rateCASE <Informatik>Computer networkStapeldateiModule (mathematics)Thread (computing)Domain-specific languageShared memoryObject-oriented programmingTrailVariable (mathematics)Data structureKernel (computing)Object-oriented programmingMemory managementConstructor (object-oriented programming)MikrokernelBoundary value problemComputer programmingPointer (computer programming)Domain-specific languageFormal verificationSemantics (computer science)LinearizationNumberState of matterKernel (computing)Internet service providerShared memoryOrder (biology)Programming languageMultiplicationWorkloadSoftwareField (computer science)MereologyParameter (computer programming)Overhead (computing)System programmingSemiconductor memorySocial classModule (mathematics)Mechanism designUtility softwareFunctional programmingSystem callComputer hardwareSoftware developerStapeldateiVariable (mathematics)Cycle (graph theory)Interface (computing)Classical physicsPrimitive (album)Traffic reportingBefehlsprozessorCodeDevice driverSpeicherbereinigungDevice driverInformation securityModel theoryCompilerSeitentabelleSubsetUniqueness quantificationCombinational logicLie groupRange (statistics)Focus (optics)MathematicsVulnerability (computing)Projective planeInformation and communications technologyLine (geometry)Observational studyThread (computing)Error messageType theoryBitGame controllerCASE <Informatik>Hierarchy2 (number)Key (cryptography)Network topologyPrice indexPosition operatorProcess (computing)Image resolutionTorusGraph coloringElectronic mailing listDifferent (Kate Ryan album)Extension (kinesiology)Multiplication signComplete metric spaceCausalityOcean currentGroup actionForcing (mathematics)Wechselseitige InformationWordOperating systemBit rateDrop (liquid)DataflowSurface of revolutionVideo gameComputer configurationArithmetic meanOrbitComputer animation
BootingServer (computing)Domain-specific languageThread (computing)Scheduling (computing)Semiconductor memoryMemory managementDevice driverSystem programmingInstallable File SystemComputer networkSystem callCodeRing (mathematics)Regular expressionNumbering schemeLevel (video gaming)Windows RegistryObject-oriented programmingInvariant (mathematics)Pointer (computer programming)Type theorySubsetAlgebraic closureInterface (computing)Block (periodic table)Reading (process)WritingCompilerProxy serverImplementationStudent's t-testOperating systemBlogSystem programmingDomain-specific languageSubsetType theoryMikrokernelCASE <Informatik>Operator (mathematics)Object-oriented programmingWindows RegistryComputer fileComputer hardwarePointer (computer programming)CompilerProxy serverCodeInterface (computing)Kernel (computing)SoftwareMemory managementTrailBlock (periodic table)Reading (process)WritingBefehlsprozessorAlgebraic closureWeb pageRegular expressionInvariant (mathematics)Cycle (graph theory)System callMetadataRow (database)CountingCrash (computing)Interface (computing)Term (mathematics)Formal languageWrapper (data mining)Drop (liquid)Run time (program lifecycle phase)Ring (mathematics)Mechanism designError messageProcess (computing)Overhead (computing)Binary codeBuffer solutionINTEGRALStructural loadPoint (geometry)Thread (computing)Ideal (ethics)Normal (geometry)MereologyComputerHierarchyRootGreatest elementCore dumpConstructor (object-oriented programming)Computing platformMicrocontrollerDevice driverSemiconductor memorySet (mathematics)GradientCompilation albumFunctional programmingResultantBootingChainUniform resource locatorTheoryPrice indexData storage deviceArithmetic meanWebsitePhysical lawGoodness of fitException handlingState of matterNumberFunktionspunktmethodeWater vaporGame controllerMultiplication signOcean currentWorkstation <Musikinstrument>Extension (kinesiology)Complete metric spaceSymbol tableBuffer overflowProjective planeCausalityLie groupExtreme programmingDialectProgramming languageCone penetration testOpen sourceMathematicsMeeting/InterviewComputer animation
Similarity (geometry)Domain-specific languageInformation and communications technologyInterface (computing)Data recoveryWritingBlock (periodic table)Proxy serverAcoustic shadowObservational studyNormal (geometry)Device driverClient (computing)Denial-of-service attackSystem callCASE <Informatik>Error messageWrapper (data mining)Communications protocolObject-oriented programmingInterface (computing)Domain-specific languageData recoveryFormal languageCrash (computing)Device driverReading (process)Kernel (computing)Arithmetic meanResultantWorkstation <Musikinstrument>CodeWhiteboardOpticsSystem programmingOrder (biology)Overhead (computing)Graph coloringSoftware developerInformation and communications technologyInstance (computer science)Program flowchart
CodeSystem programmingTurbo-CodeState of matterBefehlsprozessorIntelBenchmarkRevision controlHash functionOverhead (computing)Element (mathematics)Different (Kate Ryan album)Order (biology)Cycle (graph theory)Symmetric multiprocessingProxy serverAcoustic shadowHash functionRevision controlComputer programmingThread (computing)CASE <Informatik>Computer hardwareSystem programmingComplex numberTable (information)BenchmarkKey (cryptography)ImplementationFunctional programmingComputer configurationMechanism designAdditionSystem callCodeCore dumpMikrokernelSynchronizationInterprozesskommunikationFlow separationAnalytic continuationObject-oriented programmingSoftware developerType theoryOverhead (computing)Point cloudBand matrixPairwise comparisonSemiconductor memorySubsetDomain-specific languageState of matterPrice index2 (number)MereologyProgramming languageMetropolitan area networkFreewareArithmetic meanForm (programming)Moment (mathematics)TunisComputer animation
Device driverProcess capability indexIntelComputer networkInterface (computing)Bit rateAcoustic shadowDomain-specific languageWorkstation <Musikinstrument>Cartesian coordinate systemSystem callOverhead (computing)Data conversionEqualiser (mathematics)System programmingBenchmarkProgram slicingSoftwarePoint (geometry)Interface (computing)2 (number)Dimensional analysisOperating systemLine (geometry)Device driverChemical equationAdditionInheritance (object-oriented programming)MultiplicationArithmetic meanConfiguration spaceFlow separationData storage deviceObservational studyMaxima and minimaTerm (mathematics)ApproximationBit rateSurfaceStapeldateiWeb 2.0Server (computing)Domain-specific languageStructural loadKey (cryptography)Acoustic shadowKernel (computing)Stack (abstract data type)SynchronizationNetwork socketComputer programmingPCI ExpressGeneric programmingComputer animation
Computer fileBlock (periodic table)WritingComputer programmingDomain-specific languageType theoryInterface (computing)System programmingSystem programmingCartesian coordinate systemCrash (computing)Software testingSemiconductor memory2 (number)Data recoveryDrop (liquid)Right angleProcess (computing)Programming languageData structurePersonal digital assistantPosition operatorSource codeState of matterConstructor (object-oriented programming)Metropolitan area networkEnterprise architectureInformation securityExtension (kinesiology)Exception handlingComputer programmingBenchmarkProxy serverDevice driverBlock (periodic table)Acoustic shadowBit rateMultiplication signKernel (computing)Computer fileWritingMemory managementFile systemValidity (statistics)System callCASE <Informatik>AbstractionShared memoryCompilerOverhead (computing)Interface (computing)Computer animation
MathematicsStreaming media2 (number)Cartesian coordinate systemProgramming languageSpacetimeComputer programmingComputer animationMeeting/Interview
System programmingRule of inferenceMessage passingDomain-specific languageRootNumberRegular expressionProgramming languageProcess (computing)Propositional formulaMeeting/Interview
Assembly languageCodeRegular expressionProgramming languageComputer programmingSystem callPoint (geometry)HorizonCASE <Informatik>SpacetimeProof theoryLevel (video gaming)AuthorizationExpert systemVector potentialInformation securityDimensional analysisSubsetKernel (computing)Computer hardwareRing (mathematics)Mechanism designDirection (geometry)Type theoryLine (geometry)Primitive (album)Computer clusterLimit (category theory)Mereology2 (number)Group actionAreaSound effectBasis <Mathematik>Insertion lossRight angleKey (cryptography)SpeicherbereinigungBinary codeMeeting/Interview
Category of beingAddress spaceComputer hardwareObject-oriented programmingSpectrum (functional analysis)Social classSystem programmingState of matterDomain-specific languageMeeting/Interview
Domain-specific languageComputer engineeringComputer hardwareExpected valueBranch (computer science)Cache (computing)Group actionTerm (mathematics)Programming languageOverhead (computing)Uniqueness quantificationRight angleCanonical ensembleSemiconductor memoryPrice indexReading (process)Wave packetDivisorMeeting/Interview
Process (computing)Cartesian coordinate systemObservational studySemiconductor memoryCore dumpInvariant (mathematics)MikrokernelCompilerDevice driverModel theoryConstructor (object-oriented programming)Electronic signatureDomain-specific languageModule (mathematics)Boundary value problemRight angleMeeting/Interview
Mathematical analysisInvariant (mathematics)Fluid staticsObservational studyComplete metric spaceOffice suiteSystem programmingCategory of beingString (computer science)Programming languageSoftware developerInternet service providerRight angleSpeicherbereinigungArithmetic meanMeeting/Interview
SubsetProgramming languageArithmetic meanReverse engineeringMultiplication signLine (geometry)Row (database)MereologyMeeting/Interview
System programmingMultiplication signMereologyKernel (computing)Software developerComputing platformFitness functionPlanningRight angleModel theoryMeeting/InterviewComputer animation
Different (Kate Ryan album)Programming languageCategory of beingMathematicsBitLaceTerm (mathematics)Radical (chemistry)Meeting/Interview
BitCodeTerm (mathematics)Structural loadDynamical systemProgramming languageVector spaceSystem programmingIdeal (ethics)BuildingCollisionInterface (computing)Object-oriented programmingRight angleMeeting/Interview
Wechselseitige InformationMultiplication signMeeting/InterviewComputer animation
Transcript: English(auto-generated)