doi: 10.17586/2226-1494-2020-20-1-101-109


VERIFICATION OF DYNAMIC MEMORY ALLOCATORS BASED ON SYMBOLIC PROGRAM EXECUTION

A. M. Dergachev, D. S. Sadyrin, A. G. Ilina, I. P. Loginov, Y. D. Korenkov


Read the full article  ';
Article in Russian

For citation:
Dergachev A.M., Sadyrin D.S., Ilina A.G., Loginov I.P., Korenkov Iu.D. Verification of dynamic memory allocators based on symbolic program execution. Scientific and Technical Journal of Information Technologies, Mechanics and Optics, 2020, vol. 20, no. 1, pp. 101–109 (in Russian). doi: 10.17586/2226-1494-2020-20-1-101-109


Abstract
Subject of Research. The paper presents the study of vulnerability exploitation techniques in the implementation of dynamic memory allocation algorithms (glibc library allocator): Poisoned Null-byte, Overlapped Chunks, Fastbin Attack,Unsafe Unlink, House of Einherjar, House of Force, House of Spirit, House of Lore, Unsorted Bin Attack. Examples of vulnerability exploitation code and classification of the presented techniques are given in accordance with the Common Weakness Enumeration list. The modern methods and means of vulnerabilities detection are studied; their advantages and disadvantages are shown using the Heap Hopper framework as an example. Modern methods of appropriate software verification are considered. Method. The proposed software verification method combines the approaches of static analysis and symbolic execution using an accurate model of algorithms for dynamic memory allocation. In the compilation process of program being tested, the Kripke structure is created. Dynamic memory vulnerabilities are described by temporal logic formulas. The resulting structure and formulas are passed at the input of the model checking algorithm. Concrete-symbolic execution of the assembled binary file is performed. Vulnerability conditions expressed in the form of propositional logic formulas are checked for symbolic execution paths. Main Results. The practical use of the proposed approach to detection of dynamic memory vulnerabilities in software applications is shown. Symbolic execution is implemented in the form of a low-level debugger, which reduces the operating time of algorithms due to the execution of the application being tested on a real processor. Practical Relevance. The paper presents an integrated approach for solving the problem of automatic vulnerabilities detecting at different stages of the software development life cycle. This approach is applicable for verification of the similar implementations of dynamic memory allocators, such as ptmalloc, dlmalloc, tcmalloc, jemalloc and musl.

Keywords: verification, software errors, symbolic execution, dynamic memory, C language

References
1. Andreev Yu.S., Dergachev A.M., Zharov F.A., Sadyrin D.S. Information security of automated control systems of technological processes. Journal of Instrument Engineering, 2019, vol. 62, no. 4, pp. 331–339. (in Russian). doi: 10.17586/0021-3454-2019-62-4-331-339
2. Shcheglov K., Shcheglov A. Operational characteristics of information system security threats risk. Scientific and Technical Journal of Information Technologies, Mechanics and Optics, 2014, no. 1(89), pp. 129–139. (in Russian)
3. Repel D., Kinder J., Cavallaro L. Modular synthesis of heap exploits. Proc. of the 2017 Workshop on Programming Languages and Analysis for Security, PLAS’17, 2017, pp. 25–35. doi: 10.1145/3139337.3139346
4. Heelan S., Melham T., Kroening D. Automatic heap layout manipulation for exploitation. Proc. 27th USENIX Security Symposium, 2018, pp. 763–779.
5. Liu D., Zhang M., Wang H. A robust and efficient defense against use-after-free exploits via concurrent pointer sweeping. Proc. 25th ACM Conference on Computer and Communications Security (CCS 2018), 2018, pp. 1635-1648. doi: 10.1145/3243734.3243826
6. 7. Lee B., Song C., Jang Y., Wang T., Kim T., Lu L., Lee W. Preventing use-after-free with dangling pointers nullification. Available at: https://wenke.gtisc.gatech.edu/papers/dangnull.pdf (accessed: 15.01.2020). doi: 10.14722/ndss.2015.23238
8. Novark G., Berger E.D. DieHarder: Securing the heap. Proc. 17th ACM Conference on Computer and Communications Security, CCS’10, 2010, pp. 573–584. doi: 10.1145/1866307.1866371
9. Caballero J., Grieco G., Marron M., Nappa A. Undangle: Early detection of dangling pointers in use-after-free and double-free vulnerabilities. Proc. 21st International Symposium on Software Testing and Analysis (ISSTA 2012), 2012, pp. 133–143. doi: 10.1145/04000800.2336769
10. Atzeni A., Marcelli A., Muroni F., Squillero G. HAIT: Heap analyzer with input tracing. ICETE 2017 — Proc. 14th International Joint Conference on e-Business and Telecommunications, 2017, vol. 4, pp. 327–334. doi: 10.5220/0006420803270334
11. Yun I., Karil D., Kim T. Automatic techniques to systematically discover new heap exploitation primitives. Available at: https://arxiv. org/pdf/1903.00503.pdf (accessed: 15.01.2020).
12. Chen H., Wagner D. MOPS: An infrastructure for examining security properties of software. Proc. 9th ACM Conference on Computer and Communications Security, 2002, pp. 235–244. doi: 10.1145/586110.586142
13. Clarke E., Kroening D., Lerda F. A tool for checking ANSI-C programs. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2004, vol. 2988, pp. 168–176. doi: 10.1007/978-3-540-24730-2_15
14. Eckert M, Bianchi A, Wang R, Shoshitaishvili Y, Kruegel C, Vigna G. HeapHopper: Bringing bounded model checking to heap implementation security. Proc. 27th USENIX Security Symposium, 2018, pp. 99–116.
15. Xu W., DuVarney D.C., Sekar R. An efficient and backwards- compatible transformation to ensure memory safety of C programs. Proc. Twelfth ACM SIGSOFT International Symposium on the Foundations of Software Engineering, SIGSOFT 2004/FSE-12, 2004, pp. 117–126. doi: 10.1145/1029894.1029913
16. Yet another free() exploitation technique. Available at: http://phrack. org/issues/66/6.html (accessed: 15.01.2020).
17. Malloc Des-Maleficarum. Available at: http://www.phrack.org/ issues/66/10.html (accessed: 15.01.2020).
18. A repository for learning various heap exploitation techniques. Available at: https://github.com/shellphish/how2heap (accessed: 15.01.2020).
19. Dudina I.A., Belevantsev A.A. Using static symbolic execution to detect buffer overflows. Programming and Computer Software, 2017, vol. 43, no. 5, pp. 277–288. doi: 10.1134/S0361768817050024
20. Ermakov M.K. Efficiency Improvement of Iterative Dynamic Program Analysis. Dissertation for the degree of candidate of mathematical sciences. Moscow, Lomonosov Moscow State University, 2016. (in Russian)
21. Wang F., Yan S. Angr — the next generation of binary analysis. Proc. IEEE Cybersecurity Development Conference (SecDev 2017), 2017, pp. 8–9. doi: 10.1109/SecDev.2017.14
22. Kripke structure (model checking). Available at: https://en.wikipedia. org/wiki/Kripke_structure_(model_checking) (accessed: 15.01.2020).
23. Bhat G., Cleaveland R., Grumberg O. Efficient on-the-fly model checking for CTL. Proc. 10th Annual IEEE Symposium on Logic in Computer Science, 1995, pp. 388–397. doi: 10.1109/LICS.1995.523273
24. Saudel F., Salwan J. Triton: A dynamic symbolic execution framework. Symposium sur la sécurité des technologies de l’information et des communications, SSTIC, France, Rennes, 2015, P. 31–54.
Nikiforakis N., Piessens F., Joosen W. HeapSentry: Kernel-assisted protection against heap overflows. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2013, vol. 7967, pp. 177–196. doi: 10.1007/978-3-642-39235-1_11
 


Creative Commons License

This work is licensed under a Creative Commons Attribution-NonCommercial 4.0 International License
Copyright 2001-2024 ©
Scientific and Technical Journal
of Information Technologies, Mechanics and Optics.
All rights reserved.

Яндекс.Метрика