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

Bultan, Tevfik

doi:10.4230/LIPIcs.FSTTCS.2016.6

File

LIPIcs.FSTTCS.2016.6.pdf

Filesize: 268 kB
2 pages

Document Identifiers

DOI: 10.4230/LIPIcs.FSTTCS.2016.6
URN: urn:nbn:de:0030-drops-68914

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)
https://doi.org/10.4230/LIPIcs.FSTTCS.2016.6

Abstract

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.

Keywords

Side-channels
quantitative information flow
symbolic execution
model counting
constraint solvers

Metrics

Access Statistics
Total Accesses (updated on a weekly basis)

0

PDF Downloads

0

Metadata Views

References

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