Symbolic Side-Channel Analysis for Probabilistic Programs

We consider the problem of automatically quantifying information leakage from side-channels of probabilistic programs. The analysis is based on symbolic execution and implemented using Java-pathfinder. To improve scalability, Barvinok counting and symbolic sampling are used. The use of symbolic sampling allows proving strong guarantees about the convergence of the estimated leakage to the real leakage. (joint work with MHR. Khouzani, Corina Pasareanu, Quoc-Sang Phan, Kasper Luckow)

Pasquale Malacaria is a professor of Computer Science at Queen Mary University of London. His main focus of research is information theory, game theory, optimization, verification and their applications to computer security. On the practical side, he has worked on automated security analysis for the Linux Kernel, open SSL and side-channels in Java programs using CBMC, Java-pathfinder and #SAT solvers.