Seminar 2016-03-30

Speaker: Roberto Guanciale

Bio

Roberto Guanciale is an Assistant Professor at the School of Computer Science in the Department of Theoretical Computer Science. Roberto Guanciale received his PhD in Computer Science and Systems Engineering from IMT Lucca, Italy 2009. He has a MSc and BSc in Computer Science from University of Pisa, Italy, His research interests include System Security, Software Verification and Formal Methods. Currently, he is involved in designing, implementing, modeling and verifying low level execution platforms for embedded systems, such as hypervisor, operating systems and run- time monitors.

Abstract

Caches pose a significant challenge to formal verification, as the cache access pattern of security-critical services may leak secret information. We present a novel attack vector, exposing a low-noise cache storage channel that can be exploited by adapting well-known timing channel analysis techniques. The vector can also be used to attack on various types of security-critical  software such as hypervisors and application security monitors. The attack vector uses virtual aliases with mismatched memory attributes and self-modifying code to misconfigure the memory system, allowing an attacker to place inconsistent copies of the same physical address into the caches and observe which addresses are stored in different levels of cache. We evaluate well-known countermeasures against the new attack vector and propose a verification methodology that allows to formally prove the effectiveness of defense mechanisms on the binary code of the trusted software.

Slides: R.Guanciale.pdf (pdf 631 kB)