Document Open Access Logo

Computing Information Flow Using Symbolic Model-Checking

Authors Rohit Chadha, Umang Mathur, Stefan Schwoon

Thumbnail PDF


  • Filesize: 0.55 MB
  • 12 pages

Document Identifiers

Author Details

Rohit Chadha
Umang Mathur
Stefan Schwoon

Cite AsGet BibTex

Rohit Chadha, Umang Mathur, and Stefan Schwoon. Computing Information Flow Using Symbolic Model-Checking. In 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 29, pp. 505-516, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2014)


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.
  • Information leakage
  • Min Entropy
  • Shannon Entropy
  • Abstract decision diagrams
  • Program summaries


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads
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