BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Micro-Policies: A Framework for Tag-Based Security Monitors  - Ben
 jamin C. Pierce\, University of Pennsylvania
DTSTART:20140911T090000Z
DTEND:20140911T100000Z
UID:TALK53853@talks.cam.ac.uk
CONTACT:Microsoft Research Cambridge Talks Admins
DESCRIPTION:Current cybersecurity practice is inadequate to defend against
  the threats faced by society. A host of vulnerabilities arise from the vi
 olation of known---but not enforced---safety and security policies\, inclu
 ding both high-level programming models and critical invariants of low-lev
 el programs. Unlike safety-critical physical systems (cars\, airplanes\, c
 hemical processing plants)\, present-day computers lack supervising safety
  interlocks to help prevent catastrophic failures.\n\nWe argue that a rich
  and valuable set of low-level MICRO-POLICIES can be enforced at the hardw
 are instruction-set level to provide such safety interlocks with modest pe
 rformance impact. The enforcement of these micro-policies provides more se
 cure and robust macro-scale behavior for computer systems. We describe wor
 k originating in the DARPA CRASH/SAFE project (www.crash-safe.org) to (1) 
 introduce an architecture for ISA-level micro-policy enforcement\; (2) dev
 elop a linguistic framework for formally defining micro-policies\; (3) ide
 ntify and implement a diverse collection of useful micro-policies\; (4) ve
 rify\, through a combination of rigorous testing and formal proof\, that c
 ombinations of hardware and software handlers correctly implement the desi
 red policies and that the policies imply specific high-level safety and se
 curity properties\; and (5) microarchitecture to provide hardware support 
 with low performance overhead and acceptable resource costs. Thus\, emergi
 ng hardware capabilities and advances in formal specification and verifica
 tion combine to enable engineering systems with strong security and safety
  properties. \n
LOCATION:Auditorium\, Microsoft Research Ltd\, 21 Station Road\, Cambridge
 \, CB1 2FB
END:VEVENT
END:VCALENDAR