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
• Wednesday 10 September 2014, 13:00-14:00
• FW26.

If you have a question about this talk, please contact Peter Sewell.

Note in FW26

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.

BIO : Benjamin Pierce is Henry Salvatori Professor of Computer and Information Science at the University of Pennsylvania and a Fellow of the ACM . His research interests include programming languages, type systems, language-based security, computer-assisted formal verification, differential privacy, and synchronization technologies. He is the author of the widely used graduate textbooks Types and Programming Languages and Software Foundations. He has served as co-Editor 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 the lead designer of the popular Unison file synchronizer.

This talk is part of the REMS lunch series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Department of Computer Science and Technology talks and seminars
• FW26
• Interested Talks
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31

Note that ex-directory lists are not shown.