Coloring Symbolic Memory Graphs to Detect DRM-Specific Errors in Linux Drivers
https://doi.org/10.15514/ISPRAS-2025-37(5)-5
Abstract
This paper discusses a particular type of subtle use-after-free errors in the Direct Rendering Manager (DRM) subsystem of the Linux kernel. These errors occur due to incorrectly allocated memory for structures accessible from user space via device callbacks. To detect these errors, we use a shape analysis based on the Symbolic Memory Graph (SMG) domain. We introduce the coloring of allocated memory to track its origin. Among 186 Linux DRM drivers, we have found 6 violations of the proposed rule.
Keywords
Supporting agencies: The authors would like to thank Vadim Mutilin, colleagues from the Linux Verification Center, and the maintainers of the Linux DRM subsystem for their feedback and comments.
About the Authors
Ekaterina Mikhaylovna ORLOVA
Institute for System Programming of the Russian Academy of Sciences
Russian Federation
Russian Federation
Master’s student at the Faculty of Computational Mathematics and Cybernetics of Lomonosov Moscow State University (MSU), lab assistant at the Institute for System Programming of the RAS. Research interests: static analysis and verification of the Linux kernel.
Anton Aleksandrovich VASILYEV
Institute for System Programming of the Russian Academy of Sciences
Russian Federation
Russian Federation
Junior researcher at the Ivannikov Institute for System Programming of the RAS. Research interests: static verification, software model checking, static program analysis.
Oleg Maximovich PETROV
Institute for System Programming of the Russian Academy of Sciences
Russian Federation
Russian Federation
Postgraduate student and intern researcher at the Ivannikov Institute for System Programming of the RAS. His research interests include software model checking, static program analysis, delta debugging.
References
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.
Review
For citations:
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
Email this article 