Моделирование окружения драйверов устройств операционной системы Linux
Аннотация
При статической верификации драйверов устройств операционной системы Linux необходимо учитывать особенности взаимодействия драйверов с сердцевиной ядра, так как это взаимодействие оказывает определяющее влияние на работу драйвера. В то же время, верификации драйвера в комбинации с исходным кодом сердцевины ядра не представляется возможной ввиду сложности и объема получающегося кода. В качестве решения этой проблемы в статье предлагается метод моделирования окружения драйверов на основе П-исчисления Р.Милнера и метод трансляции П-модели окружения в программу на языке Си, которая при связывании с исходным кодом драйвера описывает с точки зрения инструментов статической верификации те же сценарии работы драйвера, что и реальное окружение драйвера в операционной системе.
Об авторах
И. С. Захаров
ИСП РАН
Россия
Россия
В. С. Мутилин
ИСП РАН
Россия
Россия
Е. М. Новиков
ИСП РАН
Россия
Россия
А. В. Хорошилов
ИСП РАН
Россия
Россия
Список литературы
1. N. Palix, G. Thomas, S. Saha, C. Calves, J. Lawall, and Gilles Muller. Faults in Linux: Ten years later. Proceedings of the sixteenth international conference on Architectural support for programming languages and operating systems (ASPLOS '11), USA, 2011.
2. D. Beyer, T. Henzinger, R. Jhala, R. Majumdar. The Software Model Checker Blast: Applications to Software Engineering. International Journal on Software Tools for Technology Transfer (STTT), vol. 5, p. 505-525, 2007.
3. Shved P., Mandrykin M., Mutilin V. Predicate Analysis with Blast 2.7 //Proceedings of TACAS. 2012. Vol. 7214. P. 525–527.
4. D. Beyer, M.E. Keremoglu. CPAchecker: A Tool for Configurable Software Verification. In Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 184–190. Springer, Heidelberg, 2011.
5. T. Ball, E. Bounimova, R. Kumar, V. Levin. SLAM2: Static Driver Verification with Under 4% False Alarms. FMCAD, 2010.
6. J. Corbet, G. Kroah-Hartman, A. McPherson. Linux kernel development. How Fast it is Going, Who is Doing It, What They are Doing, and Who is Sponsoring It. http://go.linuxfoundation.org/who-writes-linux-2012, 2012.
7. Milner R. The Polyadic π-Calculus: a Tutorial. LFCS, Department of Computer Science, University of Edinburgh, 1991. P. 49.
8. Мутилин В.С. Верификация драйверов операционной системы Linux при помощи предикатных абстракций. Диссертация на соискание ученой степени к.ф.-м.н., 2012.
9. Мандрыкин М. У., Мутилин В. С., Новиков Е. М. и др. Использование драйверов устройств операционной системы Linux для сравнения инструментов статической верификации //Программирование. 2012. Т. 5. С. 54–71.
Рецензия
Для цитирования:
Захаров И.С., Мутилин В.С., Новиков Е.М., Хорошилов А.В. Моделирование окружения драйверов устройств операционной системы Linux. Труды Института системного программирования РАН. 2013;25:85-112.
For citation:
Zakharov I.S., Mutilin V.S., Novikov E.M., Khoroshilov A.V. Environment Modeling of Linux Operating System Device Drivers. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2013;25:85-112. (In Russ.)
Послать статью по эл. почте 