Automated formal analysis of side-channel attacks on probabilistic systems

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

Colleges, School and Institutes

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

Details

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
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
Volume11735
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349
NameSecurity and Cryptology
Volume11735

Conference

Conference24th European Symposium on Research in Computer Security (ESORICS'19)
CountryLuxembourg
Period23/09/1927/09/19