Paper 2018/329

Symbolic Side-Channel Analysis for Probabilistic Programs

Pasquale Malacaria, MHR. Khouzani, Corina S. Păsăreanu, Quoc-Sang Phan, and Kasper Luckow


In this paper we describe symbolic side-channel analysis techniques for detecting and quantifying information leakage, given in terms of Shannon and Min Entropy. Measuring the precise leakage is challenging due to the randomness and noise often present in program executions and side-channel observations. We account for this noise by introducing additional (symbolic) program inputs which are interpreted probabilistically, using symbolic execution with parameterized model counting. We also explore an approximate sampling approach for increased scalability. In contrast to typical Monte Carlo techniques, our approach works by sampling symbolic paths, representing multiple concrete paths, and uses pruning to accelerate computation and guarantee convergence to the optimal results. The key novelty of our approach is to provide bounds on the leakage that are provably under- and over-approximating the real leakage. We implemented the techniques in the Symbolic PathFinder tool and we demonstrate them on Java programs.

Available format(s)
Publication info
Published elsewhere. Major revision. 31th IEEE Computer Security Foundations Symposium
Side-Channel AttacksQuantitative Information FlowSymbolic ExecutionModel Counting
Contact author(s)
sphan @ us fujitsu com
2018-04-24: revised
2018-04-10: received
See all versions
Short URL
Creative Commons Attribution


      author = {Pasquale Malacaria and MHR.  Khouzani and Corina S.  Păsăreanu and Quoc-Sang Phan and Kasper Luckow},
      title = {Symbolic Side-Channel Analysis for Probabilistic Programs},
      howpublished = {Cryptology ePrint Archive, Paper 2018/329},
      year = {2018},
      note = {\url{}},
      url = {}
Note: In order to protect the privacy of readers, does not use cookies or embedded third party content.