HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation
Preprints, Working Papers, ...

Scalable Approximation of Quantitative Information Flow in Programs

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.
Document type :
Preprints, Working Papers, ...
Complete list of metadata

Cited literature [30 references]  Display  Hide  Download

Contributor : Fabrizio Biondi Connect in order to contact the contributor
Submitted on : Monday, November 6, 2017 - 9:57:49 AM
Last modification on : Monday, April 4, 2022 - 9:28:22 AM
Long-term archiving on: : Wednesday, February 7, 2018 - 1:28:56 PM


Files produced by the author(s)


  • HAL Id : hal-01629131, version 1


Fabrizio Biondi, Michael Enescu, Annelie Heuser, Axel Legay, Kuldeep Meel, et al.. Scalable Approximation of Quantitative Information Flow in Programs. 2017. ⟨hal-01629131⟩



Record views


Files downloads