Cryptology ePrint Archive: Report 2017/244

Model-counting Approaches For Nonlinear Numerical Constraints

Mateus Borges and Quoc-Sang Phan and Antonio Filieri and Corina S. Păsăreanu

Abstract: Model counting is of central importance in quantitative reasoning about systems. Examples include computing the probability that a system successfully accomplishes its task without errors, and measuring the number of bits leaked by a system to an adversary in Shannon entropy. Most previous work in those areas demonstrated their analysis on programs with linear constraints, in which cases model counting is polynomial time. Model counting for nonlinear constraints is notoriously hard, and thus programs with nonlinear constraints are not well-studied. This paper surveys state-of-the-art techniques and tools for model counting with respect to SMT constraints, modulo the bitvector theory, since this theory is decidable, and it can express nonlinear constraints that arise from the analysis of computer programs. We integrate these techniques within the Symbolic Pathfinder platform and evaluate them on difficult nonlinear constraints generated from the analysis of cryptographic functions.

Category / Keywords: implementation / Side-channel Attacks, Modulo Exponentiation, Quantitative Information Flow, Model Counting Modulo Theories

Original Publication (with major differences): 9th NASA Formal Methods Symposium NFM 2017

Date: received 9 Mar 2017

Contact author: sang phan at sv cmu edu

Available format(s): PDF | BibTeX Citation

Version: 20170320:141312 (All versions of this report)

Short URL: ia.cr/2017/244

Discussion forum: Show discussion | Start new discussion


[ Cryptology ePrint archive ]