Formally Verified Security Micro Policies

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

• Arthur Azevedo de Amorim (Upenn)
• Friday 06 June 2014, 14:00-15:00
• FW26, Computer Laboratory, William Gates Building.

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.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Computer Laboratory Programming Research Group Seminar
• Department of Computer Science and Technology talks and seminars
• FW26, Computer Laboratory, William Gates Building
• Interested Talks
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31

Note that ex-directory lists are not shown.