Конфигурируемая система статической верификации модулей ядра операционных систем

Ядро операционной системы (ОС) представляет собой критичную в отношении надежности и производительности программную систему. Качество ядра современных ОС уже находится на достаточно высоком уровне. Иначе обстоит дело с модулями ядра, например, драйверами устройств, которые по ряду причин имеют существенно более низкий уровень качества. Одними из наиболее критичных и распространенных ошибок в модулях ядра являются нарушения правил корректного использования программного интерфейса ядра ОС. Выявить все такие нарушения в модулях или доказать их корректность потенциально можно с помощью инструментов статической верификации, которым для проведения анализа необходимо предоставить контрактные спецификации, описывающие формальным образом обязательства ядра и модулей по отношению друг к другу. В статье рассматриваются существующие методы и системы статической верификации модулей ядра различных ОС. Предлагается новый метод статической верификации модулей ядра ОС Linux, который позволяет конфигурировать процесс проверки на каждом из его этапов. Показывается, каким образом данный метод может быть адаптирован для проверки компонентов ядра других ОС. Описывается архитектура конфигурируемой системы статической верификации модулей ядра ОС Linux, реализующей предложенный метод, и демонстрируются результаты ее практического применения. В заключении рассматриваются направления дальнейшего развития

ядро операционной системы, модуль ядра, качество программной системы, статическая верификация, контрактная спецификация, модель окружения, спецификация правила корректного использования программного интерфейса

1. Chou A., Yang J., Chelf B., Hallem S., Engler D. An empirical study of operating system errors. Proceedings of the 18th ACM Symposium on Operating Systems Principles (SOSP), pp. 73-88, 2001. doi: 10.1145/502034.502042

2. Swift M., Bershad B., Levy H. Improving the reliability of commodity operating systems. Proceedings of the 19th ACM Symposium on Operating Systems Principles (SOSP), pp. 73-88, 2003. doi: 10.1145/502034.502042

3. Palix N., Thomas G., Saha S., Calves C., Lawall J., Muller G. Faults in Linux: ten years later. Proceedings of the 16th International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS), pp. 305-318, 2011. doi: 10.1145/1950365.1950401

4. Мутилин В.С., Новиков Е.М., Хорошилов А.В. Анализ типовых ошибок в драйверах операционной системы Linux. Труды Института системного программирования РАН, т. 22, стр. 349-374, 2012.

5. Ball T., Bounimova E., Cook B., Levin V., Lichtenberg J., McGarvey C., Ondrusek B., Rajamani S. K., Ustuner A. Thorough static analysis of device drivers. Proceedings of the 1st ACM SIGOPS/EuroSys European Conference on Computer Systems (EuroSys), pp. 73-85, 2006. doi: 10.1145/1218063.1217943

6. Glass R.L. Facts and fallacies of software engineering. Addison-Wesley Professional, 2002.

7. Engler D., Chelf B., Chou A., Hallem S. Checking system rules using system-specific, programmer-written compiler extensions. Proceedings of the 4th conference on Symposium on Operating System Design & Implementation (OSDI), vol. 4, pp. 1-16, 2000.

8. Аветисян А., Белеванцев А., Бородин А., Несов В. Использование статического анализа для поиска уязвимостей и критических ошибок в исходном коде программ. Труды Института системного программирования РАН, т. 21, стр. 23-38, 2011.

9. Lawall J. L., Brunel J., Palix N., Rydhof H. R., Stuart H., Muller G. WYSIWIB: A declarative approach to finding API protocols and bugs in Linux code. Proceedings of the 39th Annual IEEE/IFIP International Conference on Dependable Systems and Networks (DSN), pp. 43-52, 2009. doi: 10.1109/DSN.2009.5270354

10. Мандрыкин М.У., Мутилин В.С., Хорошилов А.В. Введение в метод CEGAR - уточнение абстракции по контрпримерам. Труды Института системного программирования РАН, т. 24, стр. 219-292, 2013.

11. Engler D., Musuvathi M. Static analysis versus model checking for bug finding. Proceedings of the 5th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI), LNCS, vol. 2937, pp. 191-210, 2004. doi: 10.1007/978-3-540-24622-0_17

12. Beyer D. Competition on Software Verification. Proceedings of the 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), LNCS, vol. 7214, pp. 504-524, 2012. doi: 10.1007/978-3-642-28756-5_38

13. Beyer D. Second Competition on Software Verification. Proceedings of the 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), LNCS, vol. 7795, pp. 594-609, 2013. doi: 10.1007/978-3-642-36742-7_43

14. Мандрыкин М.У., Мутилин В.С., Новиков Е.М., Хорошилов А.В. Обзор инструментов статической верификации Си программ в применении к драйверам устройств операционной системы Linux. Труды Института системного программирования РАН, т. 22, стр. 293-326, 2012.

15. Corbet J., Kroah-Hartman G., McPherson A. 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.

16. Ball T., Levin V., Rajamani S.K. A decade of software model checking with SLAM. Communications of the ACM, vol. 54, issue 7, pp. 68-76, 2011. doi: 10.1145/1965724.1965743

17. Ball T., Bounimova E., Kumar R., Levin V. SLAM2: Static driver verification with under 4% false alarms. Proceedings of the 10th International Conference on Conference on Formal Methods in Computer-Aided Design (FMCAD), pp. 35-42, 2010.

18. Ball T., Rajamani S.K. SLIC: A specification language for interface checking of C. Technical Report MSR-TR-2001-21, Microsoft Research, 2001.

19. Ball T., Bounimova E., Levin V., Kumar R., Lichtenberg J. The Static Driver Verifier Research Platform. Proceedings of the 22nd International Conference on Computer Aided Verification (CAV), LNCS, vol. 6174, pp. 119-122, 2010. doi: 10.1007/978-3-642-14295-6_11

20. Witkowski T., Blanc N., Kroening D., Weissenbacher G. Model checking concurrent Linux device drivers. Proceedings of the 22nd IEEE/ACM international conference on Automated Software Engineering (ASE), pp. 501-504, 2007. doi: 10.1145/1321631.1321719

21. Post H., Küchlin W. Integrated static analysis for Linux device driver verification. Proceedings of the 6th International Conference on Integrated Formal Methods (IFM), LNCS, vol. 4591, pp. 518-537, 2007. doi: 10.1007/978-3-540-73210-5_27

22. Clarke E., Kroening D., Lerda F. A tool for checking ANSI-C programs. Proceedings of the 10th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), LNCS, vol. 2988, pp. 168-176, 2004. doi: 10.1007/978-3-540-24730-2_15

23. Clarke E., Kroening D., Sharygina N., Yorav K. SATABS: SAT-based predicate abstraction for ANSI-C. Proceedings of the 11th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), LNCS, vol. 3440, pp. 570-574, 2005. doi: 10.1007/978-3-540-31980-1_40

24. Мутилин В.С. Верификация драйверов операционной системы Linux при помощи предикатных абстракций. Диссертация на соискание ученой степени кандидата физико-математических наук, Институт системного программирования РАН, 2012.

25. Захаров И.С., Мутилин В.С., Новиков Е.М., Хорошилов А.В. Моделирование окружения драйверов устройств операционной системы Linux. Труды Института системного программирования РАН, т. 25, стр. 85-112, 2013.

26. Новиков Е.М. Развитие метода контрактных спецификаций для верификации модулей ядра операционной системы Linux. Диссертация на соискание ученой степени кандидата физико-математических наук, Институт системного программирования РАН, 2013.

27. Necula G. C., McPeak S., Rahul S.P., Weimer W. CIL: Intermediate language and tools for analysis and transformation of C programs. Proceedings of the 11th International Conference on Conference on Compiler Construction, LNCS, vol. 2304, pp. 213-228, 2002. doi: 10.1007/3-540-45937-5_16

28. Мутилин В.С., Новиков Е.М., Страх А.В., Хорошилов А.В., Швед П.Е. Архитектура Linux Driver Verification. Труды Института системного программирования РАН, т. 20, стр. 163-187, 2011.

29. Khoroshilov A., Mutilin V., Novikov E., Zakharov I. Modeling environment for static verification of Linux kernel modules. Proceedings of the 11th International Andrei Ershov Memorial Conference (PSI), 2014.

30. Beyer D., Henzinger T., Jhala R., Majumdar R. The software model checker BLAST: Applications to software engineering. International Journal on Software Tools for Technology Transfer (STTT), vol. 5, pp. 505-525, 2007. doi: 10.1007/s10009-007-0044-z

31. Beyer D., Keremoglu M.E. CPAchecker: A tool for configurable software verification. In Proceedings of the 23rd International Conference on Computer Aided Verification (CAV), LNCS, vol. 6806, pp. 184-190, 2011. doi: 10.1007/978-3-642-22110-1_16

32. Albarghouthi A., Li Y., Gurfinkel A., Chechik M. UFO: A framework for abstraction and interpolation-based software verification. Proceedings of the 24th International Conference on Computer Aided Verification, LNCS, vol. 7358, pp. 672-678, 2012. doi: 10.1007/978-3-642-31424-7_48

33. Новиков Е.М. Упрощение анализа трасс ошибок инструментов статического анализа кода. Сборник научных трудов научно-практической конференции Актуальные Проблемы Программной Инженерии (АППИ), стр. 215-221, 2011.

34. Список ошибок, выявленных в модулях ядра ОС Linux с помощью конфигурируемой системы статической верификации Linux Driver Verification Tools. http://linuxtesting.org/results/ldv.

35. Мандрыкин М.У., Мутилин В.С., Новиков Е.М., Хорошилов А.В., Швед П.Е. Использование драйверов устройств операционной системы Linux для сравнения инструментов статической верификации. Программирование, т. 38, н. 5, стр. 54-71, 2012.

36. Бейер Д., Петренко А.К. Верификация драйверов операционной системы Linux. Труды Института системного программирования РАН, т. 23, стр. 405-412, 2012.

37. Chou A., Yang J., Chelf B., Hallem S., Engler D. An empirical study of operating system errors. Proceedings of the 18th ACM Symposium on Operating Systems Principles (SOSP), pp. 73-88, 2001. doi: 10.1145/502034.502042

38. Swift M., Bershad B., Levy H. Improving the reliability of commodity operating systems. Proceedings of the 19th ACM Symposium on Operating Systems Principles (SOSP), pp. 73-88, 2003. doi: 10.1145/502034.502042

39. Palix N., Thomas G., Saha S., Calves C., Lawall J., Muller G. Faults in Linux: ten years later. Proceedings of the 16th International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS), pp. 305-318, 2011. doi: 10.1145/1950365.1950401

40. Mutilin V.S., Novikov E.M., Khoroshilov А.V. Аnaliz tipovykh oshibok v drajverakh operatsionnoj sistemy Linux [Analysis of typical faults in Linux operating system drivers]. Trudy ISP RАN [The Proceedings of ISP RAS], vol. 22, pp. 349-374, 2012 (in Russian).

41. Ball T., Bounimova E., Cook B., Levin V., Lichtenberg J., McGarvey C., Ondrusek B., Rajamani S. K., Ustuner A. Thorough static analysis of device drivers. Proceedings of the 1st ACM SIGOPS/EuroSys European Conference on Computer Systems (EuroSys), pp. 73-85, 2006. doi: 10.1145/1218063.1217943

42. Glass R.L. Facts and fallacies of software engineering. Addison-Wesley Professional, 2002.

43. Engler D., Chelf B., Chou A., Hallem S. Checking system rules using system-specific, programmer-written compiler extensions. Proceedings of the 4th conference on Symposium on Operating System Design & Implementation (OSDI), vol. 4, pp. 1-16, 2000.

44. Аvetisyan А., Belevantsev А., Borodin А., Nesov V. Ispol'zovanie staticheskogo analiza dlya poiska uyazvimostej i kriticheskikh oshibok v iskhodnom kode programm [Using static analysis for finding security vulnerabilities and critical errors in source code]. Trudy ISP RАN [The Proceedings of ISP RAS], vol. 21, pp. 23-38, 2011 (in Russian).

45. Lawall J. L., Brunel J., Palix N., Rydhof H. R., Stuart H., Muller G. WYSIWIB: A declarative approach to finding API protocols and bugs in Linux code. Proceedings of the 39th Annual IEEE/IFIP International Conference on Dependable Systems and Networks (DSN), pp. 43-52, 2009. doi: 10.1109/DSN.2009.5270354

46. Mandrykin M.U., Mutilin V.S., Khoroshilov А.V. Vvedenie v metod CEGAR - utochnenie abstraktsii po kontrprimeram [Introduction to CEGAR - Counter-Example Guided Abstraction Refinement]. Trudy ISP RАN [The Proceedings of ISP RAS], vol. 24, pp. 219-292, 2013 (in Russian).

47. Engler D., Musuvathi M. Static analysis versus model checking for bug finding. Proceedings of the 5th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI), LNCS, vol. 2937, pp. 191-210, 2004. doi: 10.1007/978-3-540-24622-0_17

48. Beyer D. Competition on Software Verification. Proceedings of the 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), LNCS, vol. 7214, pp. 504-524, 2012. doi: 10.1007/978-3-642-28756-5_38

49. Beyer D. Second Competition on Software Verification. Proceedings of the 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), LNCS, vol. 7795, pp. 594-609, 2013. doi: 10.1007/978-3-642-36742-7_43

50. Mandrykin M.U., Mutilin V.S., Novikov E.M., Khoroshilov А.V. Obzor instrumentov staticheskoj verifikatsii Si programm v primenenii k drajveram ustrojstv operatsionnoj sistemy Linux [Static verification tools for C programs and Linux device drivers: A survey]. Trudy ISP RАN [The Proceedings of ISP RAS], vol. 22, pp. 293-326, 2012 (in Russian).

51. Corbet J., Kroah-Hartman G., McPherson A. 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.

52. Ball T., Levin V., Rajamani S.K. A decade of software model checking with SLAM. Communications of the ACM, vol. 54, issue 7, pp. 68-76, 2011. doi: 10.1145/1965724.1965743

53. Ball T., Bounimova E., Kumar R., Levin V. SLAM2: Static driver verification with under 4% false alarms. Proceedings of the 10th International Conference on Conference on Formal Methods in Computer-Aided Design (FMCAD), pp. 35-42, 2010.

54. Ball T., Rajamani S.K. SLIC: A specification language for interface checking of C. Technical Report MSR-TR-2001-21, Microsoft Research, 2001.

55. Ball T., Bounimova E., Levin V., Kumar R., Lichtenberg J. The Static Driver Verifier Research Platform. Proceedings of the 22nd International Conference on Computer Aided Verification (CAV), LNCS, vol. 6174, pp. 119-122, 2010. doi: 10.1007/978-3-642-14295-6_11

56. Witkowski T., Blanc N., Kroening D., Weissenbacher G. Model checking concurrent Linux device drivers. Proceedings of the 22nd IEEE/ACM international conference on Automated Software Engineering (ASE), pp. 501-504, 2007. doi: 10.1145/1321631.1321719

57. Post H., Küchlin W. Integrated static analysis for Linux device driver verification. Proceedings of the 6th International Conference on Integrated Formal Methods (IFM), LNCS, vol. 4591, pp. 518-537, 2007. doi: 10.1007/978-3-540-73210-5_27

58. Clarke E., Kroening D., Lerda F. A tool for checking ANSI-C programs. Proceedings of the 10th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), LNCS, vol. 2988, pp. 168-176, 2004. doi: 10.1007/978-3-540-24730-2_15

59. Clarke E., Kroening D., Sharygina N., Yorav K. SATABS: SAT-based predicate abstraction for ANSI-C. Proceedings of the 11th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), LNCS, vol. 3440, pp. 570-574, 2005. doi: 10.1007/978-3-540-31980-1_40

60. Mutilin V.S. Verifikatsiya drajverov operatsionnoj sistemy Linux pri pomoshhi predikatnykh abstraktsij [Linux drivers verification with help of predicate abstractions]. Dissertatsiya na soiskanie uchenoj stepeni kandidata fiziko-matematicheskikh nauk, ISP RАN [PhD thesis, ISP RAS], 2012 (in Russian).

61. Zakharov I.S., Mutilin V.S., Novikov E.M., Khoroshilov А.V. Modelirovanie okruzheniya drajverov ustrojstv operatsionnoj sistemy Linux [Environment modeling of Linux operating system device drivers]. Trudy ISP RАN [The Proceedings of ISP RAS], vol. 25, pp. 85-112, 2013 (in Russian).

62. Novikov E.M. Razvitie metoda kontraktnykh spetsifikatsij dlya verifikatsii modulej yadra operatsionnoj sistemy Linux. [Development of contract specifications method for verification of Linux kernel modules]. Dissertatsiya na soiskanie uchenoj stepeni kandidata fiziko-matematicheskikh nauk, ISP RАN [PhD thesis, ISP RAS], 2013 (in Russian).

63. Necula G. C., McPeak S., Rahul S.P., Weimer W. CIL: Intermediate language and tools for analysis and transformation of C programs. Proceedings of the 11th International Conference on Conference on Compiler Construction, LNCS, vol. 2304, pp. 213-228, 2002. doi: 10.1007/3-540-45937-5_16

64. Mutilin V.S., Novikov E.M., Strakh А.V., Khoroshilov А.V., Shved P.E. Аrkhitektura Linux Driver Verification [Linux Driver Verification architecture]. Trudy ISP RАN [The Proceedings of ISP RAS], vol. 20, pp. 163-187, 2011 (in Russian).

65. Khoroshilov A., Mutilin V., Novikov E., Zakharov I. Modeling environment for static verification of Linux kernel modules. Proceedings of the 11th International Andrei Ershov Memorial Conference (PSI), 2014.

66. Beyer D., Henzinger T., Jhala R., Majumdar R. The software model checker BLAST: Applications to software engineering. International Journal on Software Tools for Technology Transfer (STTT), vol. 5, pp. 505-525, 2007. doi: 10.1007/s10009-007-0044-z

67. Beyer D., Keremoglu M.E. CPAchecker: A tool for configurable software verification. In Proceedings of the 23rd International Conference on Computer Aided Verification (CAV), LNCS, vol. 6806, pp. 184-190, 2011. doi: 10.1007/978-3-642-22110-1_16

68. Albarghouthi A., Li Y., Gurfinkel A., Chechik M. UFO: A framework for abstraction and interpolation-based software verification. Proceedings of the 24th International Conference on Computer Aided Verification, LNCS, vol. 7358, pp. 672-678, 2012. doi: 10.1007/978-3-642-31424-7_48

69. Novikov E.M. Uproshhenie analiza trass oshibok instrumentov staticheskogo analiza koda. [Simplification of static verifier traces analysis]. Аktual'nye Problemy Programmnoj Inzhenerii [Аctual Problems of Software Engineering], pp. 215-221, 2011 (in Russian).

70. List of bugs found in Linux kernel modules with help of configurable toolset for static verification Linux Driver Verification Tools. http://linuxtesting.org/results/ldv.

71. Mandrykin M.U., Mutilin V.S., Novikov E.M., Khoroshilov A.V., Shved P.E. Using Linux device drivers for static verification tools benchmarking. Programming and Computer Software, vol. 38, n. 5, стр. 245-256, 2012.

72. Beyer D. Petrenko A. Linux Driver Verification. Proceedings of the 5th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation. Applications and Case Studies, LNCS, vol. 7610, pp. 1-6, 2012. doi: 10.1007/s10009-007-0044-z