  Observational models make tractable the analysis of information flow
properties by providing an abstraction of side channels. We introduce a
methodology and a tool, Scam-V, 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 indistinguishability of the two
inputs on real hardware by executing the program and analyzing the side
channel. We have evaluated our framework by validating models that abstract the
data-cache side channel of a Raspberry Pi 3 board with a processor implementing
the ARMv8-A architecture. Our results show that Scam-V can identify bugs in the
implementation of the models and generate test programs which invalidate the
models due to hidden microarchitectural behavior.
