University of Cambridge > > Microsoft Research Cambridge, public talks > Micro-Policies: A Framework for Tag-Based Security Monitors

Micro-Policies: A Framework for Tag-Based Security Monitors

Add to your list(s) Download to your calendar using vCal

If you have a question about this talk, please contact Microsoft Research Cambridge Talks Admins.

This event may be recorded and made available internally or externally via Microsoft will own the copyright of any recordings made. If you do not wish to have your image/voice recorded please consider this before attending

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 ( 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.

This talk is part of the Microsoft Research Cambridge, public talks series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


© 2006-2023, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity