Observational models make tractable the analysis of information flow properties by providing an abstraction of side channels. Scam-V, Side-channel abstract model validation, is a tool for the validation of observational models for modern computer architectures. We combine symbolic execution, relational analysis, and different program generation techniques to generate experiments and validate the side-channel models. Validation of models is done by checking indistinguishability of the two inputs on real hardware by executing the program and analyzing the side channel.

Researchers

Profile picture
Roberto Guanciale
Associate Professor, KTH
Profile picture
Pablo Buiras
Researcher, KTH
Profile picture
Andreas Lindner
PhD student, KTH
Profile picture
Hamed Nemati
Research Group Leader, CISPA
Profile picture
Tiziano Marinaro
PhD Student, CISPA