The beta version of DROPS 2 is now publicly available! Check this page out at DROPS 2 now!


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.2014.505
URN: urn:nbn:de:0030-drops-48676
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2014/4867/
Go to the corresponding LIPIcs Volume Portal

Chadha, Rohit ; Mathur, Umang ; Schwoon, Stefan

Computing Information Flow Using Symbolic Model-Checking

pdf-format:
43.pdf (0.6 MB)

Abstract

Several measures have been proposed in literature for quantifying the information leaked by the public outputs of a program with secret inputs. We consider the problem of computing information leaked by a deterministic or probabilistic program when the measure of information is based on (a) min-entropy and (b) Shannon entropy. The key challenge in computing these measures is that we need the total number of possible outputs and, for each possible output, the number of inputs that lead to it. A direct computation of these quantities is infeasible because of the state-explosion problem. We therefore propose symbolic algorithms based on binary decision diagrams (BDDs). The advantage of our approach is that these symbolic algorithms can be easily implemented in any BDD-based model-checking tool that checks for reachability in deterministic non-recursive programs by computing program summaries. We demonstrate the validity of our approach by implementing these algorithms in a tool Moped-QLeak, which is built upon Moped, a model checker for Boolean programs. Finally, we show how this symbolic approach extends to probabilistic programs.

BibTeX - Entry

@InProceedings{chadha_et_al:LIPIcs:2014:4867,
  author =	{Rohit Chadha and Umang Mathur and Stefan Schwoon},
  title =	{{Computing Information Flow Using Symbolic Model-Checking}},
  booktitle =	{34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)},
  pages =	{505--516},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-77-4},
  ISSN =	{1868-8969},
  year =	{2014},
  volume =	{29},
  editor =	{Venkatesh Raman and S. P. Suresh},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2014/4867},
  URN =		{urn:nbn:de:0030-drops-48676},
  doi =		{10.4230/LIPIcs.FSTTCS.2014.505},
  annote =	{Keywords: Information leakage, Min Entropy, Shannon Entropy, Abstract decision diagrams, Program summaries}
}

Keywords: Information leakage, Min Entropy, Shannon Entropy, Abstract decision diagrams, Program summaries
Collection: 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)
Issue Date: 2014
Date of publication: 12.12.2014

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