COOKIES: By using this website you agree that we can place Google Analytics Cookies on your device for performance monitoring. |
University of Cambridge > Talks.cam > Logic and Semantics Seminar (Computer Laboratory) > Micro-Policies: A Framework for Tag-Based Security Monitors
Micro-Policies: A Framework for Tag-Based Security MonitorsAdd to your list(s) Download to your calendar using vCal
If you have a question about this talk, please contact Jonathan Hayman. 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 Logic and Semantics Seminar (Computer Laboratory) series. This talk is included in these lists:
Note that ex-directory lists are not shown. |
Other listsCambridge Energy Seminars Horizon Forum: The Cell-Materials Interface Summer Hebrew Ulpan CMS Events women@CL Coffee and CakeOther talksChanging understandings of the human fetus over five decades of legal abortion Adaptation in log-concave density estimation St Catharine’s Political Economy Seminar - ‘Bank Credit Rating Changes, Capital Structure Adjustments and Lending’ by Claudia Girardone Science Makers: multispectral imaging with Raspberry Pi Trees as keys, ladders, maps: a revisionist history of early systematic trees |