Rafael Dutra
ABSTRACT
In software and hardware testing, generating multiple inputs which satisfy a given set of constraints is an important problem with applications in fuzz testing and stimulus generation. However, it is a challenge to perform the sampling efficiently, while generating a diverse set of inputs which satisfy the constraints. We developed a new algorithm QuickSampler which requires a small number of solver calls to produce millions of samples which satisfy the constraints with high probability. We evaluate QuickSampler on large real-world benchmarks and show that it can produce unique valid solutions orders of magnitude faster than other state-of-the-art sampling tools, with a distribution which is reasonably close to uniform in practice.
- Saswat Anand and Mary Jean Harrold. 2011. Heap cloning: Enabling dynamic symbolic execution of java programs. In ASE. 33--42. Google Scholar
Digital Library
- Saswat Anand, Corina S. Păsăreanu, and Willem Visser. 2007. JPF-SE: a symbolic execution extension to Java PathFinder. In TACAS'07. Google ScholarDigital Library
- Shay Artzi, Adam Kiezun, Julian Dolby, Frank Tip, Danny Dig, Amit Paradkar, and Michael D. Ernst. 2008. Finding bugs in dynamic web applications. In ISSTA'08. Google ScholarDigital Library
- Thanassis Avgerinos, Alexandre Rebert, Sang Kil Cha, and David Brumley. 2014. Enhancing Symbolic Execution with Veritesting. In Proceedings of the 36th International Conference on Software Engineering (ICSE 2014). ACM, New York, NY, USA, 1083--1094. Google ScholarDigital Library
- Nikolaj Bjørner, Anh-Dung Phan, and Lars Fleckenstein. 2015. vZ-An Optimizing SMT Solver.. In TACAS, Vol. 15. 194--199. Google ScholarDigital Library
- Marcel Böhme, Van-Thuan Pham, and Abhik Roychoudhury. 2016. Coverage-based greybox fuzzing as markov chain. In Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security. ACM, 1032--1043. Google ScholarDigital Library
- Jacob Burnim and Koushik Sen. 2008. Heuristics for Scalable Dynamic Test Generation. In ASE'08. Google ScholarDigital Library
- Cristian Cadar, Daniel Dunbar, and Dawson Engler. 2008. KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs. In OSDI'08. Google ScholarDigital Library
- Supratik Chakraborty, Daniel J Fremont, Kuldeep S Meel, Sanjit A Seshia, and Moshe Y Vardi. 2015. On Parallel Scalable Uniform SAT Witness Generation.. In TACAS. 304--319. Google ScholarDigital Library
- Supratik Chakraborty, Kuldeep S Meel, and Moshe Y Vardi. 2013. A scalable approximate model counter. In International Conference on Principles and Practice of Constraint Programming. Springer, 200--216.Google ScholarCross Ref
- Supratik Chakraborty, Kuldeep S Meel, and Moshe Y Vardi. 2014. Balancing scalability and uniformity in SAT witness generator. In Design Automation Conference (DAC), 2014 51st ACM/EDAC/IEEE. IEEE, 1--6. Google ScholarDigital Library
- Vitaly Chipounov, Volodymyr Kuznetsov, and George Candea. 2012. The S2E Platform: Design, Implementation, and Applications. ACM Trans. Comput. Syst. 30, 1 (2012), 2. Google ScholarDigital Library
- Lori A. Clarke. 1976. A program testing system. In Proc. of the 1976 annual conference. 488--491. Google ScholarDigital Library
- Leonardo De Moura and Nikolaj Bjørner. 2008. Z3: An efficient SMT solver. Tools and Algorithms for the Construction and Analysis of Systems (2008), 337--340. Google ScholarDigital Library
- Stefano Ermon, Carla P Gomes, Ashish Sabharwal, and Bart Selman. 2013. Embed and project: Discrete sampling with universal hashing. In Advances in Neural Information Processing Systems. 2085--2093. Google ScholarDigital Library
- Stefano Ermon, Carla P Gomes, and Bart Selman. 2012. Uniform solution sampling using a constraint solver as an oracle. Conference on Uncertainty in Artificial Intelligence (2012). Google ScholarDigital Library
- Gordon Fraser and Andrea Arcuri. 2011. EvoSuite: automatic test suite generation for object-oriented software. In Proceedings of the 19th ACM SIGSOFT Symposium and the 13th European Conference on Foundations of Software Engineering (ESEC/FSE '11). ACM, New York, NY, USA, 416--419. Google ScholarDigital Library
- P. Godefroid, N. Klarlund, and K. Sen. 2005. DART: Directed Automated Random Testing. In PLDI'05. Google ScholarDigital Library
- P. Godefroid, M.Y. Levin, and D. Molnar. 2008. Automated Whitebox Fuzz Testing. In NDSS'08.Google Scholar
- Carla P Gomes, Ashish Sabharwal, and Bart Selman. 2007. Near-uniform sampling of combinatorial spaces using XOR constraints. In Advances In Neural Information Processing Systems. 481--488. Google ScholarDigital Library
- Christian Holler, Kim Herzig, and Andreas Zeller. 2012. Fuzzing with Code Fragments. In Proceedings of the 21st USENIX Conference on Security Symposium (Security'12). USENIX Association, Berkeley, CA, USA, 38--38. Google ScholarDigital Library
- Allen D. Householder and Jonathan M. Foote. 2012. Probability-Based Parameter Selection for Black-Box Fuzz Testing. Technical Report. Carnegie Mellon University Software Engineering Institute.Google Scholar
- Alexander Ivrii, Sharad Malik, Kuldeep S Meel, and Moshe Y Vardi. 2016. On computing minimal independent support and its applications to sampling and counting. Constraints 21, 1 (2016), 41--58. Google ScholarDigital Library
- Karthick Jayaraman, David Harvison, Vijay Ganesh, and Adam Kiezun. 2009. jFuzz: A Concolic Whitebox Fuzzer for Java. In In NFM'09.Google Scholar
- James C.King. 1976. Symbolic execution and program testing. Commun. ACM 19 (July 1976), 385--394. Issue 7. Google ScholarDigital Library
- Nathan Kitchen and Andreas Kuehlmann. 2007. Stimulus generation for constrained random simulation. In Computer-Aided Design, 2007. ICCAD 2007. IEEE/ACM International Conference on. IEEE, 258--265. Google ScholarDigital Library
- Nathan Boyd Kitchen. 2010. Markov Chain Monte Carlo Stimulus Generation for Constrained Random Simulation. University of California, Berkeley.Google Scholar
- Guodong Li, Indradeep Ghosh, and Sreeranga P. Rajan. 2011. KLOVER: A Symbolic Execution and Automatic Test Generation Tool for C++ Programs. In CAV. 609--615. Google ScholarDigital Library
- Kuldeep S Meel. 2014. Sampling techniques for boolean satisfiability. Master's thesis (2014).Google Scholar
- Kuldeep S Meel, Moshe Y Vardi, Supratik Chakraborty, Daniel J Fremont, Sanjit A Seshia, Dror Fried, Alexander Ivrii, and Sharad Malik. 2016. Constrained Sampling and Counting: Universal Hashing Meets SAT Solving.. In AAAI Workshop: Beyond NP.Google Scholar
- Alexander Nadel. 2011. Generating Diverse Solutions in SAT.. In SAT. Springer, 287--301. Google ScholarDigital Library
- Reuven Naveh and Amit Metodi. 2013. Beyond feasibility: CP usage in constrained-random functional hardware verification. In International Conference on Principles and Practice of Constraint Programming. Springer, 823--831.Google ScholarCross Ref
- Yehuda Naveh, Michal Rimon, Itai Jaeger, Yoav Katz, Michael Vinov, Eitan s Marcu, and Gil Shurek. 2007. Constraint-based random stimuli generation for hardware verification. AI magazine 28, 3 (2007), 13.Google Scholar
- Carlos Pacheco, Shuvendu K. Lahiri, Michael D. Ernst, and Thomas Ball. 2007. Feedback-directed random test generation. In ICSE'07, Proceedings of the 29th International Conference on Software Engineering. Minneapolis, MN, USA, 75--84. Google ScholarDigital Library
- C. Pasareanu, P. Mehlitz, D. Bushnell, K. Gundy-Burlet, M. Lowry, S. Person, and M. Pape. 2008. Combining Unit-level Symbolic Execution and System-level Concrete Execution for Testing NASA Software. In ISSTA'08. Google ScholarDigital Library
- Prateek Saxena, Devdatta Akhawe, Steve Hanna, Feng Mao, Stephen McCamant, and Dawn Song. 2010. A Symbolic Execution Framework for JavaScript. In Proceedings of the 2010 IEEE Symposium on Security and Privacy (SP '10). IEEE, 513--528. Google ScholarDigital Library
- Koushik Sen and Gul Agha. 2006. CUTE and jCUTE : Concolic Unit Testing and Explicit Path Model-Checking Tools. In CAV'06. Google ScholarDigital Library
- Koushik Sen, Swaroop Kalasapur, Tasneem Brutch, and Simon Gibbs. 2013. Jalangi: A Selective Record-Replay and Dynamic Analysis Framework for JavaScript. In ESEC/FSE'13. To appear. Google ScholarDigital Library
- Koushik Sen, Darko Marinov, and Gul Agha. 2005. CUTE: A Concolic Unit Testing Engine for C. In ESEC/FSE'05. Google ScholarDigital Library
- Dawn Song, David Brumley, Heng Yin, Juan Caballero, Ivan Jager, Min Gyung Kang, Zhenkai Liang, James Newsome, Pongsin Poosankam, and Prateek Saxena. 2008. BitBlaze: A New Approach to Computer Security via Binary Analysis. In ICISS'08. Google ScholarDigital Library
- Marc Thurley. 2006. sharpSAT-counting models with advanced component caching and implicit BCP. SAT 4121 (2006), 424--429. Google ScholarDigital Library
- Nikolai Tillmann and Jonathan de Halleux. 2008. Pex - White Box Test Generation for .NET. In TAP'08. Google ScholarDigital Library
- Wei Wei, Jordan Erenrich, and Bart Selman. 2004. Towards efficient sampling: Exploiting random walk strategies. In AAAI, Vol. 4. 670--676. Google ScholarDigital Library
- Wei Wei and Bart Selman. 2005. A new approach to model counting. In SAT. Springer, 324--339. Google ScholarDigital Library
- Xuejun Yang, Yang Chen, Eric Eide, and John Regehr. 2011. Finding and Understanding Bugs in C Compilers. In Proceedings of the 32Nd ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI '11). ACM, New York, NY, USA, 283--294. Google ScholarDigital Library
- MichaÅĆ Zalewski. {n. d.}. American Fuzzy Lop. http://lcamtuf.coredump.cx/afl. ({n. d.}). Accessed October 1, 2016.Google Scholar
- Yanni Zhao, Jinian Bian, Shujun Deng, and Zhiqiu Kong. 2009. Random stimulus generation with self-tuning. In Computer Supported Cooperative Work in Design, 2009. CSCWD 2009. 13th International Conference on. IEEE, 62--65. Google ScholarDigital Library
Index Terms
- Efficient sampling of SAT solutions for testing
Recommendations
Line segment sampling with blue-noise properties
Line segment sampling has recently been adopted in many rendering algorithms for better handling of a wide range of effects such as motion blur, defocus blur and scattering media. A question naturally raised is how to generate line segment samples with ...
Sampling in software engineering research: a critical review and guidelines
AbstractRepresentative sampling appears rare in empirical software engineering research. Not all studies need representative samples, but a general lack of representative sampling undermines a scientific field. This article therefore reports a critical ...
Efficient sampling: application to image data
PAKDD'05: Proceedings of the 9th Pacific-Asia conference on Advances in Knowledge Discovery and Data MiningSampling is an important preprocessing algorithm that is used to mine large data efficiently. Although a simple random sample often works fine for reasonable sample size, accuracy falls sharply with reduced sample size. In kdd'03 we proposed ease that ...
Comments