2026-08-16T22:47:46Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:4867 2024-03-06T10:35:28Z ddc:004 open_access

Computing Information Flow Using Symbolic Model-Checking Chadha, Rohit Mathur, Umang Schwoon, Stefan Information leakage Min Entropy Shannon Entropy Abstract decision diagrams Program summaries 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Rohit Chadha and Umang Mathur and Stefan Schwoon 2014 Is Part Of LIPIcs, Volume 29, 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSTTCS.2014.505 urn:nbn:de:0030-drops-48676 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2014.505 eng https://creativecommons.org/licenses/by/3.0/legalcode