Language-Based Safety MechanismsConcepts Overview & OutlineContrast With David’s “Req Spec”What Is “Safety” in this context?TechniquesBackground: “The Thin Red Line”Call GatesBackground: Virtual MachinesVM ExamplesWhat Can You Do With This?Static Analysis, Type-Safe LanguagesExample: Spin and Modula-3Limiting the LanguagePros & Cons of Static AnalysisStatic analysis, cont’d.At Runtime: Classic SFI and JanusPros & cons of runtime approachesDynamic Dataflow AnalysisInterface CompilationExploiting SemanticsInterface Compilation With MAGIKIC as an Orthogonal MechanismLessons? Anyone?Language-Based Safety Language-Based Safety MechanismsMechanismsStanford University CS 444A, Autumn 99Stanford University CS 444A, Autumn 99Software Development for Critical ApplicationsSoftware Development for Critical ApplicationsArmando Fox & David DillArmando Fox & David Dill{fox,dill}@cs.stanford.edu{fox,dill}@cs.stanford.eduConcepts Overview & OutlineConcepts Overview & OutlineStatic approachesStatic approaches““Safe by design” (limiting the language)Safe by design” (limiting the language)Static analysis/type-safe languagesStatic analysis/type-safe languagesDynamic approachesDynamic approachesinterpreters and sandboxesinterpreters and sandboxesDynamic dataflow analysisDynamic dataflow analysisA few examples (and problems)A few examples (and problems)Java, the Exokernel, VMware, SFI, Janus, Interface CompilationJava, the Exokernel, VMware, SFI, Janus, Interface CompilationAs usual…each bullet is the subject of volumes of As usual…each bullet is the subject of volumes of papers…this is just an introduction to the landscapepapers…this is just an introduction to the landscapeContrast With David’s “Req Spec”Contrast With David’s “Req Spec”RS is about verifying a program (or FSM) RS is about verifying a program (or FSM) in the in the abstractabstractSFI is about securing them SFI is about securing them in practicein practiceThe two are complementaryThe two are complementaryEx: “Transitions in FSM cover all possibilities”Ex: “Transitions in FSM cover all possibilities”What is “all”, really?What is “all”, really?Recall: dreaming up desired emergent propertiesRecall: dreaming up desired emergent propertiesCompare: Intel P6 bus protocol Compare: Intel P6 bus protocol verificationverification vs. vs. implementation implementation validationvalidationWhat Is “Safety” in this context?What Is “Safety” in this context?Primary emphasis: prevent buggy/malicious app from Primary emphasis: prevent buggy/malicious app from doing harm doing harm to othersto othersDon’t interfere with other apps directly (read/write their Don’t interfere with other apps directly (read/write their data or files)data or files)Don’t interfere with other apps Don’t interfere with other apps indirectlyindirectly (hog OS (hog OS resources so other apps are denied service)resources so other apps are denied service)Don’t crash or corrupt the OSDon’t crash or corrupt the OSparticularly important, since OS usually is the “trusted arbiter” of particularly important, since OS usually is the “trusted arbiter” of limited resourceslimited resourcesNon-goal: stability of the isolated app.Non-goal: stability of the isolated app.TechniquesTechniquesTwo basic families of techniques:Two basic families of techniques:1. Limit things at runtime1. Limit things at runtime2. Limit things at compile time2. Limit things at compile timeMany schemes use a combination of bothMany schemes use a combination of bothRuntime schemes typically rely on some OS and/or Runtime schemes typically rely on some OS and/or hardware supporthardware supportBackground: “The Thin Red Line”Background: “The Thin Red Line”Separates untrusted Separates untrusted user user space(s)space(s) from trusted from trusted kernel kernel spacespaceKernel manages hardware, shared Kernel manages hardware, shared resources, …resources, …If you can bend the kernel to your If you can bend the kernel to your will, you can do serious damagewill, you can do serious damageTypical implementation: hardware Typical implementation: hardware VM supportVM supportEach user process has its own page Each user process has its own page tables (managed by the kernel)tables (managed by the kernel)Certain addresses mapped to kernel Certain addresses mapped to kernel pagespagesUsercodeKernelcodeProgramming modelUserpageUserpageUserpageKernel pagesUserpageUserpageUserpageCall GatesCall GatesCall gatesCall gates (or call descriptors, or traps, or…) (or call descriptors, or traps, or…)Controlled breach in the thin red lineControlled breach in the thin red lineTypically involve an address space change, which relies on Typically involve an address space change, which relies on VM; so they are slow and expensiveVM; so they are slow and expensiveImplementation often uses exception-handling capability of Implementation often uses exception-handling capability of processorprocessorUser codeKernel codeBackground: Virtual MachinesBackground: Virtual MachinesIn practice, a VM provides a combination of a language In practice, a VM provides a combination of a language execution environment and a “pseudo-OS” runtime execution environment and a “pseudo-OS” runtime systemsystem““guest” VM may virtualize hardware resources differently from guest” VM may virtualize hardware resources differently from “host” OS“host” OSSafety is often not a primary goal of a VMSafety is often not a primary goal of a VMThe “guest” and “host” OS’s may be the same or different The “guest” and “host” OS’s may be the same or different with respect to…with respect to…Machine language/programmer-visible architectureMachine language/programmer-visible architectureVirtualization of resourcesVirtualization of resourcesCommon flavor to various approaches: Control access to Common flavor to various approaches: Control access to “unsafe” language/VM features“unsafe” language/VM featuresVM ExamplesVM ExamplesJava: artificial-machine-in-a-real-machineJava: artificial-machine-in-a-real-machineProvides a language, a runtime, and OS-like abstractions Provides a language, a runtime, and OS-like abstractions (network, filesystems, etc.)(network, filesystems, etc.)Centralized Java
View Full Document
Unlocking...