Input data generation for reaching specific function in program by iterative dynamic analysis

Dynamic symbolic execution is a well-known technique used for different tasks of program analysis: input generation for increasing test coverage for program, inputs of death generation, exploit generation and etc. But huge time costs of program analysis during dynamic symbolic execution for any real-life program is a well-known problem caused by path explosion and necessity of path constraint solving for every path with different SAT/SMT techniques which is a NP-complete task in general case. Brute force analysis of every path in program has limited practical sense for time limited analysis; instead different techniques and heuristics are used to improve analysis performance and reduce space of analysis for specific needs of analyst or while solving specific problem under analysis. We present our approach which combines static analysis of program binary code based on binutils library with dynamic symbolic execution tool based on Avalanche - an iterative dynamic analysis tool to perform targeted input data generation for reaching specific function in the program. As the first step of our algorithm we extract reduced program call graph which contains only calls to functions which ends with the function of interest, then we amplify this call graph with control flow graph inside of functions included into reduced call graph. Using the reduced control-flow graph of program which contain only calls and conditional jumps directions which lead to the function of interest we built the metric of best next analysis direction. This approach allows us to significantly (up to twelve times for some real world programs) reduce the time of reaching function of interest comparatively to brute force program paths analysis with inversion of every conditional jump at the execution path dependent on tainted data.

dynamic program analysis, static program analysis, directed analysis, input data generation

1. Myers G. J., Badgett T., Sandler C. The Art of Software Testing. Third Edition. John Wiley & Sons, Inc., Hoboken, New Jersey, 2012, 240 p.

2. Ju.G. Karpov. MODEL CHECKING. Verification of parralel and distributed systems. SPb:BHV-Peterburg. 2010 (in Russian)

3. Klark Je.M., Gramberg O., Peled D. Verification of program models: Model Checking, M.:MCNMO, 2002 (in Russian)

4. Kyung-Suk Lhee, S.J. Chapin. Buffer Overflow and Format String Overflow Vulnerabilities. Software-Practice & Experience — Special Issue: Security Software, Volume 33 Issue 5, 25 April 2003, pp. 423-460

5. Ari Takanen, Jared D. Demott, Charles Miller. Fuzzing for Software Security Testing and Quality Assurance. Artech House, 2008

6. I.K. Isaev, D.V. Sidorov. Application of dynamic analysis for generating input data exposing critical errors and vulnerabilities in programs. Programmirovanie №4, 2010 g. (in Russian)

7. Cadar C., Dunbar D., Engler. D. KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs USENIX Symposium on Operating Systems Design and Implementation (OSDI 2008), December 8-10, 2008, San Diego, CA, USA

8. Chipounov V., Kuznetsov V., Candea G. The S2E Platform: Design, Implementation, and Applications. ACM Transactions on Computer Systems (TOCS) Special issue: Best papers of ASPLOS, February 2012.

9. V.V. Kaushan, Ju.V. Markin, V.A. Padarjan, A.Ju. Tihonov. Methods of finding errors in binary code. ISP RAS preprints, Preprint 24, 2013. (in Russian)

10. L. de Moura, N. Bjørner. Z3: an Efficient SMT Solver. Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008

11. Ganesh V. Decision Procedures for Bit-Vectors, Arrays and Integers. (PhD. Thesis) Computer Science Department, Stanford University, Stanford, CA, U.S., Sept 2007

12. Isaev I.K., Sidorov D.V., Gerasimov A.Ju., Ermakov M.K. Avalanche: application of dynamic analysis for automatic error detection in programs using network sockets. Trudy ISP RAN/Proc. ISP RAS, vol 21, 2011. (in Russian)

13. I. Johnson. Formal Verification with SMT Solvers: Why and How. ACL2 Theorem Proving Seminar at the University of Texas, Autin, 2009

14. Novikova N.M. Optimization basics. Moskva. 1998. pp. 17–22. (in Russian)

15. S.A. Cook. The complexity of theorem-proving procedures. Proceedings of the third annual ACM symposium on Theory of computing, New York, USA, NY,1971, pp 151-158

16. M.K. Ermakov, A.Y. Gerasimov. [Avalanche: adaptation of parallel and distributed computing for dynamic analysis to improve performance of defect detection]. Trudy ISP RAN/Proc. ISP RAS, vol. 25, 2013, pp. 29-38 (in Russian).

17. S.P. Vartanov, D.V. Sidorov. [Optimization of Boolean satisfiability solver by caching intermediate results]. Trudy ISP RAN/Proc. ISP RAS, vol. 22, 2012, pp. 281-292 (in Russian).

18. Thanassis Agerinos, Sang Kil Cha, Brent Lim Tze Hao, David Broomley. AEG: Automatic Exploit Generation. Proceedings of the Network and Distributed Security Symposyum, Carnegie Mellon University, 2011

19. GNU Binutils [HTML] (http://www.gnu.org/software/binutils/)

20. Schütte J., Fedler R., Titze D. ConDroid: Targeted Dynamic Analysis of Android Applications. Advanced Information Networking and Applications (AINA), IEEE, Gwangui, 2105, DOI:10.1109/AINA.2015.238

21. Wong M., Lie D. IntelliDroid: A Targeted Input Generator for the Dynamic Analysis of Android Malware. In Proceedings of the 2016 Network and Distributed System Security Symposium (NDSS), Feb 2016.