Automated formal analysis of side-channel attacks on probabilistic systems

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Standard

Automated formal analysis of side-channel attacks on probabilistic systems. / Novakovic, Chris; Parker, Dave.

Computer Security – ESORICS 2019: 24th European Symposium on Research in Computer Security, Luxembourg, September 23–27, 2019, Proceedings, Part I. ed. / Kazue Sako; Steve Schneider; Peter Y. A. Ryan. Springer, 2019. p. 319-337 (Lecture Notes in Computer Science ; Vol. 11735), (Security and Cryptology; Vol. 11735).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Harvard

Novakovic, C & Parker, D 2019, Automated formal analysis of side-channel attacks on probabilistic systems. in K Sako, S Schneider & PYA Ryan (eds), Computer Security – ESORICS 2019: 24th European Symposium on Research in Computer Security, Luxembourg, September 23–27, 2019, Proceedings, Part I. Lecture Notes in Computer Science , vol. 11735, Security and Cryptology, vol. 11735, Springer, pp. 319-337, 24th European Symposium on Research in Computer Security (ESORICS'19), Luxembourg, 23/09/19. https://doi.org/10.1007/978-3-030-29959-0_16

APA

Novakovic, C., & Parker, D. (2019). Automated formal analysis of side-channel attacks on probabilistic systems. In K. Sako, S. Schneider, & P. Y. A. Ryan (Eds.), Computer Security – ESORICS 2019: 24th European Symposium on Research in Computer Security, Luxembourg, September 23–27, 2019, Proceedings, Part I (pp. 319-337). (Lecture Notes in Computer Science ; Vol. 11735), (Security and Cryptology; Vol. 11735). Springer. https://doi.org/10.1007/978-3-030-29959-0_16

Vancouver

Novakovic C, Parker D. Automated formal analysis of side-channel attacks on probabilistic systems. In Sako K, Schneider S, Ryan PYA, editors, Computer Security – ESORICS 2019: 24th European Symposium on Research in Computer Security, Luxembourg, September 23–27, 2019, Proceedings, Part I. Springer. 2019. p. 319-337. (Lecture Notes in Computer Science ). (Security and Cryptology). https://doi.org/10.1007/978-3-030-29959-0_16

Author

Novakovic, Chris ; Parker, Dave. / Automated formal analysis of side-channel attacks on probabilistic systems. Computer Security – ESORICS 2019: 24th European Symposium on Research in Computer Security, Luxembourg, September 23–27, 2019, Proceedings, Part I. editor / Kazue Sako ; Steve Schneider ; Peter Y. A. Ryan. Springer, 2019. pp. 319-337 (Lecture Notes in Computer Science ). (Security and Cryptology).

Bibtex

@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",

}

RIS

TY - GEN

T1 - Automated formal analysis of side-channel attacks on probabilistic systems

AU - Novakovic, Chris

AU - Parker, Dave

PY - 2019/9/15

Y1 - 2019/9/15

N2 - 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’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.

AB - 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’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.

U2 - 10.1007/978-3-030-29959-0_16

DO - 10.1007/978-3-030-29959-0_16

M3 - Conference contribution

SN - 978-3-030-29958-3

T3 - Lecture Notes in Computer Science

SP - 319

EP - 337

BT - Computer Security – ESORICS 2019

A2 - Sako, Kazue

A2 - Schneider, Steve

A2 - Ryan, Peter Y. A.

PB - Springer

T2 - 24th European Symposium on Research in Computer Security (ESORICS'19)

Y2 - 23 September 2019 through 27 September 2019

ER -