Citation
Daniel J. Fremont, Sanjit Seshia. "Speeding Up SMT-Based Quantitative Program Analysis". 12th International Workshop on Satisfiability Modulo Theories, 3-13, 17, July, 2014.

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.

Electronic downloads

• paper-02.pdf · application/pdf · 520 kbytes

• HTML

  Daniel J. Fremont, Sanjit Seshia. <a
  href="http://www.terraswarm.org/pubs/278.html"
  >Speeding Up SMT-Based Quantitative Program
  Analysis</a>, 12th International Workshop on
  Satisfiability Modulo Theories, 3-13, 17, July, 2014.

• Plain text

  Daniel J. Fremont, Sanjit Seshia. "Speeding Up
  SMT-Based Quantitative Program Analysis". 12th
  International Workshop on Satisfiability Modulo Theories,
  3-13, 17, July, 2014.

• BibTeX

  @inproceedings{FremontSeshia14_SpeedingUpSMTBasedQuantitativeProgramAnalysis,
      author = {Daniel J. Fremont and Sanjit Seshia},
      title = {Speeding Up SMT-Based Quantitative Program Analysis},
      booktitle = {12th International Workshop on Satisfiability
                Modulo Theories},
      pages = {3-13},
      day = {17},
      month = {July},
      year = {2014},
      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.},
      URL = {http://terraswarm.org/pubs/278.html}
  }
  

Posted by Barb Hoversten on 20 Feb 2014.
Groups: tools