2011 · 20 citations · 13 references
EngineeringSecure Host ArchitectureInformation SecuritySafety ScienceFormal VerificationSocial SciencesHardware SecuritySystems EngineeringTrusted Execution EnvironmentSecure ComputingBasic Architectural ChoicesClean-slate DesignDesignOperating System SecuritySecure By DesignData SecurityArchitectural DesignSafety EngineeringSoftware SecurityOperating SystemsFormal MethodsSafety SystemFunctional SafetySystem SoftwareSafe Platform
Safe is a clean-slate design for a secure host architecture. It integrates advances in programming languages, operating systems, and hardware and incorporates formal methods at every step. Though the project is still at an early stage, we have assembled a set of basic architectural choices that we believe will yield a high-assurance system. We sketch the current state of the design and discuss several of these choices.
13
A lattice model of secure information flow
Dorothy E. Denning · Communications of the ACM · 1976 · 1.9K citations · Full text
Gerwin Klein, Kevin Elphinstone, Gernot Heiser et al. · 2009 · 1.5K citations
Engineering, Hardware Verification Language, Verification +18
Formal verification of a realistic compiler
Xavier Leroy · Communications of the ACM · 2009 · 1.1K citations · Full text