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:TALK54224@talks.cam.ac.uk
CONTACT:Laurent Simon
DESCRIPTION:*Abstract:*\nCurrent cybersecurity practice is inadequate to d
 efend against the\nthreats faced by society. A host of vulnerabilities ari
 se from the\nviolation of known—-but not enforced—-safety and security
  policies\,\nincluding both high-level programming models and critical inv
 ariants of\nlow-level programs. Unlike safety-critical physical systems (c
 ars\,\nairplanes\, chemical processing plants)\, present-day computers lac
 k\nsupervising safety interlocks to help prevent catastrophic failures.\n\
 nWe argue that a rich and valuable set of low-level MICRO -POLICIES can\nb
 e enforced at the hardware instruction-set level to provide such safety\ni
 nterlocks with modest performance impact. The enforcement of these\nmicro-
 policies provides more secure and robust macro-scale behavior for\ncompute
 r systems. We describe work originating in the DARPA CRASH /SAFE\nproject 
 (www.crash-safe.org) to (1) introduce an architecture for ISA\n-level micr
 o-policy enforcement\; (2) develop a linguistic framework for\nformally de
 fining micro-policies\; (3) identify and implement a diverse\ncollection o
 f useful micro-policies\; (4) verify\, through a combination\nof rigorous 
 testing and formal proof\, that combinations of hardware and\nsoftware han
 dlers correctly implement the desired policies and that the\npolicies impl
 y specific high-level safety and security properties\; and\n(5) microarchi
 tecture to provide hardware support with low performance\noverhead and acc
 eptable resource costs. Thus\, emerging hardware\ncapabilities and advance
 s in formal specification and verification\ncombine to enable engineering 
 systems with strong security and safety\nproperties.\n\n*Bio:* \nBenjamin 
 Pierce is Henry Salvatori Professor of Computer and\nInformation Science a
 t the University of Pennsylvania and a Fellow of\nthe ACM . His research i
 nterests include programming languages\, type\nsystems\, language-based se
 curity\, computer-assisted formal verification\,\ndifferential privacy\, a
 nd synchronization technologies. He is the author\nof the widely used grad
 uate textbooks Types and Programming Languages\nand Software Foundations. 
 He has served as co-Editor in Chief of the\nJournal of Functional Programm
 ing\, as Managing Editor for Logical\nMethods in Computer Science\, and as
  editorial board member of\nMathematical Structures in Computer Science\, 
 Formal Aspects of\nComputing\, and ACM Transactions on Programming Languag
 es and Systems. He\nis also the lead designer of the popular Unison file s
 ynchronizer.\n
LOCATION:FW26\, Computer Laboratory\, William Gates Building
END:VEVENT
END:VCALENDAR