Linux Driver Verification Architecture
Abstract
The paper discusses requirements to a twofold verification system that should be an open platform for experimentation with various verification techniques as well as an industrial-ready domain specific verification tool for Linux device drivers. An architecture of a verification system implementing the requirements is presented and its components are described in details. Finally, we discuss the first experience of usage of the system and evaluate directions for its further development.
About the Authors
V. S. Mutilin
ISP RAS, Moscow
Russian Federation
Russian Federation
E. M. Novikov
ISP RAS, Moscow
Russian Federation
Russian Federation
A. V. Strakh
ISP RAS, Moscow
Russian Federation
Russian Federation
A. V. Khoroshilov
ISP RAS, Moscow
Russian Federation
Russian Federation
P. E. Shved
ISP RAS, Moscow
Russian Federation
Russian Federation
References
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.
Review
For citations:
Mutilin V.S., Novikov E.M., Strakh A.V., Khoroshilov A.V., Shved P.E. Linux Driver Verification Architecture. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2011;20. (In Russ.)
Email this article 