Preview

Труды Института системного программирования РАН

Расширенный поиск

Статическая верификация ошибок использования памяти в модулях ядра ОС Linux

https://doi.org/10.15514/ISPRAS-2016-30(6)-8

Аннотация

Ошибки использования памяти в модулях ядра операционной системы Linux сложно обнаружить, но они могут привести к серьезным последствиям. В данной статье мы описываем метод статической верификации, позволяющий обнаруживать все ошибки в рамках предположений метода. Статическая верификация крупных пректов таких, как ядро ОС Linux, требуют дополнительных усилий. Современные инструменты статической верификации не позволяют анализировать ядро как единое целое, поэтому мы используем упрощенную автоматически генерируемую модель окружения. Эта модель вносит некоторую неточность, но позволяет проводить статическую верификацию. Также мы допускаем отсутствие тела некоторых функций, что приводит к неполным программам, написанных на языке ANSI C. В данной работе предлагается подход к обнаружению ошибок использования памяти в таких неполных программах. Наша техника статической верификации основана на теории символических графов памяти и ее расширении для снижения количества ложных срабатываний. Мы ввели концепцию памяти по требованию для упрощения моделей интерфейсов ядра ОС и реализовали ее в фреймворке статической верификации CPAchecker. Также мы изменили точность модели памяти CPAchecker с байтов на поддержку отдельных битов и добавили поддержку выравнивания структур, аналогичное использованому в компиляторе. Для повышения точности анализа мы реализовали предикатное расширение состояния символического графа памяти. Мы провели проверку модулей ядра ОС Linux для версий 4.11.6 и 4.16.10 с помощью фреймворка статической верификации Klever с инструментом верификации CPAchecker, что позволило проанализировать 6224 и 5215 модулей соответствующих версий. Ручной анализ предупреждений от фреймворка Klever выявил 78 реальных ошибок в модулях ядра. Мы сделали патчи для исправления 33 из них.

Об авторе

А. А. Васильев
Институт системного программирования им. В.П. Иванникова РАН
Россия


Список литературы

1. . G. Klein, J. Andronick, K. Elphinstone, T. Murray, T. Sewell, R. Kolanski, and G. Heiser, Comprehensive formal verification of an os microkernel. ACM Transactions on Computer Systems, vol. 32, no. 1, 2014, pp. 2:1–2:70.

2. . T. Ball, E. Bounimova, B. Cook, V. Levin, J. Lichtenberg, C. McGarvey, B. Ondrusek, S. K. Rajamani, and A. Ustuner, Thorough static analysis of device drivers. SIGOPS Operating Systems Review, vol. 40, no. 4, 2006, pp. 73–85.

3. . D. Engler and M. Musuvathi. Static analysis versus software model checking for bug finding. Lecture Notes in Computer Science, vol. 2937, 2004, pp. 191–210.

4. . Saturn. Precise and Scalable Software Analysis. Available at: http://saturn.stanford.edu/, accessed 01.12.2018.

5. . T. Witkowski, N. Blanc, D. Kroening, and G. Weissenbacher. Model checking concurrent Linux device drivers. In Proceedings of the 22nd IEEE/ACM Int. Conference on Automated Software Engineering, 2007, pp. 501–504.

6. . N. Palix, G. Thomas, S. Saha, C. Calvès, J. Lawall, and G. Muller. Faults in Linux: Ten years later. In Proceedings of the 16th Int. Conference on Architectural Support for Programming Languages and Operating Systems, 2011, pp. 305–318.

7. . Linux driver verification project. Available at: http://linuxtesting.org/ldv, accessed 01.12.2018.

8. . В.С. Мутилин, Е.М. Новиков, А.В. Хорошилов, Анализ типовых ошибок в драйверах операционной системы Linux. Труды ИСП РАН, том 22, 2012, стр. 349-374. DOI: 10.15514/ISPRAS-2012-22-19.

9. . A. Khoroshilov, V. Mutilin, A. Petrenko, and V. Zakharov. Establishing Linux driver verification process, Lecture Notes in Computer Science, vol. 5947, pp. 165–176, 2010.

10. . I. Zakharov, M. Mandrykin, V. Mutilin, E. Novikov, A. Petrenko, and A. Khoroshilov. Configurable toolset for static verification of operating systems kernel modules. Programming and Computer Software, vol. 41, no. 1, 2015, pp. 49–64.

11. . Klever verification framework. Available at: https://forge.ispras.ru/projects/klever, accessed 01.12.2018.

12. . 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, 2015, pp. 183–195.

13. . A. Khoroshilov, V. Mutilin, E. Novikov, and I. Zakharov. Modeling environment for static verification of linux kernel modules. Lecture Notes in Computer Science, vol. 8974, 2015, pp. 400–414.

14. . E. Novikov and I. Zakharov. Towards automated static verification of GNU C programs. Lecture Notes in Computer Science, vol. 10742, 2018, pp. 402–416.

15. . D. Beyer and M. Keremoglu. CPAchecker: A tool for configurable software verification. Lecture Notes in Computer Science, vol. 6806, 2011, pp. 184–190.

16. . K. Dudka, P. Peringer, and T. Vojnar. Byte-precise verification of low-level list manipulation. Lecture Notes in Computer Science, vol. 7935, 2013, pp. 215–237.

17. . R. Wilhelm, S. Sagiv, and T. W. Reps. Shape analysis. Lecture Notes in Computer Science, vol. 1781, 2000, pp. 1–17.

18. . D. Beyer, T. A. Henzinger, and G. Théoduloz. Configurable software verification: concretizing the convergence of model checking and program analysis. Lecture Notes in Computer Science, vol. 4590, 2007, pp. 504–518. [Online]. Available: http://portal.acm.org/citation.cfm?id=1770351.1770419


Рецензия

Для цитирования:


Васильев А.А. Статическая верификация ошибок использования памяти в модулях ядра ОС Linux. Труды Института системного программирования РАН. 2018;30(6):143-160. https://doi.org/10.15514/ISPRAS-2016-30(6)-8

For citation:


Vasilyev A.A. Static verification for memory safety of Linux kernel drivers. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2018;30(6):143-160. https://doi.org/10.15514/ISPRAS-2016-30(6)-8



Creative Commons License
Контент доступен под лицензией Creative Commons Attribution 4.0 License.


ISSN 2079-8156 (Print)
ISSN 2220-6426 (Online)