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:TALK54200@talks.cam.ac.uk
CONTACT:Peter Sewell
DESCRIPTION:Current cybersecurity practice is inadequate to defend against
  the\nthreats faced by society. A host of vulnerabilities arise from the\n
 violation of known—-but not enforced—-safety and security policies\,\n
 including both high-level programming models and critical invariants of\nl
 ow-level programs. Unlike safety-critical physical systems (cars\,\nairpla
 nes\, chemical processing plants)\, present-day computers lack\nsupervisin
 g safety interlocks to help prevent catastrophic failures.\n\nWe argue tha
 t a rich and valuable set of low-level MICRO -POLICIES can\nbe enforced at
  the hardware instruction-set level to provide such safety\ninterlocks wit
 h modest performance impact. The enforcement of these\nmicro-policies prov
 ides more secure and robust macro-scale behavior for\ncomputer systems. We
  describe work originating in the DARPA CRASH /SAFE\nproject (www.crash-sa
 fe.org) to (1) introduce an architecture for ISA\n-level micro-policy enfo
 rcement\; (2) develop a linguistic framework for\nformally defining micro-
 policies\; (3) identify and implement a diverse\ncollection of useful micr
 o-policies\; (4) verify\, through a combination\nof rigorous testing and f
 ormal proof\, that combinations of hardware and\nsoftware handlers correct
 ly implement the desired policies and that the\npolicies imply specific hi
 gh-level safety and security properties\; and\n(5) microarchitecture to pr
 ovide hardware support with low performance\noverhead and acceptable resou
 rce costs. Thus\, emerging hardware\ncapabilities and advances in formal s
 pecification and verification\ncombine to enable engineering systems with 
 strong security and safety\nproperties.\n\nBIO : Benjamin Pierce is Henry 
 Salvatori Professor of Computer and\nInformation Science at the University
  of Pennsylvania and a Fellow of\nthe ACM . His research interests include
  programming languages\, type\nsystems\, language-based security\, compute
 r-assisted formal verification\,\ndifferential privacy\, and synchronizati
 on technologies. He is the author\nof the widely used graduate textbooks T
 ypes and Programming Languages\nand Software Foundations. He has served as
  co-Editor in Chief of the\nJournal of Functional Programming\, as Managin
 g Editor for Logical\nMethods in Computer Science\, and as editorial board
  member of\nMathematical Structures in Computer Science\, Formal Aspects o
 f\nComputing\, and ACM Transactions on Programming Languages and Systems. 
 He\nis also the lead designer of the popular Unison file synchronizer.
LOCATION:FW26
END:VEVENT
END:VCALENDAR