Архитектура Linux Driver Verification

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

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

1. Инструмент Coverity. http://www.coverity.com/products/static-analysis.html.

2. Инструмент Klocwork Insight. http://www.klocwork.com/products/insight/.

3. В.С. Несов, О.Р. Маликов. Использование информации о линейных зависимостях для обнаружения уязвимостей в исходном коде программ. Труды Института системного программирования РАН, том 9, стр. 51-56, 2006.

4. В.С. Несов, С.С. Гайсарян. Автоматическое обнаружение дефектов в исходном коде программ. Методы и технические средства обеспечения безопасности информации: Материалы XVII Общероссийской научно-технической конференции. СПб.: Изд-во Политехн. Ун-та, с. 107, 2008.

5. V. Nesov. Automatically Finding Bugs in Open Source Programs. Proceedings of the Third International Workshop on Foundations and Techniques for Open Source Software Certification, Volume 20, pages 19-29, 2009.

6. Инструмент Saturn. http://saturn.stanford.edu/.

7. Инструмент FindBugs. http://findbugs.sourceforge.net/.

8. Инструмент Splint. http://www.splint.org/.

9. T. Ball, E. Bounimova, R. Kumar, V. Levin. SLAM2: Static Driver Verification with Under 4% False Alarms. FMCAD, 2010.

10. D. Beyer, T. Henzinger, R. Jhala, R. Majumdar. The Software Model Checker Blast: Applications to Software Engineering. Int. Journal on Software Tools for Technology Transfer, 9(5-6):505-525, 2007.

11. D. Beyer, M. Keremoglu. CPAchecker: A Tool for Configurable Software Verification. Technical report SFU-CS-2009-02, School of Computing Science (CMPT), Simon Fraser University (SFU), January 2009.

12. E. Clarke, D. Kroening, F. Lerda. A Tool for Checking ANSI-C Programs. In Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, LNCS, Vol. 2988/168-176, 2004.

13. Инструмент ARMC. http://www.mpi-sws.org/~rybal/armc/.

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

15. A. Khoroshilov, V. Mutilin. Formal Methods for Open Source Components Certification. OpenCert 2008 2nd International Workshop on Foundations and Techniques for Open Source Software Certification 52-63 Milan, 2008.

16. A. Khoroshilov, V. Mutilin, V. Shcherbina, O. Strikov, S. Vinogradov, V. Zakharov. How to Cook an Automated System for Linux Driver Verification. SYRCoSE'2008 2nd Spring Young Researchers' Colloquium on Software Engineering, Volume 2 11-14 St. Petersburg May 29-30, 2008.

17. A. Khoroshilov, V. Mutilin, A. Petrenko, V. Zakharov. Establishing Linux Driver Verification Process. PSI 2009 Perspectives of System informatics 2009 LNCS, Vol. 5947/ 165-176, 2009.

18. В.П.Иванников, А.К. Петренко. Задачи верификации ОС Linux в контексте ее использования в государственном секторе. Труды Института системного программирования РАН, том 10, стр. 9-14, 2006.

19. G. Kroah-Hartman, J. Corbet, A. McPherson. Linux kernel development. http://www.linux-foundation.org/publications/linuxkerneldevelopment.php, 2008.

20. A. Chou. An Empirical Study of Operating System Errors. Proc. 18th ACM Symp. Operating System Principles, ACM Press, 2001.

21. M. Swift, B. Bershad, H. Levy. Improving the reliability of commodity operating systems. In: SOSP ’03: Proceedings of the nineteenth ACM symposium on Operating systems principles, New York, NY, USA, ACM 207–222, 2003.

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

23. N. Beckman, A. Nori, S. Rajamani, R. Simmons. Proofs from tests. In ISSTA’08: International Symposium on Software Testing and Analysis, pages 3–14, 2008.

24. 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.

25. 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 (ASE '07), pages 501-504, 2007.

26. E. Clarke, D. Kroening, N. Sharygina, K. Yorav. SATABS: SAT-based Predicate Abstraction for ANSI-C. In Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, LNCS, Vol. 3440/570-574, 2005.

27. Набор инструментов LLVM. http://llvm.org/.

28. Инструмент Linux Driver Verifier. http://forge.ispras.ru/projects/ldv.