Static Verification Tools for C Programs and Linux Device Drivers: A Survey
Abstract
The survey considers methods and techniques used in modern static verification tools for C programs. It describes two main approaches Counter Example Guided Abstraction Refinement (CEGAR) and Bounded Model Checking (BMC) and techniques used to efficiently implement them such as Predicate Abstraction, Abstract Reachability Tree, Lazy Abstraction, Configurable Program Analysis, Explicit Analysis, Interpolation, and Shape Analysis. The paper also discusses current capabilities of the tools such as supported C programming language constructs, scalability, properties being checked, and trustworthiness of analysis results.
We provide description of such static verification tools, as BLAST, CPAchecker, HSF(C), SATABS, SLAM, WOLVERINE, YOGI, CBMC, ESBMC, LLBMC, FSHELL and PREDATOR. This description shows techniques implemented in these tools and their current capabilities. The paper presents results of the 1st International Competition on Software Verification in category DeviceDrivers64 which contains verification tasks based on device drivers from Linux kernel 3.0.
Specifics of device drivers verification are discussed and existing driver verification systems are described including Microsoft SDV for Windows operating system and DDVerify, Avinux and Linux Driver Verification for Linux.
The paper concludes that BMC-based tools work well for programs of limited size and control flow complexity. Regarding verification of device drivers that means these tools are able to quickly find violations of properties being checked if paths to these violations are quite short, but they mostly fail to prove correctness and to find complicated bugs. CEGAR-based tools demonstrate better scalability, while they have problems with handling address arithmetic and complex memory structures. For future improvements in static verification of C programs and Linux device drivers we propose composition of various techniques and modularization of analysis.About the Authors
M. U. Mandrykin
ISP RAS
Russian Federation
Russian Federation
V. S. Mutilin
ISP RAS
Russian Federation
Russian Federation
E. M. Novikov
ISP RAS
Russian Federation
Russian Federation
A. V. Khoroshilov
ISP RAS
Russian Federation
Russian Federation
References
1. Ball T., Cook B., Levin V., Rajamani S. K. SLAM and Static Driver Verifier: Technology transfer of formal methods inside Microsoft. In Proc. Integrated Formal Methods (IFM), LNCS, vol. 2999, pp. 1-20, 2004. doi: 10.1007/978-3-540-24756-2_1
2. Clarke E., Grumberg O., Jha S., Lu Y., Veith H. Counterexample-Guided Abstraction Refinement. In Proc. Computer Aided Verification (CAV), LNCS, vol. 1855, pp 154-169, 2000. doi: 10.1007/10722167_15
3. Graf S., Saidi H. Construction of Abstract State Graphs with PVS. In Proc. Computer Aided Verification (CAV), LNCS, vol. 1254, pp. 72-83, 1997. doi: 10.1007/3-540-63166-6_10
4. Ball T., Rajamani S. K. The Slam project. Debugging system software via static analysis. In Proc. Symposium on Principles of Programming Languages (POPL), pp. 1–3, 2002.
5. Ball T., Bounimova E., Levin V., De Moura L. Efficient evaluation of pointer predicates with Z3 SMT Solver in SLAM2. Microsoft Research Technical Report MSR-TR-2010-24, 2010.
6. Beyer D., Henzinger T., Jhala R., Majumdar R. The Software Model Checker Blast: Applications to Software Engineering. International Journal on Software Tools for Technology Transfer (STTT), vol. 5, pp. 505-525, 2007. doi: 10.1007/s10009-007-0044-z
7. Beyer D., Cimatti A., Griggio A., Keremoglu M.E., Sebastiani R. Software Model Checking via Large-Block Encoding. In Proc. Formal Methods in Computer-Aided Design (FMCAD), pp. 25–32, 2009. doi: 10.1109/FMCAD.2009.5351147
8. McMillan K.L. Lazy abstraction with interpolants. In Proc. Computer Aided Verification (CAV), LNCS, vol. 4144, pp. 123–136, 2006. doi: 10.1007/11817963_14
9. Henzinger T.A., Jhala, R., Majumdar, R., Sutre, G. Lazy abstraction. In Proc. 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages (POPL), Pages 58-70, 2002. doi: 10.1145/503272
10. Henzinger T.A., Jhala R., Majumdar R., McMillan K.L. Abstractions from proofs. In Proc. 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages (POPL), pp. 232-244, 2004. doi: 10.1145/964001.964021
11. Cousot P., Cousot R. Compositional and inductive semantic definitions in fixpoint, equational, constraint, closure-condition, rule-based and game-theoretic form. In Proc. Computer Aided Verification (CAV), LNCS, vol. 939, pp. 293–308, 1995. doi: 10.1007/3-540-60045-0_58
12. Schmidt D.A. Data-flow analysis is model checking of abstract interpretations. In Proc. 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages (POPL), pp. 38–48, 1998. doi: 10.1145/268946.268950
13. Steffen B. Data-flow analysis as model checking. In Proc. Theoretical Aspects of Computer Software (TACS), LNCS, vol. 526, pp. 346–365, 1991. doi: 10.1007/3-540-54415-1_54
14. Gulwani S., Tiwari A. Combining abstract interpreters. In Proc. ACM SIGPLAN conference on Programming language design and implementation (PLDI), pp. 376–386, 2006. doi: 10.1145/1133255.1134026
15. Lerner S., Grove D., Chambers C. Composing data-flow analyses and transformations. In Proc. ACM SIGPLAN-SIGACT symposium on Principles of programming languages (POPL), pp. 270–282, 2002.
16. Beyer D., Henzinger T.A., Théoduloz G. Configurable Software Verification: Concretizing the Convergence of Model Checking and Program Analysis. In Proc. International Conference on Computer Aided Verification (CAV), LNCS, vol. 4590, pp. 504-518, 2007. doi: 10.1007/978-3-540-73368-3_51
17. Fischer J., Jhala R., Majumdar R. Joining data flow with predicates. In Proc. 10th European software engineering conference held jointly with 13th ACM SIGSOFT international symposium on Foundations of software engineering (ESEC/FSE), pp. 227–236, 2005. doi: 10.1145/1081706.1081742
18. Beyer D., Henzinger T. A., Theoduloz G. Program Analysis with Dynamic Precision Adjustment. In Proc. IEEE/ACM International Conference on Automated Software Engineering (ASE), pp. 29-38, 2008. doi: 10.1109/ASE.2008.13
19. Kroening D., Strichman O. Decision Procedures: An Algorithmic Point of View. Journal of Automated Reasoning, vol. 51, issue 4, pp. 453-456, 2008. doi: 10.1007/s10817-013-9295-4
20. Bozzano M., Bruttomesso R., Cimatti A., Junttila T., Ranise S., Van Rossum P., Sebastiani R. Efficient Satisfiability Modulo Theories via Delayed Theory Combination. In Proc. Computer Aided Verification (CAV), LNCS, vol. 3576, pp. 335-349, 2005. doi: 10.1007/11513988_34
21. Craig W. Linear reasoning. Symbolic Logic, vol. 22, pp. 250–268, 1957.
22. Jhala R., Majumdar R. Path Slicing. In Proc. 27th Annual ACM Conference on Programming Language Design and Implementation (PLDI), pp. 38-47, 2005. doi: 10.1145/1065010.1065016
23. Biere A., Cimatti A., Clarke E., Zhu Y. Symbolic Model Checking without BDDs. In Proc. Tools and Algorithms for the Construction and Analysis of Systems (TACAS), LNCS, vol. 1579, pp. 193–207, 1999. doi: 10.1007/3-540-49059-0_14
24. Sagiv M., Reps T., Wilhelm R. Parametric shape analysis via 3-valued logic. ACM Transactions on Programming Languages and Systems (TOPLAS), vol. 24, issue 3, pp. 217–298, 2002. doi: 10.1145/514188.514190
25. Jones N.D., Muchnick S.S. A flexible approach to interprocedural data flow analysis and programs with recursive data structures. In Proc. 9th ACM SIGPLAN-SIGACT symposium on Principles of programming languages (POPL), pp. 66-74, 1982. doi: 10.1145/582153.582161
26. Beyer D., Henzinger T. A., Théoduloz G. Lazy Shape Analysis. In Proc. Computer Aided Verification (CAV), LNCS, vol. 4144, pp. 532-546, 2005. doi: 10.1007/11817963_48
27. Godefroid P., Nori A.V., Rajamani S.K., Tetali S.D. Compositional may-must program analysis: unleashing the power of alternation. In Proc. 37th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages (POPL), pp. 43-56, 2010. doi: 10.1145/1706299.1706307
28. Wonisch D. Block Abstraction Memoization for CPAchecker. In Proc. Tools and Algorithms for the Construction and Analysis of Systems (TACAS), LNCS, vol. 7214, pp. 532–534, 2012. doi: 10.1007/978-3-642-28756-5_41
29. Shved P., Mandrykin M., Mutilin V. Predicate Analysis with Blast 2.7. In Proc. Tools and Algorithms for the Construction and Analysis of Systems (TACAS), LNCS, vol. 7214, pp. 525–527, 2012. doi: 10.1007/978-3-642-28756-5_39
30. Mutilin V.S., Novikov E.M., Strakh А.V., Khoroshilov А.V., Shved P.E. Аrkhitektura Linux Driver Verification [Linux Driver Verification Architecture]. Trudy ISP RАN [The Proceedings of ISP RAS], vol. 20, pp. 163-187, 2011 (in Russian).
31. Beyer D., Keremoglu M.E. CPAchecker: A Tool for Configurable Software Verification. In Proc. Computer Aided Verification (CAV), LNCS, vol. 6806, pp. 184–190, 2011. 10.1007/978-3-642-22110-1_16
32. Löwe S., Wendler P. CPAchecker with Adjustable Predicate Analysis. In Proc. Tools and Algorithms for the Construction and Analysis of Systems (TACAS), LNCS, vol. 7214, pp. 528–530, 2012. doi: 10.1007/978-3-642-28756-5_40
33. Grebenshchikov S., Gupta A., Lopes N.P., Popeea C., Rybalchenko A.. HSF(C): A Software Verifier Based on Horn Clauses. In Proc. Tools and Algorithms for the Construction and Analysis of Systems (TACAS), LNCS, vol. 7214, pp. 549–551, 2012. doi: 10.1007/978-3-642-28756-5_46
34. B. Cook, A. Podelski, and A. Rybalchenko. Termination proofs for systems code. In Proc. ACM SIGPLAN conference on Programming language design and implementation (PLDI), pp. 415–426, 2006. doi: 10.1145/1133981.1134029
35. Basler G., Donaldson A., Kaiser A., Kröning D., Tautschnig M., Wahl T.. SATabs: A Bit-Precise Verifier for C Programs. In Proc. Tools and Algorithms for the Construction and Analysis of Systems (TACAS), LNCS, vol. 7214, pp. 552–555, 2012. doi: 10.1007/978-3-642-28756-5_47
36. Jhala R., Majumdar R. Software model checking. ACM Computing Surveys (CSUR), vol. 41, issue 4, article 21, 2009. doi: 10.1145/1592434.1592438
37. McMillan K.L. The SMV system. Technical Report CMU-CS-92-131, Carnegie Mellon University, 1992.
38. Cook B., Kroening D., Sharygina N. Symbolic model checking for asynchronous Boolean programs. In Proc. Model Checking Software, LNCS, vol. 3639, pp. 75-90, 2005. doi: 10.1007/11537328_9
39. Basler G., Kroening D., Weissenbacher G. SAT-based summarisation for Boolean programs. In Proc. Model Checking Software, LNCS, vol. 4597, pp. 131-148, 2007. doi: 10.1007/978-3-540-73370-6_10
40. Donaldson A., Kaiser A., Kroening D., Wahl T. Symmetry-aware predicate abstraction for shared variable concurrent programs. In Proc. Computer Aided Verification (CAV), LNCS, vol. 6806, pp. 356-371, 2011. 10.1007/978-3-642-22110-1_28
41. Ball T., Rajamani S.K. Bebop: A symbolic model checker for Boolean programs. In Proc. Model Checking Software, LNCS, vol. 1885, pp. 113-130, 2000. doi: 10.1007/10722468_7
42. Buchi J. Regular canonical systems. Archive for Mathematical Logic, vol. 6, issue 3-4, pp. 91-111, 1964. doi: 10.1007/BF01969548
43. Ball T., Rajamani S. Generating abstract explanations of spurious counterexamples in C programs. Technical Report MSR-TR-2002-09, Microsoft Research, 2002.
44. Ball T., Cook B., Das S., Rajamani S.K. Refining Approximations in Software Predicate Abstraction. In Proc. Tools and Algorithms for the Construction and Analysis of Systems (TACAS), LNCS, vol. 2988, pp. 388-403, 2004. doi: 10.1007/978-3-540-24730-2_30
45. Ball T., Podelski A., Rajamani S.K. Relative completeness of abstraction refinement for software model checking. In Proc. Tools and Algorithms for the Construction and Analysis of Systems (TACAS), LNCS, vol. 2280, pp. 158-172, 2002. doi: 10.1007/3-540-46002-0_12
46. Ball T., Bounimova E., Kumar R., Levin V. SLAM2: Static Driver Verification with Under 4% False Alarms. In Proc. Conference on Formal Methods in Computer-Aided Design (FMCAD), pp. 35-42, 2010.
47. Weissenbacher G., Kröning D., Malik S. Wolverine: Battling Bugs with Interpolants. In Proc. Tools and Algorithms for the Construction and Analysis of Systems (TACAS), LNCS, vol. 7214, pp. 556–558, 2012. doi: 10.1007/978-3-642-28756-5_48
48. Nori A.V., Rajamani S.K., Tetali S., Thakur A.V. The Yogi Project: Software Property Checking via Static Analysis and Testing. In Proc. Tools and Algorithms for the Construction and Analysis of Systems (TACAS), LNCS, vol. 5505, pp. 178-181, 2009. doi: 10.1007/978-3-642-00768-2_17
49. Clarke E., Kroening D., Lerda F. A tool for checking ANSI-C programs. In Proc. Tools and Algorithms for the Construction and Analysis of Systems (TACAS), LNCS, vol. 2988, pp. 168-176, 2004. doi: 10.1007/978-3-540-24730-2_15
50. Cordeiro L., Morse J., Nicole D., Fischer B. Context-Bounded Model Checking with ESBMC 1.17. In Proc. Tools and Algorithms for the Construction and Analysis of Systems (TACAS), LNCS, vol. 7214, pp. 535–538, 2012. doi: 10.1007/978-3-642-28756-5_42
51. Sinz C., Merz F., Falke S. LLBMC: A Bounded Model Checker for LLVM’s Intermediate Representation. In Proc. Tools and Algorithms for the Construction and Analysis of Systems (TACAS), LNCS, vol. 7214, pp. 542–544, 2012. doi: 10.1007/978-3-642-28756-5_44
52. Holzer A., Kröning D., Schallhart C., Tautschnig M., Veith H. Proving Reachability Using FShell. In Proc. Tools and Algorithms for the Construction and Analysis of Systems (TACAS), LNCS, vol. 7214, pp. 538-541, 2012. doi: 10.1007/978-3-642-28756-5_43
53. Dudka K., Müller P., Peringer P., Vojnar T. Predator: A Verification Tool for Programs with Dynamic Linked Data Structures. In Proc. Tools and Algorithms for the Construction and Analysis of Systems (TACAS), LNCS, vol. 7214, pp. 545-548, 2012. doi: 10.1007/978-3-642-28756-5_45
54. Beyer D. Competition on Software Verification. In Proc. Tools and Algorithms for the Construction and Analysis of Systems (TACAS), LNCS, vol. 7214, pp. 504-524, 2012. doi: 10.1007/978-3-642-28756-5_38
55. Ball T., Bounimova E., Levin V., Kumar R., Lichtenberg J. The static driver verifier research platform. In Proc. Computer Aided Verification (CAV), LNCS, vol. 6174, pp. 119-122, 2010. 10.1007/978-3-642-14295-6_11.
56. Ball T., Rajamani S.K. SLIC: A specification language for interface checking. Technical report MSR-TR-2001-21, Microsoft Research, 2001.
57. Witkowski T., Blanc N., Kroening D., Weissenbacher G. Model checking concurrent linux device drivers. In Proc. IEEE/ACM International Conference on Automated Software Engineering (ASE), pp. 501-504, 2007. doi: 10.1145/1321631.1321719.
58. Post H., Küchlin W. Integrated static analysis for Linux device driver verification. In Proc. Integrated Formal Methods (IFM), LNCS, vol. 4591, pp. 518-537, 2007. doi: 10.1007/978-3-540-73210-5_27
59. Post H., Kuchlin W. Automatic data environment construction for static device drivers analysis. In Proc. Conference on Specification and Verification of Component-Based Systems (SAVCBS), pp. 89–92, 2006. doi: 10.1145/1181195.1181215
Review
For citations:
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.)
Email this article 