Model Counting, Uniform Generation, and Quantitative Information Flow
Supratik Chakraborty, Daniel J. Fremont, Kuldeep Meel, Sanjit Seshia, Moshe Vardi

Citation
Supratik Chakraborty, Daniel J. Fremont, Kuldeep Meel, Sanjit Seshia, Moshe Vardi. "Model Counting, Uniform Generation, and Quantitative Information Flow". Talk or presentation, 29, October, 2014.

Abstract
Model counting is a generalization of SAT which asks not just whether a propositional formula has a satisfying assignment, but how many such assignments there are. This problem and the closely related one of generating satisfying assignments uniformly at random have a wide variety of applications including probabilistic inference, Monte Carlo simulation, and constrained-random verification. In particular, model counting is an essential tool for quantitative information flow analysis, which seeks to measure how much information is leaked by a program. In this poster we describe two lines of research we have been working on lately. First, we have improved recent approximate model counting and sampling algorithms by Chakraborty et al., making them more performant and extending them to the case where assignments have unequal weights. Second, we have developed a new technique for QIF analysis of timing and power side-channels in programs with certain types of control flow that were difficult for earlier methods to handle.

Electronic downloads


Internal. This publication has been marked by the author for TerraSwarm-only distribution, so electronic downloads are not available without logging in.
Citation formats  
  • HTML
    Supratik Chakraborty, Daniel J. Fremont, Kuldeep Meel,
    Sanjit Seshia, Moshe Vardi. <a
    href="http://www.terraswarm.org/pubs/407.html"
    ><i>Model Counting, Uniform Generation, and
    Quantitative Information Flow</i></a>, Talk or
    presentation,  29, October, 2014.
  • Plain text
    Supratik Chakraborty, Daniel J. Fremont, Kuldeep Meel,
    Sanjit Seshia, Moshe Vardi. "Model Counting, Uniform
    Generation, and Quantitative Information Flow". Talk or
    presentation,  29, October, 2014.
  • BibTeX
    @presentation{ChakrabortyFremontMeelSeshiaVardi14_ModelCountingUniformGenerationQuantitativeInformation,
        author = {Supratik Chakraborty and Daniel J. Fremont and
                  Kuldeep Meel and Sanjit Seshia and Moshe Vardi},
        title = {Model Counting, Uniform Generation, and
                  Quantitative Information Flow},
        day = {29},
        month = {October},
        year = {2014},
        abstract = {Model counting is a generalization of SAT which
                  asks not just whether a propositional formula has
                  a satisfying assignment, but how many such
                  assignments there are. This problem and the
                  closely related one of generating satisfying
                  assignments uniformly at random have a wide
                  variety of applications including probabilistic
                  inference, Monte Carlo simulation, and
                  constrained-random verification. In particular,
                  model counting is an essential tool for
                  quantitative information flow analysis, which
                  seeks to measure how much information is leaked by
                  a program. In this poster we describe two lines of
                  research we have been working on lately. First, we
                  have improved recent approximate model counting
                  and sampling algorithms by Chakraborty et al.,
                  making them more performant and extending them to
                  the case where assignments have unequal weights.
                  Second, we have developed a new technique for QIF
                  analysis of timing and power side-channels in
                  programs with certain types of control flow that
                  were difficult for earlier methods to handle.},
        URL = {http://terraswarm.org/pubs/407.html}
    }
    

Posted by Daniel J. Fremont on 28 Oct 2014.
Groups: tools

Notice: This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All persons copying this information are expected to adhere to the terms and constraints invoked by each author's copyright.