Speeding Up SMT-Based Quantitative Program Analysis

Daniel J. Fremont and Sanjit A. Seshia. Speeding Up SMT-Based Quantitative Program Analysis. In In 12th International Workshop on Satisfiability Modulo Theories (SMT), pp. 3–13, July 2014.

Download

[pdf] 

Abstract

Quantitative program analysis involves computing numerical quantities about individual or collections of program executions. An example of such a computation is quantitative information flow analysis, where one estimates the amount of information leaked about secret data through a program'soutput channels. Such information can be quantified in several ways, including channel capacity and (Shannon) entropy. In this paper, we formalize a class of quantitative analysis problems defined over a weighted control flow graph of a loop-free program. These problems can be solved using a combination of path enumeration, SMT solving, and model counting. However, existing methods can only handle very small programs, primarily because the number of execution paths can be exponential in the program size. We show how path explosion can be mitigated in some practical cases by taking advantage of special branching structure and by novel algorithm design. We demonstrate our techniques by computing the channel capacities of the timing side-channels of two programs with extremely large numbers of paths.

BibTeX

@inproceedings{fremont-smt14,
  author    = {Daniel J. Fremont and Sanjit A. Seshia},
  title     = {Speeding Up SMT-Based Quantitative Program Analysis},
 booktitle = {In 12th International Workshop on Satisfiability Modulo Theories (SMT)},
 month = "July",
 year = {2014},
 pages = {3--13},
 abstract = {Quantitative program analysis involves computing numerical quantities about individual or collections 
of program executions. An example of such a computation is quantitative information flow 
analysis, where one estimates the amount of information leaked about secret data through a program's
output channels. Such information can be quantified in several ways, including channel capacity and 
(Shannon) entropy. In this paper, we formalize a class of quantitative analysis problems defined over 
a weighted control flow graph of a loop-free program. These problems can be solved using a combination 
of path enumeration, SMT solving, and model counting. However, existing methods can only 
handle very small programs, primarily because the number of execution paths can be exponential in 
the program size. We show how path explosion can be mitigated in some practical cases by taking advantage 
of special branching structure and by novel algorithm design. We demonstrate our techniques 
by computing the channel capacities of the timing side-channels of two programs with extremely large 
numbers of paths.},
}