Validation of abstract side-channel models for computer architectures

DOI10.1007/978-3-030-53288-8_12MaRDI QIDQ2225102zbMATH OpenOpenAlexFDO

Authors Hamed Nemati, Pablo Buiras, A. Lindner, Roberto Guanciale, Swen Jacobs

Publication date 4 February 2021

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://arxiv.org/abs/2005.05254

zbMATH Keywords

information flow securitymicroarchitecturesmodel validationside channelstesting

Mathematics Subject Classification ID

Mathematical problems of computer architecture (68M07) Computer security (68M25) Specification and verification (program logics, model checking, etc.) (68Q60)

Abstract: 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.

Recommendations

• Efficient Information-Flow Verification Under Speculative Execution
• From operational models to information theory; side channels in pGCL with Isabelle
• Formal verification of side-channel countermeasures using self-composition
• Information Security and Cryptology - ICISC 2005
• Formal verification of integrity-preserving countermeasures against cache storage side-channels

Cited in

(2)

• Formal verification of integrity-preserving countermeasures against cache storage side-channels
• Hoare-style logic for unstructured programs

This page was built for publication: Validation of abstract side-channel models for computer architectures

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2225102)