[NP19] Chris Novakovic and David Parker. Automated Formal Analysis of Side-Channel Attacks on Probabilistic Systems. In Proc. 24th European Symposium on Research in Computer Security (ESORICS'19), volume 11735 of LNCS, pages 319-337, Springer. September 2019. [pdf] [bib] [Develops techniques to identify side-channel attacks in probabilistic systems, building on PRISM-pomdps.]
Downloads:  pdf pdf (520 KB)  bib bib
Notes: Supporting material (tool, source code, examples) is at https://www.cs.bham.ac.uk/research/projects/schimp/.
The original publication is available at link.springer.com.
Abstract. The security guarantees of even theoretically-secure systems can be undermined by the presence of side channels in their implementations. We present SCHIMP, 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 SCHIMP 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.