Обзор инструментов статической верификации Си программ в применении к драйверам устройств операционной системы Linux
Аннотация
В работе рассмотрены методы и техники, используемые в современных инструментах статической верификации Си программ. Представлен обзор текущих возможностей инструментов, в том числе по таким направлениям, как поддержка конструкций языка Си, масштабируемость, виды проверяемых свойств и достоверность результатов анализа. Рассмотрены особенности применения инструментов статической верификации для анализа исходного кода драйверов устройств операционных систем и описаны существующие системы верификации драйверов, построенные на основе таких инструментов.
Об авторах
М. У. Мандрыкин
ИСП РАН
Россия
Россия
В. С. Мутилин
ИСП РАН
Россия
Россия
Е. М. Новиков
ИСП РАН
Россия
Россия
А. В. Хорошилов
ИСП РАН
Россия
Россия
Список литературы
1. T. Ball, B. Cook, V. Levin, and S. K. Rajamani. SLAM and Static Driver Verifier: Technology transfer of formal methods inside Microsoft. In Integrated Formal Methods (IFM), volume 2999 of LNCS. Springer, 2004.
2. E. M. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith. Counterexample-guided abstraction refinement for symbolic model checking. J. ACM, 50(5), 752–794, 2003.
3. S. Graf and H. Saïdi. Construction of abstract state graphs with Pvs. In Proc. CAV, LNCS 1254, pages 72–83. Springer, 1997.
4. T. Ball and S. K. Rajamani. The Slam project. Debugging system software via static analysis. In Proc. POPL, pages 1–3. ACM, 2002.
5. T. Ball, E. Bounimova, V. Levin, and L. De Moura. Efficient evaluation of pointer predicates with Z3 SMT Solver in SLAM2. 2010.
6. Beyer, D., Henzinger, T.A., Jhala, R., Majumdar, R. The Software Model Checker Blast. Int. J. Softw. Tools Technol. Transfer 9 (5-6), 505–525, 2007.
7. D. Beyer, A. Cimatti, A. Griggio, M.E. Keremoglu, R. Sebastiani. Software Model Checking via Large-Block Encoding. In Proc. FMCAD, pp. 25–32. IEEE, 2009.
8. K.L. McMillan. Lazy abstraction with interpolants. In CAV. Volume 4144 of LNCS. Springer, pp. 123–136, 2006.
9. T. A. Henzinger, R. Jhala, R. Majumdar, and G. Sutre. Lazy Abstraction. Proceedings of the 29th Annual Symposium on Principles of Programming Languages (POPL), ACM Press, pp. 58-70, 2002.
10. T. A. Henzinger, R. Jhala, R. Majumdar, and K. L. McMillan. Abstractions from proofs. POPL '04 Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, ACM New York, NY, USA, 2004.
11. P. Cousot and R. Cousot. Compositional and inductive semantic definitions in fixpoint, equational, constraint, closure-condition, rule-based and game-theoretic form. In Wolper, P. (ed.) CAV 1995. LNCS, vol. 939, pp. 293–308. Springer, Heidelberg, 1995.
12. D.A. Schmidt. Data-flow analysis is model checking of abstract interpretations. In Proc. POPL, pp. 38–48. ACM Press, New York, 1998.
13. B. Steffen. Data-flow analysis as model checking. In Proc. TACS, pp. 346–365, 1991.
14. S. Gulwani and A. Tiwari. Combining abstract interpreters. In Proc. PLDI, pp. 376–386. ACM Press, New York, 2006.
15. S. Lerner, D. Grove, and C. Chambers. Composing data-flow analyses and transformations. In Proc. POPL, pp. 270–282. ACM Press, New York, 2002.
16. D. Beyer, T. A. Henzinger, and G. Théoduloz. Configurable Software Verification: Concretizing the Convergence of Model Checking and Program Analysis. Proceedings of the 19th International Conference on Computer Aided Verification (CAV 2007), pp. 504-518, 2007.
17. J. Fischer, R. Jhala, and R. Majumdar. Joining data flow with predicates. In: Proc. ESEC/FSE, pp. 227–236. ACM Press, New York, 2005.
18. D. Beyer, T. A. Henzinger, and G. Theoduloz. Program Analysis with Dynamic Precision Adjustment. ASE '08 Proceedings of the 2008 23rd IEEE/ACM International Conference on Automated Software Engineering, IEEE Computer Society Washington, DC, USA, 2008.
19. D. Kroening, O. Strichman. Decision Procedures. An Algorithmic Point of View. Springer, 2008.
20. M. Bozzano, R. Bruttomesso, A. Cimatti, T. Junttila, S. Ranise, P. van Rossum, and R. Sebastiani. Efficient Satisfiability Modulo Theories via Delayed Theory Combination. CAV'05, 2005.
21. W. Craig. Linear reasoning. J. Symbolic Logic 22, 250–268, 1957.
22. R. Jhala and R. Majumdar. Path Slicing. Proceedings of the 27th Annual ACM Conference on Programming Language Design and Implementation, 2005. (PLDI), 2005.
23. A. Biere, A. Cimatti, E. Clarke, Y. Zhu. Symbolic Model Checking without BDDs. In Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 193–207. Springer, Heidelberg, 1999.
24. M. Sagiv, T. Reps, R. Wilhelm. Parametric shape analysis via 3-valued logic. ACM Transactions on Programming Languages and Systems (TOPLAS), 24 (3), pp. 217–298, 2002.
25. N.D. Jones, S.S. Muchnick. A flexible approach to interprocedural data flow analysis and programs with recursive data structures. POPL '82 Proceedings of the 9th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, 1982.
26. Dirk Beyer, Thomas A. Henzinger, and Grégory Théoduloz. Lazy Shape Analysis. In T. Ball and R.B. Jones, editors, Proceedings of the 18th International Conference on Computer Aided Verification (CAV 2006), LNCS 4144, pages 532-546, Springer-Verlag, Berlin, 2006.
27. P. Godefroid, A. V. Nori, S. K. Rajamani, and S. D. Tetali. Compositional may-must program analysis: unleashing the power of alternation. POPL '10 Proceedings of the 37th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, ACM New York, NY, USA, 2010.
28. D. Wonisch. Block Abstraction Memoization for CPAchecker. In Flanagan, C., König, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 532–534. Springer, Heidelberg, 2012.
29. P. Shved, M. Mandrykin, V. Mutilin. Predicate Analysis with Blast 2.7. In Flanagan, C., König, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 525–527. Springer, Heidelberg, 2012.
30. В.С. Мутилин, Е.М. Новиков, А.В. Страх, А.В. Хорошилов, П.Е. Швед. Архитектура Linux Driver Verification. Труды Института системного программирования РАН, том 20, cтр. 163-187, 2011.
31. D. Beyer, M.E. Keremoglu. CPAchecker: A Tool for Configurable Software Verification. In Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 184–190. Springer, Heidelberg, 2011.
32. S. Löwe, P. Wendler. CPAchecker with Adjustable Predicate Analysis. In Flanagan, C., König, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 528–530. Springer, Heidelberg, 2012.
33. S. Grebenshchikov, A. Gupta, N.P. Lopes, C. Popeea, A. Rybalchenko. HSF(C): A Software Verifier Based on Horn Clauses. In Flanagan, C., König, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 549–551. Springer, Heidelberg, 2012.
34. B. Cook, A. Podelski, and A. Rybalchenko. Termination proofs for systems code. PLDI, 2006.
35. G. Basler, A. Donaldson, A. Kaiser, D. Kröning, M. Tautschnig, T. Wahl. SATabs: A Bit-Precise Verifier for C Programs. In Flanagan, C., König, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 552–555. Springer, Heidelberg, 2012.
36. R. Jhala and R. Majumdar. Software model checking. ACM Computing Surveys, 2009.
37. K.L. McMillan. The SMV system. Technical Report CMU-CS-92-131, Carnegie Mellon University, 1992.
38. B. Cook, D. Kroening, and N. Sharygina. Symbolic model checking for asynchronous Boolean programs. In SPIN Workshop on Model Checking of Software, volume 3639 of LNCS. Springer, 2005.
39. G. Basler, D. Kroening, and G. Weissenbacher. SAT-based summarisation for Boolean programs. In SPIN Workshop on Model Checking of Software, volume 4595 of LNCS, 2007.
40. A. Donaldson, A. Kaiser, D. Kroening, T. Wahl. Symmetry-aware predicate abstraction for shared variable concurrent programs. Proceedings of the 23rd international conference on Computer aided verification, p.356-371, July 14-20, 2011.
41. T. Ball and S. K. Rajamani. Bebop: A symbolic model checker for Boolean programs. In Model Checking and Software Verification (SPIN), volume 1885 of LNCS, pages 113–130. Springer, 2000.
42. J. R. Buchi. Regular canonical systems. Archive for Mathematical Logic, 6(3-4):91, April 1964.
43. T. Ball, and S. Rajamani. Generating abstract explanations of spurious counterexamples in C programs. Tech. Rep. MSR-TR-2002-09, Microsoft Research, 2002.
44. T. Ball, B. Cook, S. Das, S. K. Rajamani. Refining Approximations in Software Predicate Abstraction. TACAS 2004, 2004.
45. T. Ball, A. Podelski, and S. K. Rajamani. Relative completeness of abstraction refinement for software model checking. In TACAS 02: Tools and Algorithms for Construction and Analysis of Systems. Lecture Notes in Computer Science 2280. Springer-Verlag, 158–172, 2002.
46. T. Ball, E. Bounimova, R. Kumar, V. Levin. SLAM2: Static Driver Verification with Under 4% False Alarms. FMCAD, 2010.
47. Weissenbacher, G., Kröning, D., Malik, S.: Wolverine: Battling Bugs with Interpolants. In Flanagan, C., König, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 556–558. Springer, Heidelberg (2012)
48. A. V. Nori, S. K. Rajamani, S. Tetali, A. V. Thakur. The Yogi Project: Software Property Checking via Static Analysis and Testing. In TACAS '09: Tools and Algorithms for the Construction and Analysis of Systems, March, 2009.
49. 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.
50. L. Cordeiro, J. Morse, D. Nicole, B. Fischer. Context-Bounded Model Checking with Esbmc. In Flanagan, C., König, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 535–538. Springer, Heidelberg, 2012.
51. C. Sinz, F. Merz, S. Falke. Llbmc: A Bounded Model Checker for Llvms Intermediate Representation. In Flanagan, C., König, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 542–544. Springer, Heidelberg, 2012.
52. A. Holzer, D. Kröning, C. Schallhart, M. Tautschnig, H. Veith. Proving Reachability Using FShell. In Flanagan, C., König, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 538–541. Springer, Heidelberg, 2012.
53. K. Dudka, P. Müller, P. Peringer, T. Vojnar. Predator: A Verification Tool for Programs with Dynamic Linked Data Structures. In Flanagan, C., König, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 545–548. Springer, Heidelberg, 2012.
54. D. Beyer. Competition on Software Verification. In Flanagan, C., König, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 504–524. Springer, Heidelberg, 2012.
55. T. Ball, E. Bounimova, V. Levin et al. The static driver verifier research platform. Computer Aided Verification, pp. 119–122, 2010.
56. T. Ball, S.K. Rajamani. SLIC: A specification language for interface checking. Tech. rep. Microsoft Research, 2001.
57. 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.
58. 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.
59. H. Post, W. Kuchlin. Automatic data environment construction for static device drivers analysis. Proceedings of the 2006 conference on Specification and verification of component-based systems (SAVCBS ’06), ACM, pp. 89–92, 2006.
Рецензия
Для цитирования:
Мандрыкин М.У., Мутилин В.С., Новиков Е.М., Хорошилов А.В. Обзор инструментов статической верификации Си программ в применении к драйверам устройств операционной системы Linux. Труды Института системного программирования РАН. 2012;22.
For citation:
Mandrykin M.U., Mutilin V.S., Novikov E.M., Khoroshilov A.V. Static Verification Tools for C Programs and Linux Device Drivers: A Survey. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2012;22. (In Russ.)
Послать статью по эл. почте 