Paper 2017/244
Model-counting Approaches For Nonlinear Numerical Constraints
Mateus Borges, Quoc-Sang Phan, 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.
Metadata
- Available format(s)
-
PDF
- Category
- Implementation
- Publication info
- Published elsewhere. Major revision. 9th NASA Formal Methods Symposium NFM 2017
- Keywords
- Side-channel AttacksModulo ExponentiationQuantitative Information FlowModel Counting Modulo Theories
- Contact author(s)
- sang phan @ sv cmu edu
- History
- 2017-03-20: received
- Short URL
- https://ia.cr/2017/244
- License
-
CC BY
BibTeX
@misc{cryptoeprint:2017/244,
author = {Mateus Borges and Quoc-Sang Phan and Antonio Filieri and Corina S. Păsăreanu},
title = {Model-counting Approaches For Nonlinear Numerical Constraints},
howpublished = {Cryptology {ePrint} Archive, Paper 2017/244},
year = {2017},
url = {https://eprint.iacr.org/2017/244}
}
