License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.FSTTCS.2016.6
URN: urn:nbn:de:0030-drops-68914
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2016/6891/
Go to the corresponding LIPIcs Volume Portal

Bultan, Tevfik

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

pdf-format:
LIPIcs-FSTTCS-2016-6.pdf (0.3 MB)

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.

BibTeX - Entry

@InProceedings{bultan:LIPIcs:2016:6891,
  author =	{Tevfik Bultan},
  title =	{{Side Channel Analysis Using a Model Counting Constraint Solver and Symbolic Execution (Invited Talk)}},
  booktitle =	{36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)},
  pages =	{6:1--6:2},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-027-9},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{65},
  editor =	{Akash Lal and S. Akshay and Saket Saurabh and Sandeep Sen},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2016/6891},
  URN =		{urn:nbn:de:0030-drops-68914},
  doi =		{10.4230/LIPIcs.FSTTCS.2016.6},
  annote =	{Keywords: Side-channels, quantitative information flow, symbolic execution, model counting, constraint solvers}
}

Keywords: Side-channels, quantitative information flow, symbolic execution, model counting, constraint solvers
Collection: 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)
Issue Date: 2016
Date of publication: 10.12.2016

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI