استفاده از یادگیری تقویتی جهت افزایش سرعت حل‌کننده‌های SMT با هدف تشخیص سریع‌تر مسیرهای غیر‌قابل اجرا در نرم‌افزار

فیضی, مجید; اثنی عشری, محمد مهدی

doi:10.22052/scj.2024.253499.1186

استفاده از یادگیری تقویتی جهت افزایش سرعت حل‌کننده‌های SMT با هدف تشخیص سریع‌تر مسیرهای غیر‌قابل اجرا در نرم‌افزار

نوع مقاله : مقاله پژوهشی

نویسندگان

دانشکده مهندسی کامپیوتر، دانشگاه صنعتی خواجه نصیرالدین طوسی، تهران، ایران.

10.22052/scj.2024.253499.1186

چکیده

آزمون نرم‌افزار یک موضوع مهم و لازم در فرآیند توسعه هر نرم‌افزاری می‌باشد. امروزه بخش عمده‌ای از آزمون نرم‌افزار به شیوه خودکار انجام می‌شود. در آزمون خودکار نرم‌افزار موانعی می‌توانند وجود داشته باشند که آزمون را با مشکل مواجه کنند. از این موانع، می‌توان به وجود مسیرهای غیرقابل اجرا در گراف جریان کنترلی حاصل از کدهای نرم‌افزار تحت آزمون اشاره کرد. مسیرهای غیرقابل اجرا، مسیرهایی هستند که با هیچ ورودی نمی‌توان از آنها عبور کرد. وجود چنین مسیرهایی، می‌تواند در حوزه‌های مختلف، مانند تولید داده آزمون، امنیت و مانند آن مشکلاتی را به وجود آورد و باعث هدر رفت منابع شود. برای پیشگیری از مشکلات ذکر شده، تشخیص مسیرهای غیرقابل اجرا بسیار مهم می‌باشد. اما تشخیص این مسیرها در نرم‌افزارهای بزرگ، به دلیل حجم زیاد کدها و زیاد بودن تعداد مسیرها در گراف جریان کنترلی، می‌تواند کاری زمانبر باشد. در روش ارائه شده در این مقاله، سرعت تشخیص مسیرهای غیرقابل اجرا با بکارگیری الگوریتم‌های یادگیری تقویتی بهبود داده شده است. در این روش سرعت حل‌کننده SMT به نام Z3 با بهره‌گیری از عامل DQN، افزایش داده می‌شود. Z3 ابزاری است که برای بررسی قابل حل بودن فرمول‌های ساخته شده از شرط‌های موجود در گراف جریان کنترلی در تشخیص مسیر‌های غیرقابل اجرا استفاده می‌شود. در واقع در این مقاله تاکتیک‌‌های ارائه شده توسط Z3 با استفاده از یادگیری تقویتی یاد گرفته شده و سپس با انتخاب و اعمال تاکتیک‌های Z3 براساس یادگیری انجام شده، سرعت حل Z3 افزایش می‌یابد. با افزایش سرعت Z3، سرعت تمامی روش‌ها و الگوریتم‌هایی که از این ابزار برای تشخیص مسیرهای غیرقابل اجرا استفاده می‌کنند نیز افزایش خواهد یافت. همچنین ابزار Z3 در هر حوزهای که بتوان مسائل را به مساله بررسی صدق‌پذیری یک فرمول کاهش داد نیز کاربرد دارد و بهبود عملکرد آن در چنین حوزه‌هایی نیز می‌تواند موثر باشد. روش ارائه شده در این مقاله در منطق‌های QF_NRA و QF_NIA آزمایش شده است. در آزمایش‌های انجام شده، نشان داده شده است که با استفاده از روش پیشنهادی، سرعت Z3 را می‌توان تا 4.7 برابر افزایش داد. همچنین در آزمایش‌های انجام شده با استفاده از این روش، سرعت Z3 در منطق QF_NRA، به طور میانگین 1.954 برابر و در منطق QF_NIA، به طور میانگین 1.687 برابر افزایش یافته است.

کلیدواژه‌ها

موضوعات

آزمون نرم افزار

عنوان مقاله [English]

Improve methods of infeasible path detection by SMT solvers in software testing using Reinforcement Learning

نویسندگان [English]

Majid Feyzi
Mohammad Mehdi Esnaashari

Faculty of Computer Engineering, K.N Toosi University of Technology, Tehran, Iran.

چکیده [English]

Software testing is an important and necessary matter in the development process of any software. Nowadays, an important part of software testing carrying out automatically. In automatic software testing, there may be obstacles that make the test difficult. One of these obstacles is the infeasible paths in the control flow graph obtained from the codes of software under test. The existence of such paths can cause problems in various fields such as test data generation, security and etc. and also cause resources waste. In order to prevent the mentioned problems, detection of infeasible paths can be very critical. But in some cases, recognizing these paths can be a time-consuming task due to the large amount of codes. In this article, a method is proposed that can increase the infeasible paths detection speed by applying reinforcement learning algorithms. In this method, the speed of the Z3 SMT solver has been increased by using the DQN agent. As the speed of the Z3 tool increases, the speed of all algorithms and methods that use this tool to detect infeasible paths in control flow graphs will also increase. Also, the Z3 tool is using in various other fields, and improving its performance in those fields can also be effective. The proposed method in this article has been tested on QF_NRA and QF_NIA logics. In the experiments, it is shown that using the proposed method, the speed of the Z3 solver can be increased up to 4.7 times.

کلیدواژه‌ها [English]

Automatic software testing
infeasible paths
SMT solvers
Z3 solver
Reinforcement learning
DQN

مراجع

[1] P. Ammann and J. Offutt, Introduction to Software Testing. Cambridge, U.K.: Cambridge Univ. Press, 2016, doi: 10.1017/9781316771273.
[2] B. Beizer, Software Testing Techniques. New York, NY, USA: Van Nostrand Reinhold, 1990.
[3] H. Farzaneh, S. Bakhshayeshi, R. Ebrahimi Atani, and A. Shahbahrami, “A survey on test data generation techniques based on Mutation Testing,” Soft Comput. J., vol. 2, no. 1, pp. 72-85, 2013, dor: 20.1001.1.23223707.1392.2.1.61.5 [In Persian].
[4] Y.-W. Wang, Y. Xing, and X.-Z. Zhang, “A method of path feasibility judgment based on symbolic execution and range analysis,” Int. J. Future Gener. Commun. Netw., vol. 7, no. 3, pp. 205-212, 2014, doi: 10.14257/ijfgcn.2014.7.3.19.
[5] H. Zhu, D. Jin, Y. Gong, Y. Xing, and M. Zhou, “Detecting interprocedural infeasible paths based on unsatisfiable path constraint patterns,” IEEE Access, vol. 7, pp. 15040-15055, 2019, doi: 10.1109/ACCESS.2019.2894593.
[6] S. Jiang et al., “An approach for detecting infeasible paths based on a SMT solver,” IEEE Access, vol. 7, pp. 69058-69069, 2019, doi: 10.1109/ACCESS.2019.2918558.
[7] L. de Moura and N. Bjorner, “Z3: An efficient SMT solver,” in Proc. Int. Conf. Tools Algorithms Constr. Anal. Syst., 2008, pp. 337-340, doi: 10.1007/978-3-540-78800-3_24.
[8] C. Barrett and C. Tinelli, “Satisfiability modulo theories,” in Handbook of Model Checking, Springer, 2018, pp. 305-343, doi: 10.1007/978-3-319-10575-8_11.
[9] M. Balunovic, P. Bielik, and M. Vechev, “Learning to solve SMT formulas,” Adv. Neural Inf. Process. Syst., vol. 31, 2018.
[10] S. Anand, P. Godefroid, and N. Tillmann, “Demand-driven compositional symbolic execution,” in Proc. Int. Conf. Tools Algorithms Constr. Anal. Syst., 2008, pp. 367-381, doi: 10.1007/978-3-540-78800-3_28.
[11] J. Scott, F. Mora, and V. Ganesh, “BanditFuzz: Fuzzing SMT solvers with reinforcement learning,” University of Waterloo, Waterloo Research, 2020.
[12] S. Jeon and J. Moon, “Dr. PathFinder: Hybrid fuzzing with deep reinforcement concolic execution toward deeper path-first search,” Neural Comput. Appl., vol. 34, pp. 10731-10750, 2022, doi: 10.1007/s00521-022-07008-8.
[13] M. Hajibaba and S. Parsa, “Software Fault Localization using Cross Entropy and N-gram Models,” Soft Comput. J., vol. 2, no. 1, pp. 44-59, 2013, dor: 20.1001.1.23223707.1392.2.1.59.3 [In Persian].
[14] S. Ding, H.B.K. Tan, and K.P. Liu, “A survey of infeasible path detection,” in Proc. 7th Int. Conf. Eval. Novel Approaches Softw. Eng. (ENASE), 2012, pp. 43-52.
[15] S. Jang, H.-Y. Kim, Y.-H. Choi, and T.-M. Chung, “A study of advanced hybrid execution using reverse traversal,” in Proc. 2011 Int. Conf. Inf. Manag. Innov. Manag. Ind. Eng., vol. 2, 2011, pp. 557-559, doi: 10.1109/ICIII.2011.278.
[16] H. Ghorbani Moghadam, B. Jamasb, and H. Dehdashti Jahromi, “Review on security requirements in the software production process,” Soft Comput. J., vol. 10, no. 2, pp. 72-83, 2022, doi: 10.22052/scj.2022.242857.0 [In Persian]
[17] B. Barhoush and I. Alsmadi, “Infeasible paths detection using static analysis,” Res. Bull. Jordan ACM, vol. 2, no. 3, pp. 120-126, 2013.
[18] N. Malevris, D. Yates, and A. Veevers, “Predictive metric for likely feasibility of program paths,” Inf. Softw. Technol., vol. 32, no. 2, pp. 115-118, 1990, doi: 10.1016/0950-5849(90)90110-D.
[19] D. Yates and N. Malevris, “Reducing the effects of infeasible paths in branch testing,” ACM SIGSOFT Softw. Eng. Notes, vol. 14, no. 8, pp. 48-54, 1989, doi: 10.1145/75309.75315.
[20] SMT-LIB, Accessed: Feb. 6, 2022, [Online]. Available: https://smtlib.cs.uiowa.edu/.
[21] R.S. Sutton and A.G. Barto, Reinforcement Learning: An Introduction. London, U.K.: The MIT Press, 2018.
[22] E.J. Weyuker, “The applicability of program schema results to programs,” Int. J. Comput. Inf. Sci., vol. 8, no. 5, pp. 387-403, 1979, doi: 10.1007/BF00995175.
[23] D. Gong and X. Yao, “Automatic detection of infeasible paths in software testing,” IET Softw., vol. 4, no. 5, pp. 361-370, 2010, doi: 10.1049/iet-sen.2009.0092.
[24] D. Kundu, M. Sarma, and D. Samanta, “A UML model-based approach to detect infeasible paths,” J. Syst. Softw., vol. 107, pp. 71-92, 2015, doi: 10.1016/j.jss.2015.05.007.
[25] G. Brockman, V. Cheung, L. Pettersson, J. Schneider, J. Schulman, J. Tang and W. Zaremba, “OpenAI Gym,” arXiv preprint, arXiv:1606.01540, 2016.
[26] V. Mnih et al., “Human-level control through deep reinforcement learning,” Nature, vol. 518, pp. 529-533, 2015, doi: 10.1038/nature14236.