Automated formal analysis of side-channel attacks on probabilistic systems

Chris Novakovic, Dave Parker

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

155 Downloads (Pure)


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.
Original languageEnglish
Title of host publicationComputer Security – ESORICS 2019
Subtitle of host publication24th European Symposium on Research in Computer Security, Luxembourg, September 23–27, 2019, Proceedings, Part I
EditorsKazue Sako, Steve Schneider, Peter Y. A. Ryan
Number of pages19
ISBN (Electronic)978-3-030-29959-0
ISBN (Print)978-3-030-29958-3
Publication statusPublished - 15 Sep 2019
Event24th European Symposium on Research in Computer Security (ESORICS'19) - , Luxembourg
Duration: 23 Sep 201927 Sep 2019

Publication series

NameLecture Notes in Computer Science
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349
NameSecurity and Cryptology


Conference24th European Symposium on Research in Computer Security (ESORICS'19)


Dive into the research topics of 'Automated formal analysis of side-channel attacks on probabilistic systems'. Together they form a unique fingerprint.

Cite this