CRASH/SAFE: Clean-slate Co-design of a Secure Host Architecture

Add to your list(s) Download to your calendar using vCal

• Catalin Hritcu, University of Pennsylvania
• Thursday 28 March 2013, 10:00-11:00
• Auditorium, Microsoft Research Ltd, 21 Station Road, Cambridge, CB1 2FB.

If you have a question about this talk, please contact Microsoft Research Cambridge Talks Admins.

This event may be recorded and made available internally or externally via http://research.microsoft.com. Microsoft will own the copyright of any recordings made. If you do not wish to have your image/voice recorded please consider this before attending

An important cause for the insecurity of today’s computer systems is security—performance trade-offs made decades ago, which are now deeply embedded in the hardware and software ecosystem, but which are based on assumptions that are now obsolete. We are now living in an era in which security is no longer a side issue, hardware resources are abundant, and formal methods are more practical, so the time is ripe for a redesign.

The CRASH /SAFE project brings together academics (University of Pennsylvania, Harvard, and Northeastern) and industry (BAE Systems and Clozure Associates), with the very ambitious goal of designing a significantly more secure network host from scratch, without any legacy constraints. In this DARPA -funded project, we have undertaken a clean-slate co-design of novel hardware, operating system, programming language, and verification strategy based on modern cost structure and capabilities.

The SAFE hardware and a very thin layer of privileged software (a zero-kernel operating system), provide a run-time system for Breeze, a safe high-level language in which application software is written. This simpler design eliminates some of the traditional sources of complexity in operating systems and makes formal analysis more tractable. Moreover, safety and security are enforced at all layers of the system, not just at the programming language level. The SAFE hardware and runtime system dynamically enforce type and memory safety as well as fine-grained dynamic information-flow control (IFC) and label-based access control (clearance).

I’m going to talk about the CRASH /SAFE project in general and about a couple of specific research problems on which I’ve been working. I will focus on the novel exception handling mechanism in Breeze, which allows IFC violations to be recoverable exceptions as opposed to fatal stop-the-world failures. This work identifies public labels and delayed exceptions as the crucial ingredients for making all errors recoverable in a sound and usable language with fine-grained dynamic IFC . Finally, I’m going to discuss several directions for future research.

This talk is part of the Microsoft Research Cambridge, public talks series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Auditorium, Microsoft Research Ltd, 21 Station Road, Cambridge, CB1 2FB
• Cambridge Centre for Data-Driven Discovery (C2D3)
• Cambridge talks
• Chris Davis' list
• Guy Emerson's list
• Interested Talks
• Microsoft Research Cambridge, public talks
• Optics for the Cloud
• PMRFPS's
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31
• ndk22's list
• ob366-ai4er
• personal list
• rp587

Note that ex-directory lists are not shown.