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 - Benj
 amin C. Pierce\, University of Pennsylvania
DTSTART:20140910T120000Z
DTEND:20140910T130000Z
UID:TALK53852@talks.cam.ac.uk
CONTACT:Jonathan Hayman
DESCRIPTION:Current cybersecurity practice is inadequate to defend against
  the threats\nfaced by society.  A host of vulnerabilities arise from the 
 violation of\nknown---but not enforced---safety and security policies\, in
 cluding both\nhigh-level programming models and critical invariants of low
 -level programs.\nUnlike safety-critical physical systems (cars\, airplane
 s\, chemical\nprocessing plants)\, present-day computers lack supervising 
 safety interlocks\nto help prevent catastrophic failures.\n\nWe argue that
  a rich and valuable set of low-level MICRO-POLICIES can be\nenforced at t
 he hardware instruction-set level to provide such safety\ninterlocks with 
 modest performance impact.  The enforcement of these\nmicro-policies provi
 des more secure and robust macro-scale behavior for\ncomputer systems.  We
  describe work originating in the DARPA CRASH/SAFE\nproject (www.crash-saf
 e.org) to (1) introduce an architecture for ISA-level\nmicro-policy enforc
 ement\; (2) develop a linguistic framework for formally\ndefining micro-po
 licies\; (3) identify and implement a diverse collection of\nuseful micro-
 policies\; (4) verify\, through a combination of rigorous testing\nand for
 mal proof\, that combinations of hardware and software handlers\ncorrectly
  implement the desired policies and that the policies imply\nspecific high
 -level safety and security properties\; and (5)\nmicroarchitecture to prov
 ide hardware support with low performance overhead\nand acceptable resourc
 e costs.  Thus\, emerging hardware capabilities and advances \nin formal s
 pecification and verification combine to enable engineering \nsystems with
  strong security and safety properties.\n\nBIO: Benjamin Pierce is Henry S
 alvatori Professor of Computer and Information Science at the University o
 f Pennsylvania and a Fellow of the ACM. His research interests include pro
 gramming languages\, type systems\, language-based security\, computer-ass
 isted formal verification\, differential privacy\, and synchronization tec
 hnologies. He is the author of the widely used graduate textbooks Types an
 d Programming Languages and Software Foundations. He has served as co-Edit
 or in Chief of the Journal of Functional Programming\, as Managing Editor 
 for Logical Methods in Computer Science\, and as editorial board member of
  Mathematical Structures in Computer Science\, Formal Aspects of Computing
 \, and ACM Transactions on Programming Languages and Systems. He is also t
 he lead designer of the popular Unison file synchronizer.
LOCATION:Room FW26\, Computer Laboratory\, William Gates Building
END:VEVENT
END:VCALENDAR