Построение спецификаций программных интерфейсов в открытой системе покомпонентной верификации ядра Linux

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

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

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

2. M.E. Fagan. Design and Code Inspections to Reduce Errors in Program Development. IBM Systems Journal, 15(3), 182-211, 1976.

3. B. Boehm, V. Basili. Software Defect Reduction Top 10 List. IEEE Computer, 34(1), 135-137, January, 2001.

4. E.S. Raymond. The Cathedral and the Bazaar: Musings on Linux and Open Source by an Accidental Revolutionary. O’Reilly, Sebastopol, CA, USA, 2001.

5. P. Larson. Testing Linux with the Linux Test Project. Proceedings of the Ottawa Linux Symposium, Ottawa, Ontario, Canada, June 26–29, 2002.

6. Novell System Test Kit for Linux.

7. https://www.suse.com/partners/ihv/pdf/SystemTestKit-7.1-Linux-10_22_12.pdf.

8. Oracle Linux Tests.

9. https://oss.oracle.com/projects/olt/dist/documentation/OLT_TestCoverage.pdf.

10. А.В. Цыварев, В.А. Мартиросян. Тестирование драйверов файловых систем в ОС Linux. Труды Института системного программирования РАН, т. 23, стр. 413-426, 2012.

11. D. Engler, B. Chelf, A. Chou, S. Hallem. Checking system rules using system-specific, programmer-written compiler extensions. Proceedings of the 4th conference on Symposium on Operating System Design & Implementation, San Diego, California, pp.1-16, October 22-25, 2000.

12. Coverity Scan: 2011 Open Source Integrity Report.

13. http://www.coverity.com/library/pdf/coverity-scan-2011-open-source-integrity-report.pdf.

14. H. Stuart. Hunting bugs with Coccinelle. Masters Thesis, University of Copenhagen, August, 2008.

15. Sparse - a Semantic Parser for C. https://sparse.wiki.kernel.org/index.php/Main_Page.

16. Dan Carpenter. Killing Bugs in C with Smatch. Linux Plumbers Conference, Santa Rosa, California, September 7-9, 2011.

17. P. Shved, M. Mandrykin, V. Mutilin. Predicate Analysis with Blast 2.7. Proceedings of TACAS, vol. 7214, pp. 525–527, 2012.

18. S. Löwe, P. Wendler. CPAchecker with Adjustable Predicate Analysis. Proceedings of TACAS, vol. 7214, pp. 528–530, 2012.

19. C. Sinz, F. Merz, S. Falke. LLBMC: A Bounded Model Checker for LLVM's Intermediate Representation. Proceedings of TACAS, vol. 7214, pp. 542–544, 2012.

20. D. Beyer. Competition on software verification. Proceedings of TACAS, vol. 7214, pp. 504–524, 2012.

21. Results of the 2013 2nd International Competition on Software Verification.

22. http://sv-comp.sosy-lab.org/2013/results/index.php.

23. D. Engler, M. Musuvathi. Static analysis versus model checking for bug finding. In VMCAI, pp. 191-210, 2004.

24. T. Witkowski, N. Blanc, D. Kroening, G. Weissenbacher. Model checking concurrent Linux device drivers. In Proceedings of the twenty-second IEEE/ACM international conference on Automated software engineering, pp. 501-504, 2007.

25. T. Ball, E. Bounimova, V. Levin, R. Kumar, J. Lichtenberg. The Static Driver Verifier Research Platform. CAV 2010, 2010.

26. H. Post, W. Küchlin. Integration of static analysis for Linux device driver verification. The 6th Intl. Conf. on Integrated Formal Methods, IFM 2007, 2007.

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

28. A. Khoroshilov, V. Mutilin, E. Novikov, P. Shved, A. Strakh. Towards an Open Framework for C Verification Tools Benchmarking. Proceedings of the Eighth International Andrei Ershov Memorial Conference «Perspectives of Systems Informatics» (PSI 2011), pp. 82-91, 2011.

29. Открытая система верификации Linux Driver Verification.

30. http://forge.ispras.ru/projects/ldv.

31. E. Novikov. One Approach to Aspect-Oriented Programming Implementation for the C programming language. roceedings of the 5th Spring/Summer Young Researchers' Colloquium on Software Engineering, Yekaterinburg, pp. 74-81, 12-13 May, 2011.

32. Реализация аспектно-ориентированного программирования для языка Си C Instrumentation Framework. http://forge.ispras.ru/projects/cif.

33. Е.М. Новиков, А.В. Хорошилов. Использование аспектно-ориентированного программирования для выполнения запросов по исходному коду программ. Труды Института системного программирования РАН, т. 23, стр. 371-386, 2012.

34. D. Chamberlain, D. Cross, A. Wardley. Perl Template Toolkit. O'Reilly Media, pp. 592, December, 2003.

35. N. Gunton. Creating Modular Web Pages With EmbPerl. March 13, 2001, http://www.perl.com/pub/2001/03/embperl.html.