BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Formally Verified Security Micro Policies - Arthur Azevedo de Amor
 im (Upenn)
DTSTART:20140606T130000Z
DTEND:20140606T140000Z
UID:TALK52893@talks.cam.ac.uk
CONTACT:Raphael Proust
DESCRIPTION:Many safety and security policies can be expressed in terms of
 \nmetadata that is monitored and propagated throughout the execution of\na
  program\, with significant examples including information-flow\ncontrol a
 nd memory safety. Recent years have seen a steady\nincrease in computing p
 ower\, making it feasible to consider computer\narchitectures where more r
 esources are dedicated to security. In this\ntalk\, we will present a flex
 ible hardware mechanism designed for\nenforcing such policies. The mechani
 sm works by marking data with\nprogrammable tags that are managed by a sof
 tware handler through a\nhardware cache. We will demonstrate how the mecha
 nism can be used to\nenforce information-flow control (its original motiva
 tion)\, as well as\nother security policies\, and discuss how formal verif
 ication can be\nused to obtain precise guarantees about the behavior of th
 e system.
LOCATION:FW26\, Computer Laboratory\, William Gates Building
END:VEVENT
END:VCALENDAR