Validation of Abstract Side-Channel Models for Computer Architectures
| Autor: | Swen Jacobs, Roberto Guanciale, Pablo Buiras, Andreas Lindner, Hamed Nemati |
|---|---|
| Rok vydání: | 2020 |
| Předmět: |
050101 languages & linguistics
Computer science 05 social sciences 02 engineering and technology Symbolic execution Grey relational analysis Model validation Raspberry pi Computer engineering 0202 electrical engineering electronic engineering information engineering 020201 artificial intelligence & image processing 0501 psychology and cognitive sciences Side channel attack Information flow (information theory) Abstraction (linguistics) |
| Zdroj: | Computer Aided Verification ISBN: 9783030532871 CAV (1) |
| DOI: | 10.1007/978-3-030-53288-8_12 |
| Popis: | 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|