Окрашивание символьных графов памяти для выявления ошибок, специфичных для DRM-драйверов Linux
https://doi.org/10.15514/ISPRAS-2025-37(5)-5
Аннотация
В статье рассматривается одна трудновоспроизводимая ошибка типа use-after-free в подсистеме Direct Rendering Manager (DRM) ядра операционной системы Linux. Её причиной является некорректный способ выделения памяти, доступной для пользовательского кода через обратные вызовы устройства. Для поиска ошибок работы с памятью мы используем анализ на основе символьных графов памяти (SMG). Чтобы отследить способ выделения памяти, мы добавили ей цвет. Среди 186 проанализированных драйверов DRM ОС Linux было найдено 6 нарушений предложенного правила.
Ключевые слова
драйверы Linux,
уязвимость use-after-free,
анализ динамической памяти,
автоматическая статическая верификация,
символьные графы памяти.
При поддержке: Авторы выражают благодарность Вадиму Мутилину, коллегам из Технологического центра исследования безопасности ядра Linux, а также разработчикам, поддерживающим подсистему DRM в Linux, за их отзывы и комментарии.
Об авторах
Екатерина Михайловна ОРЛОВА
Институт системного программирования РАН
Россия
Россия
Студентка магистратуры факультета вычислительной математики и кибернетики МГУ, лаборант Института системного программирования РАН. Сфера научных интересов: статический анализ и верификация ядра Linux.
Антон Александрович ВАСИЛЬЕВ
Институт системного программирования РАН
Россия
Россия
Младший научный сотрудник Института системного программирования им. В.П. Иванникова РАН. Сфера научных интересов: статическая верификация и анализ программ.
Олег Максимович ПЕТРОВ
Институт системного программирования РАН
Россия
Россия
Аспирант и стажёр-исследователь Института системного программирования им. В.П. Иванникова РАН. Сфера научных интересов: статическая верификация и анализ исходного кода программ, delta debugging.
Список литературы
1. E.M. Clarke, T.A. Henzinger, H. Veith, and R. Bloem. Handbook of Model Checking. Springer International Publishing, Cham. 2018. DOI: 10.1007/978-3-319-10575-8.
2. I.S. Zakharov, M.U. Mandrykin, V.S. Mutilin, E.M. Novikov, A.K. Petrenko, and A.V. Khoroshilov. Configurable toolset for static verification of operating systems kernel modules. Programming and Computer Software, vol. 41, no. 1. 01.01.2015. pp. 49–64. DOI: 10.1134/S0361768815010065.
3. I. Zakharov, E. Novikov, and I. Shchepetkov. Klever: Verification Framework for Critical Industrial C Programs. 2023. DOI: 10.48550/arXiv.2309.16427.
4. D. Baier, D. Beyer, P.-C. Chien, M.-C. Jakobs, M. Jankola, M. Kettl, N.-Z. Lee, T. Lemberger, M. Lingsch-Rosenfeld, H. Wachowitz, and P. Wendler. Software Verification with CPAchecker 3.0: Tutorial and User Guide. Formal Methods. 2025. pp. 543–570. DOI: 10.1007/978-3-031-71177-0_30.
5. V.S. Mutilin, E.M. Novikov, and A.V. Khoroshilov. Analysis of typical faults in Linux operating system drivers. Trudy ISP RAN/Proc. ISP RAS, 2012, vol. 22, pp. 349–374 (in Russian). DOI: 10.15514/ispras-2012-22-19.
6. Found Bugs by Klever. [Online]. Available at: https://github.com/ldv-klever/klever?tab=readme-ov-file#found-bugs, accessed 09.09.2025.
7. A.A. Vasilyev. Static verification for memory safety of Linux kernel drivers. Trudy ISP RAN/Proc. ISP RAS, 2018, vol. 30, issue 6, pp. 143–160. DOI: 10.15514/ISPRAS-2018-30(6)-8.
8. A.A. Vasilyev and V.S. Mutilin. Predicate Extension of Symbolic Memory Graphs for the Analysis of Memory Safety Correctness. Programming and Computer Software, vol. 46, no. 8, 01.12.2020, pp. 747–754. DOI: 10.1134/S0361768820080071.
9. K. Dudka, P. Peringer, and T. Vojnar. Byte-Precise Verification of Low-Level List Manipulation. in F. Logozzo and M. Fähndrich (eds). Static Analysis. Springer Berlin Heidelberg, Berlin, Heidelberg. 2013. pp. 215–237. DOI: 10.1007/978-3-642-38856-9_13.
10. K. Dudka, P. Muller, P. Peringer, V. Šoková, and T. Vojnar. Algorithmic Details behind the Predator Shape Analyser. 2024. DOI: 10.48550/arXiv.2403.18491.
11. DRM Internals – The Linux Kernel documentation. [Online]. Available at: https://www.kernel.org/doc/html/latest/gpu/drm-internals.html, accessed 29.09.2025.
12. E. Orlova. [PATCH v4] drm/stm: Avoid use-after-free issues with crtc and plane. [Online]. Available at: https://lore.kernel.org/all/20240216125040.8968-1-e.orlova@ispras.ru/, accessed 06.10.2025.
13. J.L. Lawall and G. Muller. Coccinelle: 10 Years of Automated Evolution in the Linux Kernel. USENIX Annual Technical Conference. 2018. [Online]. Available at: https://www.usenix.org/system/files/conference/atc18/atc18-lawall.pdf, accessed 06.10.2025.
14. O. Petrov. [PATCH] cocci: drm: report devm-allocated arguments and fields. [Online]. Available at: https://lore.kernel.org/all/20250924140126.23027-1-o.petrov@ispras.ru/, accessed 24.09.2025.
15. E. Orlova. drm/stm: Avoid use-after-free issues with crtc and plane. [Online]. Available at: https://web.git.kernel.org/pub/scm/linux/kernel/git/torvalds/linux.git/commit/?id=19dd9780b7ac673be95bf6fd6892a184c9db611f, accessed 15.07.2024.
16. M. Schmitt. Linux kernel device driver testing. How are device drivers being tested? Master’s Thesis, Institute of Mathematics and Statistics, University of São Paulo, São Paulo. 17.10.2022. DOI: 10.11606/D.45.2022.tde-30112022-152524.
17. A. Konovalov. Sanitizing the Linux kernel: On KASAN and other Dynamic Bug-finding Tools. Linux Security Summit Europe. 2022. [Online]. Available at: https://www.youtube.com/watch?v=KmFVPyHyfqQ.
18. K. Serebryany, D. Bruening, A. Potapenko, and D. Vyukov. AddressSanitizer: A Fast Address Sanity Checker. USENIX ATC 2012. 2012. [Online]. Available at: https://www.usenix.org/conference/usenixfederatedconferencesweek/addresssanitizer-fast-address-sanity-checker, accessed 06.10.2025.
19. J.L. Lawall, J. Brunel, N. Palix, R.R. Hansen, H. Stuart, and G. Muller. WYSIWIB: A declarative approach to finding API protocols and bugs in Linux code. DSN’09 – The 39th Annual IEEE/IFIP International Conference on Dependable Systems and Networks. 2009. pp. 43–52. DOI: 10.1109/DSN.2009.5270354.
20. N. Brown. Sparse: a look under the hood. 2016. [Online]. Available at: https://lwn.net/Articles/689907/, accessed 06.10.2025.
21. L. Torvalds. Sparse ‘context’ checking. [Online]. Available at: https://lwn.net/Articles/109066/, accessed 18.09.2025.
22. N. Brown. Smatch: pluggable static analysis for C. 22.06.2016. [Online]. Available at: https://lwn.net/Articles/691882/, accessed 06.10.2025.
23. D. Alden. Finding locking bugs with Smatch. 11.06.2025. Write-up of Dan Carpenter’s talk at Linaro Connect 2025. [Online]. Available at: https://lwn.net/Articles/1023646/, accessed 06.10.2025.
24. A. Belevantsev, A. Borodin, I. Dudina, V. Ignatiev, A. Izbyshev, S. Polyakov, E. Velesevich, and D. Zhurikhin. Design and Development of Svace Static Analyzers. 2018 Ivannikov Memorial Workshop (IVMEM). 2018. pp. 3–9. DOI: 10.1109/IVMEM.2018.00008.
25. Linux Verification Center — Static Analysis (in Russian). [Online]. Available at: https://portal.linuxtesting.ru/activity.html#menu3, accessed 29.09.2025.
26. Found by Linux Verification Center (linuxtesting.org) with SVACE. [Online]. Available at: https://web.git.kernel.org/pub/scm/linux/kernel/git/torvalds/linux.git/log/?qt=grep&q=Found+by+Linux+Verification+Center+(linuxtesting.org)+with+SVACE, accessed 29.09.2025.
27. E.M. Novikov. An approach to implementation of aspect-oriented programming for C. Programming and Computer Software, vol. 39, no. 4. 07.2013. pp. 194–206.
28. I.S. Zakharov, V.S. Mutilin, and A.V. Khoroshilov. Pattern-based environment modeling for static verification of Linux kernel modules. Programming and Computer Software, vol. 41, no. 3. 05.2015. pp. 183–195. DOI: 10.1134/S036176881503007X.
29. I. Zakharov and E. Novikov. Compositional Environment Modelling for Verification of GNU C Programs. 2018 Ivannikov ISPRAS Open Conference. 2018. pp. 39–44. DOI: 10.1109/ISPRAS.2018.00013.
30. P.S. Andrianov. Analysis of Correct Synchronization of Operating System Components. Programming and Computer Software, vol. 46, no. 8. 01.12.2020. pp. 712–730. DOI: 10.1134/S0361768820080022.
31. Predator. [Online]. Available at: https://www.fit.vut.cz/research/group/verifit/public/tools/predator/, accessed 29.09.2025.
32. Klever 4.0.1. [Online]. Available at: https://github.com/ldv-klever/klever/tree/v4.0.1/, accessed 18.03.2025.
33. CPAchecker 702bc1a. [Online]. Available at: https://github.com/ldv-klever/cpachecker/commit/702bc1a36f663d0e1bac13e6c6752e61828e6ac8, accessed 21.03.2025.
Рецензия
Для цитирования:
ОРЛОВА Е.М., ВАСИЛЬЕВ А.А., ПЕТРОВ О.М. Окрашивание символьных графов памяти для выявления ошибок, специфичных для DRM-драйверов Linux. Труды Института системного программирования РАН. 2025;37(5):67-80. https://doi.org/10.15514/ISPRAS-2025-37(5)-5
For citation:
ORLOVA E.M., VASILYEV A.A., PETROV O.M. Coloring Symbolic Memory Graphs to Detect DRM-Specific Errors in Linux Drivers. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2025;37(5):67-80. https://doi.org/10.15514/ISPRAS-2025-37(5)-5
Послать статью по эл. почте 