Validating Side-Channel Models for Computer Architectures
Date and time: 11 March 2021, 12 pm – 1 pm
Speaker: Roberto Guanciale, KTH Royal Institute of Technology
Title: Validating Side-Channel Models for Computer Architectures
Zoom: https://kth-se.zoom.us/j/64417677978?pwd=RzlDZ3lBMzAwKzFnL2tyWTh4MzBZQT09
Meeting ID: 644 1767 7978
Password: DF2020
Watch the recorded presentation:
Abstract: Information flow analysis that takes into account side channels is a topic of increasing relevance. The existing analyses use models that abstract from many features of modern processors, like caches and pipelining, and their effects on channels that can be accessed by an attacker, like execution time and power consumption. This abstraction makes tractable the analysis of information flow properties by including explicit “observations”, which become available to an attacker when the program is executed and that should overapproximate the information that can be observed on the real system. It turned out that this abstraction is a lie. Attacks that compromise confidentiality via different microarchitectural features and sophisticated side channels continue to emerge: e.g., Spectre, Meltdown, Rowhammer…
The problem is that hardware vendors do not provide the specification of the channels introduced by these low level (and often undocumented) features, making it impossible to trust the security analysis.
In this talk, we introduce a methodology to validate observational models for modern computer architectures.
We combine symbolic execution, relational analysis, and different program generation techniques to generate experiments and validate the models. An experiment consists of a randomly generated program together with two inputs that are observationally equivalent according to the model under the test. Validation is done by checking the indistinguishability of the two inputs on real hardware by executing the program and analyzing the side channel.
Bio: Roberto Guanciale, PhD, is an associate professor at the Division of Theoretical Computer Science at KTH. His research focuses on the design, implementation, and verification of operating systems and execution platforms. Currently, he is investigating methodologies to refine the contracts between hardware and software and new analyses techniques that can verify software security by taking into account microarchitectural optimizations.
Home page: http://www.csc.kth.se/~robertog/