BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Cache Storage Channels: Alias-Driven Attacks - Roberto Guanciale\,
  KTH
DTSTART:20160208T130000Z
DTEND:20160208T140000Z
UID:TALK64373@talks.cam.ac.uk
CONTACT:Peter Sewell
DESCRIPTION: Caches pose a significant challenge to formal verification\,\
 nas the cache access pattern of security-critical services may leak secret
  information.\nWe present a novel attack vector\, exposing a low-noise cac
 he storage channel that can be exploited by\nadapting well-known timing ch
 annel analysis techniques. The vector can\nalso be used to attack on vario
 us types of security-critical  software such as\nhypervisors and applicati
 on security monitors.\nThe attack vector uses virtual aliases with mismatc
 hed memory attributes and self-modifying code to\nmisconfigure the memory 
 system\, allowing an attacker to place inconsistent\ncopies of the same ph
 ysical address into the caches and observe\nwhich addresses are stored in 
 different levels of cache.\nWe evaluate well-known countermeasures against
  the new attack vector and\npropose a verification methodology that allows
  to formally prove the effectiveness of defense mechanisms on the binary c
 ode of the trusted software.
LOCATION:FW26
END:VEVENT
END:VCALENDAR