Loi Luu
Skip Abstract Section
Abstract
Model counting is the problem of determining the number of solutions that satisfy a given set of constraints. Model counting has numerous applications in the quantitative analyses of program execution time, information flow, combinatorial circuit designs as well as probabilistic reasoning. We present a new approach to model counting for structured data types, specifically strings in this work. The key ingredient is a new technique that leverages generating functions as a basic primitive for combinatorial counting. Our tool SMC which embodies this approach can model count for constraints specified in an expressive string language efficiently and precisely, thereby outperforming previous finite-size analysis tools. SMC is expressive enough to model constraints arising in real-world JavaScript applications and UNIX C utilities. We demonstrate the practical feasibility of performing quantitative analyses arising in security applications, such as determining the comparative strengths of password strength meters and determining the information leakage via side channels.
- BusyBox. http://www.busybox.net/.Google Scholar
- CoreUtils. http://www.gnu.org/software/coreutils.Google Scholar
- Drupal Password Strength Meter. https://drupal.org.Google Scholar
- eBay Password Strength Meter. https://ebay.com.Google Scholar
- Fuzzball. http://bitblaze.cs.berkeley.edu/fuzzball.html.Google Scholar
- Ghttpd Vulnerability. http://www.securityfocus.com/bid/5960.Google Scholar
- John the Ripper. http://www.openwall.com/john/.Google Scholar
- LattE Tool. http://www.math.ucdavis.edu/~latte/.Google Scholar
- MathLink API. http://reference.wolfram.com/mathematica/guide/MathLinkAPI.html.Google Scholar
- Microsoft Password Strength Meter. https://www.microsoft.com/security/pc-security/password-checker.aspx.Google Scholar
- Null HTTPd Vulnerability. http://www.securityfocus.com/bid/5774.Google Scholar
- RelSat Tool. http://code.google.com/p/relsat/.Google Scholar
- SMC Tool Online. https://github.com/loiluu/smc.Google Scholar
- F. Bacchus, S. Dalmao, and T. Pitassi. Solving #SAT and Bayesian Inference with Backtracking Search. Journal of Artificial Intelligence Research, 2009. Google ScholarDigital Library
- M. Backes, B. Kopf, and A. Rybalchenko. Automatic Discovery and Quantification of Information Leaks. In Proceedings of the 30th IEEE Symposium on Security and Privacy, 2009. Google ScholarDigital Library
- A. I. Barvinok. A Polynomial Time Algorithm for Counting Integral Points in Polyhedra When the Dimension Is Fixed. In Proceedings of the 34th Annual Symposium on Foundations of Computer Science, 1993. Google ScholarDigital Library
- R. J. Bayardo and J. D. Pehoushek. Counting Models using Connected Components. In Proceedings of the AAAI National Conference, 2000. Google ScholarDigital Library
- R. J. Bayardo, Jr. and R. C. Schrag. Using CSP Look-back Techniques to Solve Real-world SAT Instances. In Proceedings of the 14th National Conference on Artificial Intelligence and Ninth Conference on Innovative Applications of Artificial Intelligence, 1997. Google ScholarDigital Library
- K. Beyls and E. H. D'Hollander. Generating Cache Hints for Improved Program Efficiency. Journal of Systems Architure, 2004. Google ScholarDigital Library
- F. Biondi, A. Legay, L.-M. Traonouez, and A. Wasowski. QUAIL: A quantitative security analyzer for imperative code. In Proceedings of the 25th International Conference on Computer Aided Verification, 2013. Google ScholarDigital Library
- E. Birnbaum and E. L. Lozinskii. The good old davis-putnam procedure helps counting models. Journal of Artificial Intelligence Research, 1999. Google ScholarDigital Library
- C. Cadar, D. Dunbar, and D. Engler. KLEE: Unassisted and Automatic. Generation of High-Coverage Tests for Complex Systems Programs. In Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation, 2008. Google ScholarDigital Library
- M. Castro, M. Costa, and J.-P. Martin. Better Bug Reporting with Better Privacy. In Proceedings of the 13th International Conference on Architectural Support for Programming Languages and Operating Systems, 2008. Google ScholarDigital Library
- X. de Carné de Carnavalet and M. Mannan. From Very Weak to Very Strong: Analyzing Password-Strength Meters. In Proceedings of the Network and Distributed System Security Symposium, 2014.Google ScholarCross Ref
- A. de Moivre. Miscellanea Analytica. 1730.Google Scholar
- P. Godefroid, N. Klarlund, and K. Sen. DART: Directed Automated Random Testing. In Proceedings of ACM SIGPLAN Conference on Programming Language Design and Implementation, 2005. Google ScholarDigital Library
- P. Godefroid, M. Y. Levin, and D. A. Molnar. Automated Whitebox Fuzz Testing. In Proceedings of the Network and Distributed System Security Symposium, 2008.Google Scholar
- P. Hooimeijer and W. Weimer. A Decision Procedure for Subset Constraints over Regular Languages. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation, 2009. Google ScholarDigital Library
- A. Kiezun, V. Ganesh, P. J. Guo, P. Hooimeijer, and M. D. Ernst. HAMPI: A solver for string constraints. In Proceedings of the Eighteenth International Symposium on Software testing and Analysis, 2009. Google ScholarDigital Library
- V. Klebanov. Precise Quantitative Information Flow Analysis Using Symbolic Model Counting. In Proceedings of the International Workshop on Quantitative Aspects in Security Assurance, 2012.Google Scholar
- D. E. Knuth. The Art of Computer Programming, Volume 1 (3rd Ed.): Fundamental Algorithms. Addison Wesley Longman Publishing Co., Inc., 1997. Google ScholarDigital Library
- D. Koller and N. Friedman. Probabilistic Graphical Models: Principles and Techniques - Adaptive Computation and Machine Learning. The MIT Press, 2009. Google ScholarDigital Library
- B. Lisper. Fully Automatic, Parametric Worst-Case Execution Time Analysis. In Proceedings of Worst-Case Execution Time (WCET) Analysis Workshop, 2003.Google Scholar
- S. McCamant and M. D. Ernst. Quantitative Information Flow as Network Flow Capacity. In Proceedings of the ACM SIGPLAN Conference on Programming language Design and Implementation, 2008. Google ScholarDigital Library
- A. Morgado, P. J. Matos, V. M. Manquinho, and J. P. M. Silva. Counting Models in Integer Domains. In SAT, 2006. Google ScholarDigital Library
- J. Newsome, S. McCamant, and D. Song. Measuring Channel Capacity to Distinguish Undue Influence. In Proceedings of the ACM SIGPLAN Workshop on Programming Languages and Analysis for Security, 2009. Google ScholarDigital Library
- Q.-S. Phan, P. Malacaria, O. Tkachuk, and C. S. Păsăreanu. Symbolic Quantitative Information Flow. SIGSOFT Software Engineering Notes, Nov. 2012. Google ScholarDigital Library
- R. A. Popa, C. M. S. Redfield, N. Zeldovich, and H. Balakrishnan. CryptDB: Protecting Confidentiality with Encrypted Query Processing. In Proceedings of the Twenty-Third ACM Symposium on Operating Systems Principles, 2011. Google ScholarDigital Library
- D. Roth. On the Hardness of Approximate Reasoning. Journal Artificial Intelligence, 1996. Google ScholarDigital Library
- P. Saxena, D. Akhawe, S. Hanna, F. Mao, S. McCamant, and D. Song. A Symbolic Execution Framework for JavaScript. In Proceedings of the IEEE Symposium on Security and Privacy, 2010. Google ScholarDigital Library
- R. Sedgewick and P. Flajolet. Analytic Combinatorics. Cambridge University Press, 2009. Google ScholarDigital Library
- R. Sedgewick and P. Flajolet. An Introduction to the Analysis of Algorithms. Addison-Wesley Professional, 2013.Google Scholar
- C. E. Shannon. A Mathematical Theory of Communication. Bell System Technical Journal, 1948.Google Scholar
- G. Smith. On the Foundations of Quantitative Information Flow. In Proceedings of the 12th International Conference on Foundations of Software Science and Computational Structures, 2009. Google ScholarDigital Library
- B. Taylor. Linear Perspective. 1715.Google Scholar
- S. Tople, S. Shinde, Z. Chen, and P. Saxena. AutoCrypt: Enabling homomorphic computation on servers to protect sensitive web content. In Proceedings of the ACM SIGSAC Conference on Computer & Communications Security, 2013. Google ScholarDigital Library
- A. Turjan, B. Kienhuis, and E. Deprettere. A Compile Time Based Approach for Solving Out-of-Order Communication in Kahn Process Networks. In Proceedings of The IEEE International Conference onApplication-Specific Systems, Architectures and Processors, 2002. Google ScholarDigital Library
- S. Verdoolaege, R. Seghir, K. Beyls, V. Loechner, and M. Bruynooghe. Counting integer points in parametric polytopes using Barvinok's rational functions. Algorithmica, 2007. Google ScholarDigital Library
- M. Weir, S. Aggarwal, B. de Medeiros, and B. Glodek. Password cracking using probabilistic context-free grammars. 2012 IEEE Symposium on Security and Privacy, 2009. Google ScholarDigital Library
- Wolfram Research. Mathematica. http://www.wolfram.com/mathematica, 2013.Google Scholar
Recommendations
A model counter for constraints over unbounded strings
PLDI '14: Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and ImplementationModel counting is the problem of determining the number of solutions that satisfy a given set of constraints. Model counting has numerous applications in the quantitative analyses of program execution time, information flow, combinatorial circuit ...
Prefix and Suffix Reversals on Strings
SPIRE 2015: Proceedings of the 22nd International Symposium on String Processing and Information Retrieval - Volume 9309The Sorting by Prefix Reversals problem consists in sorting the elements of a given permutation $$\pi $$ with a minimum number of prefix reversals, i.e. reversals that always imply the leftmost element of $$\pi $$. A natural extension of this problem is ...
Prefix and suffix transreversals on binary and ternary strings
The problem of sorting by a genome rearrangement event asks for the minimum number of that event required to sort the elements of a given permutation. In this paper, we study a variant of the rearrangement event called prefix and suffix transreversal. A ...
Comments