@inproceedings{06254c36c36344789523b07629b78739,
title = "Automated formal analysis of side-channel attacks on probabilistic systems",
abstract = "The security guarantees of even theoretically-secure systems can be undermined by the presence of side channels in their implementations. We present Sch-imp, a probabilistic imperative language for side channel analysis containing primitives for identifying secret and publicly-observable data, and in which resource consumption is modelled at the function level. We provide a semantics for Sch-imp programs in terms of discrete-time Markov chains. Building on this, we propose automated techniques to detect worst-case attack strategies for correctly deducing a program{\textquoteright}s secret information from its outputs and resource consumption, based on verification of partially-observable Markov decision processes. We implement this in a tool and show how it can be used to quantify the severity of worst-case side-channel attacks against a selection of systems, including anonymity networks, covert communication channels and modular arithmetic implementations used for public-key cryptography.",
author = "Chris Novakovic and Dave Parker",
year = "2019",
month = sep,
day = "15",
doi = "10.1007/978-3-030-29959-0_16",
language = "English",
isbn = "978-3-030-29958-3",
series = "Lecture Notes in Computer Science ",
publisher = "Springer",
pages = "319--337",
editor = "Sako, {Kazue } and Steve Schneider and Ryan, {Peter Y. A. }",
booktitle = "Computer Security – ESORICS 2019",
note = "24th European Symposium on Research in Computer Security (ESORICS'19) ; Conference date: 23-09-2019 Through 27-09-2019",
}