Micro-Policies: A Framework for Tag-Based Security Monitors

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

• Benjamin C. Pierce, University of Pennsylvania
• Thursday 11 September 2014, 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

Current cybersecurity practice is inadequate to defend against the threats faced by society. A host of vulnerabilities arise from the violation of known—-but not enforced—-safety and security policies, including both high-level programming models and critical invariants of low-level programs. Unlike safety-critical physical systems (cars, airplanes, chemical processing plants), present-day computers lack supervising safety interlocks to help prevent catastrophic failures.

We argue that a rich and valuable set of low-level MICRO -POLICIES can be enforced at the hardware instruction-set level to provide such safety interlocks with modest performance impact. The enforcement of these micro-policies provides more secure and robust macro-scale behavior for computer systems. We describe work originating in the DARPA CRASH /SAFE project (www.crash-safe.org) to (1) introduce an architecture for ISA -level micro-policy enforcement; (2) develop a linguistic framework for formally defining micro-policies; (3) identify and implement a diverse collection of useful micro-policies; (4) verify, through a combination of rigorous testing and formal proof, that combinations of hardware and software handlers correctly implement the desired policies and that the policies imply specific high-level safety and security properties; and (5) microarchitecture to provide hardware support with low performance overhead and acceptable resource costs. Thus, emerging hardware capabilities and advances in formal specification and verification combine to enable engineering systems with strong security and safety properties.

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.