• Classified by Research Topic • Sorted by Date • Classified by Publication Type •
Scalable Approximation of Quantitative Information Flow in Programs.
Fabrizio Biondi, Michael Enescu, Annelie Heuser, Axel Legay, Kuldeep S. Meel and Jean Quilbeuf.
In Proceedings of International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI), January 2018.
Quantitative information flow measurement techniques have been proven to be successful in detecting leakage of confidential information from programs. Modern approaches are based on formal methods, relying on program analysis to produce a SAT formula representing the program's behavior, and model counting to measure the possible information flow. However, while program analysis scales to large codebases like the OpenSSL project, the formulas produced are too complex for analysis with precise model counting. In this paper we use the approximate model counter ApproxMC2 to quantify information flow. We show that ApproxMC2 is able to provide a large performance increase for a very small loss of precision, allowing the analysis of SAT formulas produced from complex code. We call the resulting technique ApproxFlow and test it on a large set of benchmarks against the state of the art. Finally, we show that ApproxFlow can evaluate the leakage incurred by the Heartbleed OpenSSL bug, contrarily to the state of the art.
@inproceedings{BEHLMQ18,
title={Scalable Approximation of Quantitative Information Flow in Programs},
author={Biondi, Fabrizio and Enescu, Michael and Heuser, Annelie and Legay, Axel and Meel, Kuldeep S. and Quilbeuf, Jean},
booktitle=VMCAI,
year={2018},
month=jan,
bib2html_rescat={Software Engineering},
abstract={Quantitative information flow measurement techniques have
been proven to be successful in detecting leakage of confidential information
from programs. Modern approaches are based on formal methods,
relying on program analysis to produce a SAT formula representing the
program's behavior, and model counting to measure the possible information
flow. However, while program analysis scales to large codebases
like the OpenSSL project, the formulas produced are too complex for
analysis with precise model counting. In this paper we use the approximate
model counter ApproxMC2 to quantify information flow. We show
that ApproxMC2 is able to provide a large performance increase for a very
small loss of precision, allowing the analysis of SAT formulas produced
from complex code. We call the resulting technique ApproxFlow and test it
on a large set of benchmarks against the state of the art. Finally, we show
that ApproxFlow can evaluate the leakage incurred by the Heartbleed
OpenSSL bug, contrarily to the state of the art.},
bib2html_dl_pdf={../Papers/vmcai18.pdf},
bib2html_pubtype={Refereed Conference},
}
Generated by bib2html.pl (written by Patrick Riley with layout from Sanjit A. Seshia ) on Sun Apr 14, 2024 11:15:51