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

Верификация драйверов ОС Linux - это широкая область для применения различных методов верификации, в частности, методов проверки свойств безопасности и надежности программ, а также функциональной верификации. Драйверы Linux - это индустриальное программное обеспечение, на стабильность которого полагаются ИТ-инфраструктуры. В силу этого к надежности и корректности их работы предъявляют жесткие требования, в свою очередь, это означает, что если инженер-верификатор обнаружил ошибку в драйвере, он может рассчитывать на быструю реакцию сообщества разработчиков в плане подтверждения и исправления этой ошибки. Драйверы Linux - сложное низкоуровневое системное программное обеспечение, и его характеристики требуют применения различных техник анализа программ: использования SMT-решателей, методов верификации моделей (model checking) и других методов верификации. Точность и эффективность этих методов за последнее время значительно повысилась, и поэтому сложная задача верификации драйверов ОС Linux становится реальной по мере использования этих достижений в инструментах верификации.

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

1. T. Ball, S. K. Rajamani. The Slam Project: Debugging System Software via Static Analysis // Proc. POPL, pp. 1–3. ACM (2002)

2. G. Basler, A. Donaldson, A. Kaiser, D. Kröning, M. Tautschnig, T. Wahl. SATABS: A Bit-Precise Verifier for C Programs // C. Flanagan, B. König (eds.). TACAS 2012. LNCS, vol. 7214, pp. 552–555. Springer, Heidelberg (2012)

3. D. Beyer. Competition on Software Verification // C. Flanagan, B. König (eds.). TACAS 2012. LNCS, vol. 7214, pp. 504–524. Springer, Heidelberg (2012)

4. D. Beyer, A. Cimatti, A. Griggio, M. E. Keremoglu, R. Sebastiani. Software Model Checking via Large-block Encoding // Proc. FMCAD, pp. 25–32. IEEE (2009)

5. D. Beyer, T. A. Henzinger, R. Jhala, R. Majumdar. The Software Model Checker Blast // Int. J. Softw. Tools Technol. Transfer 9(5-6), 505–525 (2007)

6. D. Beyer, T. A. Henzinger, M. E. Keremoglu, P. Wendler. Conditional Model Checking: A Technique to Pass Information Between Verifiers // Proc. FSE. ACM (2012)

7. D. Beyer, T. A. Henzinger, G. Theoduloz. Program Analysis with Dynamic Precision Adjustment // Proc. ASE, pp. 29–38. IEEE (2008)

8. D. Beyer, M. E. Keremoglu. CPAchecker: A Tool for Configurable Software Verification // G. Gopalakrishnan, S. Qadeer (eds.). CAV 2011. LNCS, vol. 6806, pp. 184–190. Springer, Heidelberg (2011)

9. D. Beyer, M. E. Keremoglu, P. Wendler. Predicate Abstraction with Adjustable-Block Encoding // Proc. FMCAD, pp. 189–197. FMCAD (2010)

10. A. Biere, A. Cimatti, E. Clarke, Y. Zhu. Symbolic Model Checking without BDDs. // W. R. Cleaveland (ed.). TACAS 1999. LNCS, vol. 1579, pp. 193–207. Springer, Heidelberg (1999)

11. E. M. Clarke, O. Grumberg, S. Jha, Y. Lu, H. Veith. Counterexample-Guided Abstraction Refinement for Symbolic Model Checking // J. ACM 50(5), 752–794 (2003)

12. E. Clarke, D. Kröning, N. Sharygina, K. Yorav. SatAbs: SAT-Based Predicate Abstraction for ANSI-C // N. Halbwachs, L. D. Zuck (eds.). TACAS 2005. LNCS, vol. 3440, pp. 570–574. Springer, Heidelberg (2005)

13. B. Cook, A. Podelski, A. Rybalchenko. Terminator: Beyond Safety // T. Ball, T., R. B. Jones (eds.). CAV 2006. LNCS, vol. 4144, pp. 415–418. Springer, Heidelberg (2006)

14. L. Cordeiro, J. Morse, D. Nicole, B. Fischer. Context-Bounded Model Checking with ESBMC 1.17 // C. Flanagan, B. König (eds.). TACAS 2012. LNCS, vol. 7214, pp. 534–537. Springer, Heidelberg (2012)

15. P. Cousot, R. Cousot, J. Feret, L. Mauborgne, A. Miné, D. Monniaux, X. Rival. Combination of Abstractions in the ASTREE Static Analyzer // M. Okada, I. Satoh (eds.). ASIAN 2006. LNCS, vol. 4435, pp. 272–300. Springer, Heidelberg (2008)

16. K. Dudka, P. Müller, P. Peringer, T. Vojnar. Predator: A Verification Tool for Programs with Dynamic Linked Data Structures // C. Flanagan, B. König (eds.). TACAS 2012. LNCS, vol. 7214, pp. 545–548. Springer, Heidelberg (2012)

17. A. Galloway, G. Lüttgen, J. T. Mühlberg, R. I. Siminiceanu. Model-Checking the Linux Virtual File System // N. D. Jones, M. Müller-Olm (eds.). VMCAI 2009. LNCS, vol. 5403, pp. 74–88. Springer, Heidelberg (2009)

18. S. Grebenshchikov, A. Gupta, N. P. Lopes, C. Popeea, A. Rybalchenko. HSF(C): A Software Verifier Based on Horn Clauses // C. Flanagan, B. Koenig (eds.). TACAS 2012. LNCS, vol. 7214, pp. 549–551. Springer, Heidelberg (2012)

19. A. Gupta, C. Popeea, A. Rybalchenko. Threader: A Constraint-Based Verifier for Multi-threaded Programs // G. Gopalakrishnan, S. Qadeer (eds.). CAV 2011. LNCS, vol. 6806, pp. 412–417. Springer, Heidelberg (2011)

20. T. A. Henzinger, R. Jhala, R. Majumdar, K. L. McMillan. Abstractions from Proofs // Proc. POPL, pp. 232–244. ACM (2004)

21. T. A. Henzinger, R. Jhala, R. Majumdar, G. Sutre. Lazy Abstraction // Proc. POPL, pp. 58–70. ACM (2002)

22. A. Khoroshilov, V. Mutilin, E. Novikov, P. Shved, A. Strakh. Towards an Open Framework for C Verification Tools Benchmarking // E. Clarke, I. Virbitskaite, A. Voronkov (eds.). PSI 2011. LNCS, vol. 7162, pp. 179–192. Springer, Heidelberg (2012)

23. A. Khoroshilov, V. Mutilin, A. Petrenko, V. Zakharov. Establishing Linux Driver Verification Process // A. Pnueli, I. Virbitskaite, A. Voronkov (eds.). PSI 2009. LNCS, vol. 5947, pp. 165–176. Springer, Heidelberg (2010)

24. J. T. Mühlberg, G. Lüttgen. Blasting Linux Code // L. Brim, B. R. Haverkort, M. Leucker, J. van de Pol (eds.). FMICS 2006 and PDMC 2006. LNCS, vol. 4346, pp. 211–226. Springer, Heidelberg (2007)

25. W. Penninckx, J. T. Mühlberg, J. Smans, B. Jacobs, F. Piessens. Sound Formal Verification of Linux’s USB BP Keyboard Driver // A. E. Goodloe, S. Person (eds.). NFM 2012. LNCS, vol. 7226, pp. 210–215. Springer, Heidelberg (2012)

26. A. Podelski, A. Rybalchenko. Transition Predicate Abstraction and Fair Termination // Proc. POPL, pp. 132–144. ACM (2005)

27. H. Post, C. Sinz, W. Küchlin. Towards Automatic Software Model Checking of Thousands of Linux Modules — A Case Study with Avinux // Softw. Test., Verif. Reliab. 19(2), 155–172 (2009)

28. P. Shved, M. Mandrykin, V. Mutilin. Predicate Analysis with BLAST 2.7 // C. Flanagan, B. König (eds.). TACAS 2012. LNCS, vol. 7214, pp. 525–527. Springer, Heidelberg (2012)

29. П. Е. Швед, В. С. Мутилин, М. У. Мандрыкин. Опыт развития инструмента статической верификации BLAST // Программирование. 2012. Т. 3. с. 24–35.

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

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

32. C. Sinz, F. Merz, S. Falke. LLBMC: A Bounded Model Checker for LLVM’s Intermediate Representation // C. Flanagan, B. König (eds.). TACAS 2012. LNCS, vol. 7214, pp. 542–544. Springer, Heidelberg (2012)

33. A. von Rhein, S. Apel, F. Raimondi. Introducing Binary Decision Diagrams in the Explicit-State Verification of Java Code // Proc. Java Pathfinder Workshop (2011)

34. T. Witkowski, N. Blanc, D. Kröning, G. Weissenbacher. Model Checking Concurrent Linux Device Drivers // Proc. ASE, pp. 501–504. ACM (2007)