CISPA
Browse
cispa_all_3211.pdf (807.54 kB)

Validation of Abstract Side-Channel Models for Computer Architectures

Download (807.54 kB)
conference contribution
posted on 2023-11-29, 18:13 authored by Hamed Nemati, Pablo Buiras, Andreas Lindner, Roberto Guanciale, Swen JacobsSwen Jacobs
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.

History

Preferred Citation

Hamed Nemati, Pablo Buiras, Andreas Lindner, Roberto Guanciale and Swen Jacobs. Validation of Abstract Side-Channel Models for Computer Architectures. In: Computer Aided Verification (CAV). 2020.

Primary Research Area

  • Reliable Security Guarantees

Name of Conference

Computer Aided Verification (CAV)

Legacy Posted Date

2020-12-01

Open Access Type

  • Unknown

BibTeX

@inproceedings{cispa_all_3211, title = "Validation of Abstract Side-Channel Models for Computer Architectures", author = "Nemati, Hamed and Buiras, Pablo and Lindner, Andreas and Guanciale, Roberto and Jacobs, Swen", booktitle="{Computer Aided Verification (CAV)}", year="2020", }

Usage metrics

    Categories

    No categories selected

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC