University of Cambridge > > Computer Laboratory Programming Research Group Seminar > Formally Verified Security Micro Policies

Formally Verified Security Micro Policies

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

If you have a question about this talk, please contact Raphael Proust.

Many safety and security policies can be expressed in terms of metadata that is monitored and propagated throughout the execution of a program, with significant examples including information-flow control and memory safety. Recent years have seen a steady increase in computing power, making it feasible to consider computer architectures where more resources are dedicated to security. In this talk, we will present a flexible hardware mechanism designed for enforcing such policies. The mechanism works by marking data with programmable tags that are managed by a software handler through a hardware cache. We will demonstrate how the mechanism can be used to enforce information-flow control (its original motivation), as well as other security policies, and discuss how formal verification can be used to obtain precise guarantees about the behavior of the system.

This talk is part of the Computer Laboratory Programming Research Group Seminar series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


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