Side Channel Analysis Using a Model Counting Constraint Solver and Symbolic Execution (Invited Talk)

Author Tevfik Bultan

Thumbnail PDF


  • Filesize: 268 kB
  • 2 pages

Document Identifiers

Author Details

Tevfik Bultan

Cite AsGet BibTex

Tevfik Bultan. Side Channel Analysis Using a Model Counting Constraint Solver and Symbolic Execution (Invited Talk). In 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 65, pp. 6:1-6:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)


A crucial problem in software security is the detection of side-channels. Information gained by observing non-functional properties of program executions (such as execution time or memory usage) can enable attackers to infer secret information (such as a password). In this talk, I will discuss how symbolic execution, combined with a model counting constraint solver, can be used for quantifying side-channel leakage in Java programs. In addition to computing information leakage for a single run of a program, I will also discuss computation of information leakage for multiple runs for a type of side channels called segmented oracles. In segmented oracles, the attacker is able to explore each segment of a secret (for example each character of a password) independently. For segmented oracles, it is possible to compute information leakage for multiple runs using only the path constraints generated from a single run symbolic execution. These results have been implemented as an extension to the symbolic execution tool Symbolic Path Finder (SPF) using the SMT solver Z3 and two model counting constraint solvers LattE and ABC.
  • Side-channels
  • quantitative information flow
  • symbolic execution
  • model counting
  • constraint solvers


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads


  1. Abdulbaki Aydin, Lucas Bang, and Tevfik Bultan. Automata-based model counting for string constraints. In Proceedings of the 27th International Conference on Computer Aided Verification (CAV), pages 255-272, 2015. Google Scholar
  2. Michael Backes, Boris Kopf, and Andrey Rybalchenko. Automatic Discovery and Quantification of Information Leaks. In Proceedings of the 2009 30th IEEE Symposium on Security and Privacy, SP'09, pages 141-153, Washington, DC, USA, 2009. IEEE Computer Society. Google Scholar
  3. Lucas Bang, Abdulbaki Aydin, Quoc-Sang Phan, Corina S. Pasareanu, and Tevfik Bultan. String analysis for side channels with segmented oracles. In Proceedings of the 24th ACM SIGSOFT International Symposium on the Foundations of Software Engineering (FSE), 2016. Google Scholar
  4. Leonardo Mendonça de Moura and Nikolaj Bjørner. Z3: an efficient SMT solver. In Proceedings of the 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29-April 6, 2008, pages 337-340, 2008. Google Scholar
  5. Boris Köpf and David A. Basin. An information-theoretic model for adaptive side-channel attacks. In Proceedings of the 2007 ACM Conference on Computer and Communications Security, CCS 2007, Alexandria, Virginia, USA, October 28-31, 2007, pages 286-296, 2007. Google Scholar
  6. Jesús A. De Loera, Raymond Hemmecke, Jeremiah Tauzer, and Ruriko Yoshida. Effective lattice point counting in rational convex polytopes. Journal of Symbolic Computation, 38(4):1273-1302, 2004. Symbolic Computation in Algebra and Geometry. Google Scholar
  7. Corina S. Păsăreanu, Quoc-Sang Phan, and Pasquale Malacaria. Multi-run side-channel analysis using Symbolic Execution and Max-SMT. In Proceedings of the 2016 IEEE 29th Computer Security Foundations Symposium, CSF'16, Washington, DC, USA, 2016. IEEE Computer Society. Google Scholar
  8. Corina S. Păsăreanu, Willem Visser, David Bushnell, Jaco Geldenhuys, Peter Mehlitz, and Neha Rungta. Symbolic PathFinder: integrating symbolic execution with model checking for Java bytecode analysis. Automated Software Engineering, pages 1-35, 2013. Google Scholar
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail