Selected publications at LSV

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.

@inproceedings{CMS-fsttcs14,
   address = {New~Dehli, India},
   author = {Chadha, Rohit and Mathur, Umang and Schwoon, Stefan},
   booktitle = {{P}roceedings of the 34th {C}onference on {F}oundations of {S}oftware {T}echnology and {T}heoretical {C}omputer {S}cience ({FSTTCS}'14)},
   DOI = {10.4230/LIPIcs.FSTTCS.2014.505},
   editor = {Raman, Venkatesh and Suresh, S.~P.},
   month = dec,
   pages = {505-516},
   publisher = {Leibniz-Zentrum f{\"u}r Informatik},
   series = {Leibniz International Proceedings in Informatics},
   title = {Computing Information Flow Using Symbolic Model-Checking},
   url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CMS-fsttcs14.pdf},
   volume = {29},
   year = {2014},
}

About LSV